LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

27 June 2023

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

44 / 44 papers shown

Title
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 45 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 54 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 W. R. Huang Yandong Wen Ge Zhang Weiyang Liu LRM 93 0 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 X. Li Jiahao Ying Yubo Ma ... Juanzi Li Aixin Sun Xuanjing Huang Tat-Seng Chua Yu Jiang ALM ELM 84 1 0 26 Apr 2025
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction Suozhi Huang Peiyang Song Robert Joseph George Anima Anandkumar AI4TS LRM 42 2 0 25 Feb 2025
Activation Steering in Neural Theorem Provers Shashank Kirtania LLMSV 126 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 107 0 0 20 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 121 9 0 05 Feb 2025
Advanced Weakly-Supervised Formula Exploration for Neuro-Symbolic Mathematical Reasoning Yuxuan Wu Hideki Nakayama NAI 53 0 0 02 Feb 2025
LLMs can Realize Combinatorial Creativity: Generating Creative Ideas via LLMs for Scientific Research Tianyang Gu Jingjin Wang Zhihao Zhang HaoHong Li LRM 77 1 0 18 Dec 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 48 0 0 23 Oct 2024
Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence İlker Işık R. G. Cinbis Ebru Aydin Gol 26 0 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 38 4 0 21 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 40 0 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 39 7 0 21 Oct 2024
FB-Bench: A Fine-Grained Multi-Task Benchmark for Evaluating LLMs' Responsiveness to Human Feedback Y. Li Miao Zheng Fan Yang Guosheng Dong Bin Cui Weipeng Chen Zenan Zhou Wentao Zhang ALM 32 5 0 12 Oct 2024
Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks Rushang Karia Daniel Bramblett D. Dobhal Siddharth Srivastava ELM LRM 30 0 0 11 Oct 2024
LeanAgent: Lifelong Learning for Formal Theorem Proving Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao Anima Anandkumar CLL LLMAG LRM 70 8 0 08 Oct 2024
Retrieval Augmented Generation (RAG) and Beyond: A Comprehensive Survey on How to Make your LLMs use External Data More Wisely Siyun Zhao Yuqing Yang Zilong Wang Zhiyuan He Luna Qiu Lili Qiu SyDa RALM 3DV 32 33 0 23 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 27 7 0 19 Sep 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 58 6 0 05 Aug 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 34 18 0 15 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 65 23 0 14 Jul 2024
Can I understand what I create? Self-Knowledge Evaluation of Large Language Models Zhiquan Tan Lai Wei Jindong Wang Xing Xie Weiran Huang ELM LRM 35 5 0 10 Jun 2024
SelfDefend: LLMs Can Defend Themselves against Jailbreaking in a Practical Manner Xunguang Wang Daoyuan Wu Zhenlan Ji Zongjie Li Pingchuan Ma Shuai Wang Yingjiu Li Yang Liu Ning Liu Juergen Rahmel AAML 71 8 0 08 Jun 2024
Proving Theorems Recursively Haiming Wang Huajian Xin Zhengying Liu Wenda Li Yinya Huang ... Zhicheng YANG Jing Tang Jian Yin Zhenguo Li Xiaodan Liang LRM 28 10 0 23 May 2024
HoneyBee: A Scalable Modular Framework for Creating Multimodal Oncology Datasets with Foundational Embedding Models Aakash Tripathi Asim Waqas Yasin Yilmaz Ghulam Rasool 32 5 0 13 May 2024
Towards Green AI: Current status and future research Christian Clemm Lutz Stobbe Kishan Wimalawarne Jan Druschke 43 2 0 01 May 2024
LLM-SR: Scientific Equation Discovery via Programming with Large Language Models Parshin Shojaee Kazem Meidani Shashank Gupta A. Farimani Chandan K. Reddy 37 15 0 29 Apr 2024
Hint-before-Solving Prompting: Guiding LLMs to Effectively Utilize Encoded Knowledge Jinlan Fu Shenzhen Huangfu Hang Yan See-Kiong Ng Xipeng Qiu LRM 38 7 0 22 Feb 2024
ChartX & ChartVLM: A Versatile Benchmark and Foundation Model for Complicated Chart Reasoning Renqiu Xia Bo-Wen Zhang Hancheng Ye Xiangchao Yan Qi Liu ... Min Dou Botian Shi Junchi Yan Junchi Yan Yu Qiao LRM 55 52 0 19 Feb 2024
Inherent limitations of LLMs regarding spatial information He Yan Xinyao Hu Xiangpeng Wan Chengyu Huang Kai Zou Shiqi Xu LRM 28 2 0 05 Dec 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 16 15 0 16 Oct 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 59 92 0 08 Mar 2023
Magnushammer: A Transformer-Based Approach to Premise Selection Maciej Mikuła Szymon Tworkowski Szymon Antoniak Bartosz Piotrowski Albert Qiaochu Jiang Jinyi Zhou Christian Szegedy Lukasz Kuciñski Piotr Milo's Yuhuai Wu 39 42 0 08 Mar 2023
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 63 157 0 21 Oct 2022
Training Language Models with Memory Augmentation Zexuan Zhong Tao Lei Danqi Chen RALM 232 127 0 25 May 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 108 156 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 73 115 0 03 Feb 2022
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning Yuhuai Wu M. Rabe Wenda Li Jimmy Ba Roger C. Grosse Christian Szegedy AIMat LRM 61 51 0 15 Jan 2021
Retrieval-Based Neural Code Generation Shirley Anugrah Hayati R. Olivier Pravalika Avvaru Pengcheng Yin A. Tomasic Graham Neubig 129 110 0 29 Aug 2018