LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

27 June 2023

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

50 / 150 papers shown

Title
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
LeanAgent: Lifelong Learning for Formal Theorem Proving Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao Anima Anandkumar CLL LLMAG LRM 74 8 0 08 Oct 2024
ImProver: Agent-Based Automated Proof Optimization Riyaz Ahuja Jeremy Avigad Prasad Tetali Sean Welleck LLMAG 42 2 0 07 Oct 2024
Consistent Autoformalization for Constructing Mathematical Libraries Lan Zhang Xin Quan André Freitas AI4CE 43 2 0 05 Oct 2024
Easy2Hard-Bench: Standardized Difficulty Labels for Profiling LLM Performance and Generalization Mucong Ding Chenghao Deng Jocelyn Choo Zichu Wu Aakriti Agrawal ... Dinesh Manocha Tom Goldstein John Langford Anima Anandkumar Furong Huang 64 5 0 27 Sep 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 36 1 0 23 Sep 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 46 36 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 37 7 0 19 Sep 2024
Great Memory, Shallow Reasoning: Limits of $k$ NN-LMs Shangyi Geng Wenting Zhao Alexander M. Rush RALM ReLM LRM 34 1 0 21 Aug 2024
KAN 2.0: Kolmogorov-Arnold Networks Meet Science Ziming Liu Pingchuan Ma Yixuan Wang Wojciech Matusik Max Tegmark 48 62 0 19 Aug 2024
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning Alex Sanchez-Stern Abhishek Varghese Zhanna Kaufman Dylan Zhang Talia Ringer Yuriy Brun 26 2 0 17 Aug 2024
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search Huajian Xin Z. Z. Ren Junxiao Song Zhihong Shao Wanjia Zhao ... Dejian Yang Zhibin Gou Z. F. Wu Fuli Luo Chong Ruan AIMat LRM 50 55 0 15 Aug 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 73 8 0 05 Aug 2024
Mission Impossible: A Statistical Perspective on Jailbreaking LLMs Jingtong Su Mingyu Lee SangKeun Lee 46 8 0 02 Aug 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Zijian Wu Jiayu Wang Dahua Lin Kai-xiang Chen 32 13 0 24 Jul 2024
Retrieval-Enhanced Machine Learning: Synthesis and Opportunities To Eun Kim Alireza Salemi Andrew Drozdov Fernando Diaz Hamed Zamani 58 7 0 17 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 47 19 0 15 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 75 26 0 14 Jul 2024
Solving General Natural-Language-Description Optimization Problems with Large Language Models Jihai Zhang Wei Wang Siyan Guo Li Wang Fangquan Lin Cheng Yang Wotao Yin 43 8 0 09 Jul 2024
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent Mahdi Buali Robert Hoehndorf 47 0 0 05 Jul 2024
Learning Formal Mathematics From Intrinsic Motivation Gabriel Poesia David Broman Nick Haber Noah D. Goodman LRM 43 11 0 30 Jun 2024
Towards Large Language Model Aided Program Refinement YuFan Cai Zhe Hou Xiaokun Luan David Miguel Sanan Baena Yun Lin Jun Sun Jin Song Dong 46 4 0 26 Jun 2024
From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models Sean Welleck Amanda Bertsch Matthew Finlayson Hailey Schoelkopf Alex Xie Graham Neubig Ilia Kulikov Zaid Harchaoui 35 51 0 24 Jun 2024
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods George Granberry Wolfgang Ahrendt Moa Johansson 39 2 0 21 Jun 2024
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving Xiaohan Lin Qingxing Cao Yinya Huang Haiming Wang Jianqiao Lu Zhengying Liu Linqi Song Xiaodan Liang LRM 44 6 0 20 Jun 2024
Proving Olympiad Algebraic Inequalities without Human Demonstrations Chenrui Wei Mengzhou Sun Wei Wang LRM 50 8 0 20 Jun 2024
miniCodeProps: a Minimal Benchmark for Proving Code Properties Evan Lohn Sean Welleck 40 3 0 16 Jun 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 79 8 0 08 Jun 2024
RATT: A Thought Structure for Coherent and Correct LLM Reasoning Jinghan Zhang Xiting Wang Weijieying Ren Lu Jiang Dongjie Wang Kunpeng Liu LRM 36 9 0 04 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 45 16 0 04 Jun 2024
Autoformalizing Euclidean Geometry Logan Murphy Kaiyu Yang Jialiang Sun Zhaoyu Li A. Anandkumar Xujie Si 44 4 0 27 May 2024
Empowering Large Language Models to Set up a Knowledge Retrieval Indexer via Self-Learning Xun Liang Pengnian Qi Zhiyu Li Sensen Zhang Shichao Song Hanyu Wang Jiawei Yang Zhiyu Li Simin Niu Chenyang Xi RALM 35 6 0 27 May 2024
Models That Prove Their Own Correctness Noga Amit S. Goldwasser Orr Paradise G. Rothblum LRM 44 2 0 24 May 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 43 12 0 23 May 2024
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data Huajian Xin Daya Guo Zhihong Shao Z. Z. Ren Qihao Zhu Bo Liu Chong Ruan Wenda Li Xiaodan Liang SyDa 45 64 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 38 5 0 13 May 2024
ATG: Benchmarking Automated Theorem Generation for Generative Language Models Xiaohan Lin Qingxing Cao Yinya Huang Zhicheng YANG Zhengying Liu Zhenguo Li Xiaodan Liang 26 4 0 05 May 2024
Generating Probabilistic Scenario Programs from Natural Language Karim Elmaaroufi Devan Shankar Ana Cismaru Marcell Vazquez-Chanlatte Alberto L. Sangiovanni-Vincentelli Matei A. Zaharia S. Seshia 40 7 0 03 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 48 15 0 03 May 2024
Towards Green AI: Current status and future research Christian Clemm Lutz Stobbe Kishan Wimalawarne Jan Druschke 51 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 47 15 0 29 Apr 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 42 25 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 56 22 0 15 Apr 2024
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving Chenyang An Zhibo Chen Qihao Ye Emily First Letian Peng Jiayun Zhang Zihan Wang Sorin Lerner Jingbo Shang LRM 42 7 0 10 Apr 2024
LeanReasoner: Boosting Complex Logical Reasoning with Lean Dongwei Jiang Marcio Fonseca Shay B. Cohen LRM 36 14 0 20 Mar 2024
StateFlow: Enhancing LLM Task-Solving through State-Driven Workflows Yiran Wu Tianwei Yue Shaokun Zhang Chi Wang Qingyun Wu 48 21 0 17 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 40 4 0 06 Mar 2024