Learning to Prove Theorems via Interacting with Proof Assistants

21 May 2019

ArXiv (abs)PDF HTML Github (403★)

Papers citing "Learning to Prove Theorems via Interacting with Proof Assistants"

48 / 48 papers shown

Title
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Nikita Khramov Andrei Kozyrev Gleb Solovev Anton Podkopaev 66 0 0 28 May 2025
Generative Evaluation of Complex Reasoning in Large Language Models Haowei Lin Xiang Wang Ruilin Yan Baizhou Huang Haotian Ye Jianhua Zhu Zihao Wang James Zou Jianzhu Ma Yitao Liang ReLM ELM LRM 449 0 0 03 Apr 2025
Steering LLMs for Formal Theorem Proving Shashank Kirtania Arun Shankar Iyer LLMSV 531 0 0 21 Feb 2025
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques Sangjun Han Taeil Hur Youngmi Hur Kathy Sangkyung Lee Myungyoon Lee Hyojae Lim 496 0 0 20 Feb 2025
One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs Hai-Tao Zheng Jiayi Kuang Haojing Huang Zhikun Xu Xinnian Liang ... Jue Chen Chao Qu Ying Shen Hai-Tao Zheng Philip S. Yu LRM 150 2 0 12 Feb 2025
Mathematical Language Models: A Survey Wen Liu Hanglei Hu Jie Zhou Yuyang Ding Junsong Li ... Mengliang He Qin Chen Bo Jiang Aimin Zhou Liang He LRM 235 14 0 03 Jan 2025
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 226 4 0 18 Dec 2024
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 Leni Aniva Chuyue Sun Alycia Lee Clark W. Barrett Sanmi Koyejo 91 6 0 21 Oct 2024
AutoVerus: Automated Proof Generation for Rust Code Chenyuan Yang Xuheng Li Md Rakib Hossain Misu Jianan Yao Weidong Cui ... Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou Shan Lu 102 11 0 19 Sep 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 161 10 0 05 Aug 2024
DafnyBench: A Benchmark for Formal Software Verification Chloe Loughridge Qinyi Sun Seth Ahrenbach Federico Cassano Chuyue Sun Ying Sheng Anish Mudide Md Rakib Hossain Misu Nada Amin Max Tegmark ALM AI4CE 86 12 0 12 Jun 2024
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems Huaiyuan Ying Zijian Wu Yihan Geng Zheng Yuan Dahua Lin Kai Chen 173 42 0 06 Jun 2024
REFACTOR: Learning to Extract Theorems from Proofs Jin Peng Zhou Yuhuai Wu Qiyang Li Roger C. Grosse AIMat 85 8 0 26 Feb 2024
Learning Structure-Aware Representations of Dependent Types Konstantinos Kogkalidis Orestis Melkonian Jean-Philippe Bernardy NAI 70 3 0 03 Feb 2024
The Tactician's Web of Large-Scale Formal Knowledge Lasse Blaauwbroek 58 4 0 05 Jan 2024
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method Rahul Vishwakarma Subhankar Mishra AIMat 74 1 0 20 Dec 2023
Leveraging Large Language Models for Automated Proof Synthesis in Rust Jianan Yao Ziqiao Zhou Weiteng Chen Weidong Cui 52 15 0 07 Nov 2023
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Kaiyu Yang Aidan M. Swope Alex Gu Rahul Chalamala Peiyang Song Shixing Yu Saad Godil R. Prenger Anima Anandkumar RALM 152 247 0 27 Jun 2023
CoProver: A Recommender System for Proof Construction Eric Yeh Briland Hitaj S. Owre Maena Quemener N. Shankar 103 5 0 01 Mar 2023
A Survey of Deep Learning for Mathematical Reasoning Pan Lu Liang Qiu Wenhao Yu Sean Welleck Kai-Wei Chang ReLM LRM 133 150 0 20 Dec 2022
Genetic Algorithm for Program Synthesis Yutaka Nagashima 74 1 0 22 Nov 2022
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Albert Q. Jiang Sean Welleck Jin Peng Zhou Wenda Li Jiacheng Liu M. Jamnik Timothée Lacroix Yuhuai Wu Guillaume Lample AIMat 157 181 0 21 Oct 2022
Project proposal: A modular reinforcement learning based automated theorem prover Boris Shminke 64 1 0 06 Sep 2022
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis Jonathan Laurent André Platzer 107 9 0 27 May 2022
Generating Natural Language Proofs with Verifier-Guided Search Kaiyu Yang Jia Deng Danqi Chen LRM 130 72 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 156 127 0 03 Feb 2022
Learning Symbolic Rules for Reasoning in Quasi-Natural Language Kaiyu Yang Jia Deng NAI ReLM LRM 61 13 0 23 Nov 2021
Generating Symbolic Reasoning Problems with Transformer GANs Jens U. Kreber Christopher Hahn AI4CE 115 6 0 19 Oct 2021
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics Kunhao Zheng Jesse Michael Han Stanislas Polu AIMat 151 178 0 31 Aug 2021
Contrastive Reinforcement Learning of Symbolic Reasoning Domains Gabriel Poesia Wenxin Dong Noah D. Goodman 174 19 0 16 Jun 2021
NaturalProofs: Mathematical Theorem Proving in Natural Language Sean Welleck Jiacheng Liu Ronan Le Bras Hannaneh Hajishirzi Yejin Choi Kyunghyun Cho AIMat 98 69 0 24 Mar 2021
Blindspots in Python and Java APIs Result in Vulnerable Code Yuriy Brun Tian Lin J. Somerville Elisha M Myers Natalie C. Ebner 63 7 0 10 Mar 2021
Training a First-Order Theorem Prover from Synthetic Data Vlad Firoiu Eser Aygun Ankit Anand Zafarali Ahmed Xavier Glorot Laurent Orseau Lei Zhang Doina Precup Shibl Mourad NAI 80 14 0 05 Mar 2021
Proof Artifact Co-training for Theorem Proving with Language Models Jesse Michael Han Jason M. Rute Yuhuai Wu Edward W. Ayers Stanislas Polu AIMat 117 127 0 11 Feb 2021
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning Yuhuai Wu M. Rabe Wenda Li Jimmy Ba Roger C. Grosse Christian Szegedy AIMat LRM 144 57 0 15 Jan 2021
Faster Smarter Induction in Isabelle/HOL Yutaka Nagashima 87 7 0 19 Sep 2020
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving Yuhuai Wu Albert Qiaochu Jiang Jimmy Ba Roger C. Grosse AIMat 108 55 0 06 Jul 2020
Retro: Learning Retrosynthetic Planning with Neural Guided A Search Binghong Chen Chengtao Li H. Dai Le Song 78 109 0 29 Jun 2020
Learning to Prove from Synthetic Theorems Eser Aygun Zafarali Ahmed Ankit Anand Vlad Firoiu Xavier Glorot Laurent Orseau Doina Precup Shibl Mourad NAI 70 20 0 19 Jun 2020
IsarStep: a Benchmark for High-level Mathematical Reasoning Wenda Li Lei Yu Yuhuai Wu Lawrence Charles Paulson AIMat LRM 77 10 0 13 Jun 2020
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek Josef Urban H. Geuvers 114 24 0 20 Mar 2020
Learning Compositional Rules via Neural Program Synthesis Maxwell Nye Armando Solar-Lezama J. Tenenbaum Brenden M. Lake NAI LRM 83 118 0 12 Mar 2020
Teaching Temporal Logics to Neural Networks Christopher Hahn Frederik Schmitt Jens U. Kreber M. Rabe Bernd Finkbeiner NAI 109 67 0 06 Mar 2020
Learning to Prove Theorems by Learning to Generate Theorems Mingzhe Wang Jia Deng NAI 132 50 0 17 Feb 2020
From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group) Zied Bouraoui Antoine Cornuéjols Thierry Denoeux Sebastien Destercke Didier Dubois ... Jérôme Mengin H. Prade Steven Schockaert M. Serrurier Christel Vrain 128 14 0 13 Dec 2019
Learning to Reason in Large Theories without Imitation Kshitij Bansal Christian Szegedy M. Rabe Sarah M. Loos Viktor Toman NAI LRM 107 42 0 25 May 2019
Graph Representations for Higher-Order Logic and Theorem Proving Aditya Sanjay Paliwal Sarah M. Loos M. Rabe Kshitij Bansal Christian Szegedy AI4CE NoLa 206 98 0 24 May 2019
Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning Gil Lederman M. Rabe Edward A. Lee Sanjit A. Seshia 89 38 0 20 Jul 2018