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"

50 / 93 papers shown

Title
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Nikita Khramov Andrei Kozyrev Gleb Solovev Anton Podkopaev 68 0 0 28 May 2025
Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities Haoyu Zhao Yihan Geng Shange Tang Yong Lin Bohan Lyu Hongzhou Lin Chi Jin Sanjeev Arora 93 0 0 19 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 70 0 0 27 Apr 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
A Survey on Mathematical Reasoning and Optimization with Large Language Models Ali Forootani OffRL LRM AI4CE 127 1 0 22 Mar 2025
From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems Zekun Zhou Xiaocheng Feng L. Huang Xiachong Feng Ziyun Song ... Baoxin Wang Dayong Wu Guoping Hu Ting Liu Bing Qin AI4TS 127 1 0 03 Mar 2025
Steering LLMs for Formal Theorem Proving Shashank Kirtania Arun Shankar Iyer LLMSV 533 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 499 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 153 2 0 12 Feb 2025
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation Quinn Dougherty Ronak Mehta ALM 97 2 0 08 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 237 14 0 03 Jan 2025
Formal Mathematical Reasoning: A New Frontier in AI Kaiyu Yang Gabriel Poesia Jingxuan He Wenda Li Kristin Lauter Swarat Chaudhuri Dawn Song LRM AI4CE 160 36 0 20 Dec 2024
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 240 4 0 18 Dec 2024
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction Liao Zhang David M. Cerna C. Kaliszyk 59 0 0 02 Nov 2024
Cobblestone: Iterative Automation for Formal Verification Saketh Ram Kasibatla Arpan Agarwal Yuriy Brun Sorin Lerner Talia Ringer Emily First 43 1 0 25 Oct 2024
CoqPilot, a plugin for LLM-based generation of proofs Andrei Kozyrev Gleb Solovev Nikita Khramov Anton Podkopaev 41 5 0 25 Oct 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
AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs Mert Ünsal Timon Gehr Martin Vechev 96 0 0 03 Oct 2024
In-Context Learning May Not Elicit Trustworthy Reasoning: A-Not-B Errors in Pretrained Language Models Pengrui Han Peiyang Song Haofei Yu Jiaxuan You ReLM LRM 80 1 0 23 Sep 2024
Proof Automation with Large Language Models Minghai Lu Benjamin Delaware Tianyi Zhang LRM 84 9 0 22 Sep 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
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning Alex Sanchez-Stern Abhishek Varghese Zhanna Kaufman Dylan Zhang Talia Ringer Yuriy Brun 137 2 0 17 Aug 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 163 10 0 05 Aug 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Zijian Wu Jiayu Wang Dahua Lin Kai-xiang Chen 101 15 0 24 Jul 2024
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition George Tsoukalas Jasper Lee John Jennings Jimmy Xin Michelle Ding Michael Jennings Amitayush Thakur Swarat Chaudhuri LRM AIMat 147 28 0 15 Jul 2024
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent Mahdi Buali Robert Hoehndorf 94 0 0 05 Jul 2024
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts Ruida Wang Jipeng Zhang Yizhen Jia Boyao Wang Shizhe Diao Renjie Pi Tong Zhang LRM 101 23 0 03 Jul 2024
Proving Olympiad Algebraic Inequalities without Human Demonstrations Chenrui Wei Mengzhou Sun Wei Wang LRM 112 9 0 20 Jun 2024
miniCodeProps: a Minimal Benchmark for Proving Code Properties Evan Lohn Sean Welleck 67 6 0 16 Jun 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
Process-Driven Autoformalization in Lean 4 Jianqiao Lu Zhengying Liu Yingjia Wan Yinya Huang Haiming Wang Zhicheng YANG Jing Tang Zhijiang Guo AI4CE 133 19 0 04 Jun 2024
Autoformalizing Euclidean Geometry Logan Murphy Kaiyu Yang Jialiang Sun Zhaoyu Li A. Anandkumar Xujie Si 69 6 0 27 May 2024
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Saikat Chakraborty Gabriel Ebner Siddharth Bhat Sarah Fakhoury Sakina Fatima Shuvendu K. Lahiri Nikhil Swamy 88 16 0 03 May 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 103 10 0 18 Apr 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 123 32 0 15 Apr 2024
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code Andreas Florath 59 0 0 19 Mar 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 93 5 0 06 Mar 2024
REFACTOR: Learning to Extract Theorems from Proofs Jin Peng Zhou Yuhuai Wu Qiyang Li Roger C. Grosse AIMat 88 8 0 26 Feb 2024
Learning Better Representations From Less Data For Propositional Satisfiability Mohamed Ghanem Frederik Schmitt Julian Siber Bernd Finkbeiner NAI 67 0 0 13 Feb 2024
Learning Structure-Aware Representations of Dependent Types Konstantinos Kogkalidis Orestis Melkonian Jean-Philippe Bernardy NAI 70 3 0 03 Feb 2024
Large Language Models for Mathematical Reasoning: Progresses and Challenges Janice Ahn Rishu Verma Renze Lou Di Liu Rui Zhang Wenpeng Yin LRM 158 146 0 31 Jan 2024
Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion Dylan Zhang Curt Tigges Zory Zhang Stella Biderman Maxim Raginsky Talia Ringer 120 12 0 23 Jan 2024
The Tactician's Web of Large-Scale Formal Knowledge Lasse Blaauwbroek 58 4 0 05 Jan 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts Lasse Blaauwbroek Miroslav Olšák Jason Rute F. I. S. Massolo Jelle Piepenbrock Vasily Pestun 96 11 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
Large Language Models for Mathematicians Simon Frieder Julius Berner P. Petersen Thomas Lukasiewicz 63 7 0 07 Dec 2023
Leveraging Large Language Models for Automated Proof Synthesis in Rust Jianan Yao Ziqiao Zhou Weiteng Chen Weidong Cui 54 15 0 07 Nov 2023
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models Jing Xiong Jianhao Shen Ye Yuan Haiming Wang Yichun Yin ... Yinya Huang Chuanyang Zheng Xiaodan Liang Ming Zhang Qun Liu AIMat LRM 63 20 0 16 Oct 2023
An In-Context Learning Agent for Formal Theorem-Proving Amitayush Thakur George Tsoukalas Yeming Wen Jimmy Xin Swarat Chaudhuri LLMAG 80 33 0 06 Oct 2023