LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

27 June 2023

Papers citing "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models"

50 / 147 papers shown

Title
CLEVER: A Curated Benchmark for Formally Verified Code Generation Amitayush Thakur Jasper Lee George Tsoukalas Meghana Sistla Matthew Zhao Stefan Zetzsche Greg Durrett Yisong Yue Swarat Chaudhuri ALM 12 0 0 20 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 14 0 0 19 May 2025
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation Junyu Lai Jiakun Zhang Shuo Xu Taolue Chen Zihang Wang Yao Yang Jiarui Zhang Chun Cao Jingwei Xu 7 0 0 17 May 2025
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation Zhenwen Liang Linfeng Song Yang Li Tao Yang Feng Zhang Haitao Mi Dong Yu LRM 17 0 0 16 May 2025
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 29 0 0 09 May 2025
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving Qi Liu Xinhao Zheng Renqiu Xia Xingzhi Qi Qinxiang Cao Junchi Yan AIMat 52 0 0 07 May 2025
Knowledge Augmented Complex Problem Solving with Large Language Models: A Survey Da Zheng Lun Du Junwei Su Yuchen Tian Yuqi Zhu Jintian Zhang Lanning Wei Ningyu Zhang H. Chen LRM 61 0 0 06 May 2025
FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models Zhouliang Yu Ruotian Peng Keyi Ding Y. K. Li Zhongyuan Peng ... Huajian Xin Yifan Jiang Yandong Wen Ge Zhang Weiyang Liu LRM 165 1 0 05 May 2025
ACE: A Security Architecture for LLM-Integrated App Systems Evan Li Tushin Mallick Evan Rose William K. Robertson Alina Oprea Cristina Nita-Rotaru 52 0 0 29 Apr 2025
Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework Yuan Xia Akanksha Atrey Fadoua Khmaissia Kedar S. Namjoshi LRM ELM 45 0 0 28 Apr 2025
Toward Generalizable Evaluation in the LLM Era: A Survey Beyond Benchmarks Yixin Cao Shibo Hong Xuzhao Li Jiahao Ying Yubo Ma ... Juanzi Li Aixin Sun Xuanjing Huang Tat-Seng Chua Tianwei Zhang ALM ELM 96 2 0 26 Apr 2025
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification Balaji Rao William Eiers Carlo Lipizzi 37 0 0 23 Apr 2025
Leanabell-Prover: Posttraining Scaling in Formal Reasoning Jingyuan Zhang Qi Wang Xingguang Ji Yong-Jin Liu Yang Yue Fuzheng Zhang Di Zhang Guorui Zhou Kun Gai LRM 44 4 0 08 Apr 2025
FEABench: Evaluating Language Models on Multiphysics Reasoning Ability N. Mudur Hao Cui Subhashini Venugopalan Paul Raccuglia M. Brenner Peter C. Norgaard LLMAG ELM LRM 45 0 0 08 Apr 2025
Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving Sara Rajaee Kumar Pratik Gabriele Cesa Arash Behboodi OffRL LRM 61 0 0 12 Mar 2025
Machine Learning meets Algebraic Combinatorics: A Suite of Datasets Capturing Research-level Conjecturing Ability in Pure Mathematics Herman Chau Helen Jenne Davis Brown Jesse He Mark Raugas Sara Billey Henry Kvinge 38 0 0 09 Mar 2025
MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving Ruida Wang Rui Pan Yuxin Li Jipeng Zhang Yizhen Jia Shizhe Diao Renjie Pi Junjie Hu Tong Zhang LRM LLMAG 95 6 0 05 Mar 2025
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction Suozhi Huang Peiyang Song Robert Joseph George Anima Anandkumar AI4TS LRM 50 2 0 25 Feb 2025
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization Shuming Shi Ruobing Zuo Gaolei He Jianlin Wang Chenyang Xu Zhengfeng Yang 69 0 0 25 Feb 2025
Forecasting Rare Language Model Behaviors Erik Jones Meg Tong Jesse Mu Mohammed Mahfoud Jan Leike Roger C. Grosse Jared Kaplan William Fithian Ethan Perez Mrinank Sharma 47 1 0 24 Feb 2025
Activation Steering in Neural Theorem Provers Shashank Kirtania LLMSV 219 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 185 0 0 20 Feb 2025
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs David Yin Jing Gao 44 0 0 16 Feb 2025
A cross-regional review of AI safety regulations in the commercial aviation Penny A. Barr Sohel M. Imroz 49 0 0 12 Feb 2025
ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data Xiaoyang Liu Kangjie Bao Jiashuo Zhang Yunqi Liu Yu Chen Yu Chen Yang Jiao Tao Luo AIMat 55 0 0 08 Feb 2025
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation Quinn Dougherty Ronak Mehta ALM 51 1 0 08 Feb 2025
RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation Sicheng Zhong Jiading Zhu Yifang Tian Xujie Si 57 0 0 07 Feb 2025
Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoning Yibo Yan Shen Wang Jiahao Huo Jingheng Ye Zhendong Chu Xuming Hu Philip S. Yu Carla P. Gomes B. Selman Qingsong Wen LRM 130 13 0 05 Feb 2025
Advanced Weakly-Supervised Formula Exploration for Neuro-Symbolic Mathematical Reasoning Yuxuan Wu Hideki Nakayama NAI 58 1 0 02 Feb 2025
Conversational Text Extraction with Large Language Models Using Retrieval-Augmented Systems Soham Roy Mitul Goswami Nisharg Nargund Suneeta Mohanty Prasant Kumar Pattnaik RALM 56 0 0 20 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 86 24 0 20 Dec 2024
LLMs can Realize Combinatorial Creativity: Generating Creative Ideas via LLMs for Scientific Research Tianyang Gu Jingjin Wang Zhihao Zhang HaoHong Li LRM 85 2 0 18 Dec 2024
Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challenges Chandan K. Reddy Parshin Shojaee 75 5 0 16 Dec 2024
Inference Scaling fLaws: The Limits of LLM Resampling with Imperfect Verifiers Benedikt Stroebl Sayash Kapoor Arvind Narayanan LRM 87 13 0 26 Nov 2024
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically Kefan Dong Arvind V. Mahankali Tengyu Ma ReLM LRM 30 6 0 04 Nov 2024
Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation Chenyang An Shima Imani Feng Yao Chengyu Dong Ali Abbasi ... Samuel Buss Jingbo Shang Gayathri Mahalingam Pramod Sharma Maurice Diesendruck LRM 31 1 0 30 Oct 2024
Assured Automatic Programming via Large Language Models Martin Mirchev Andreea Costea Abhishek Kr Singh Abhik Roychoudhury 35 1 0 24 Oct 2024
ZIP-FIT: Embedding-Free Data Selection via Compression-Based Alignment Elyas Obbad Iddah Mlauzi Brando Miranda Rylan Schaeffer Kamal Obbad Suhana Bedi Sanmi Koyejo CVBM 60 0 0 23 Oct 2024
Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence İlker Işık R. G. Cinbis Ebru Aydin Gol 36 0 0 22 Oct 2024
Learning Mathematical Rules with Large Language Models Antoine Gorceix Bastien Le Chenadec Ahmad Rammal N. Vadori Manuela Veloso 23 1 0 22 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 Brando Miranda Clark W. Barrett Sanmi Koyejo 46 4 0 21 Oct 2024
Automated Proof Generation for Rust Code via Self-Evolution Tianyu Chen Shuai Lu Shan Lu Y. Gong Chenyuan Yang ... Peng Cheng Fan Yang Shuvendu Lahiri Tao Xie Lidong Zhou 49 8 0 21 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 45 0 0 21 Oct 2024
Think Thrice Before You Act: Progressive Thought Refinement in Large Language Models Chengyu Du Jinyi Han Yizhou Ying Aili Chen Qianyu He ... Haoran Guo Jiaqing Liang Zulong Chen Liangyue Li Yanghua Xiao KELM CLL LRM 30 1 0 17 Oct 2024
Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning Matthew Ho Vincent Zhu Xiaoyin Chen Moksh Jain Nikolay Malkin Edwin Zhang LRM 37 4 0 17 Oct 2024
Chain of Ideas: Revolutionizing Research Via Novel Idea Development with LLM Agents Long Li Weiwen Xu Jiayan Guo Ruochen Zhao Xingxuan Li ... Ronghao Dang Deli Zhao Yu Rong Tian Feng Lidong Bing LRM AI4CE 39 20 0 17 Oct 2024
FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware Minwoo Kang Mingjie Liu Ghaith Bany Hamad Syed Suhaib Haoxing Ren LRM 31 2 0 15 Oct 2024
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes Sean Lamont Christian J. Walder Amir Dezfouli Paul Montague Michael Norrish 31 0 0 14 Oct 2024
FB-Bench: A Fine-Grained Multi-Task Benchmark for Evaluating LLMs' Responsiveness to Human Feedback Heng Chang Miao Zheng Fan Yang Guosheng Dong Bin Cui Xin Wu Zenan Zhou Wentao Zhang ALM 51 6 0 12 Oct 2024
Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks Rushang Karia Daniel Bramblett D. Dobhal Siddharth Srivastava ELM LRM 35 0 0 11 Oct 2024