Title
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 12 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 40 0 0 07 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 26 0 0 27 Apr 2025
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries Huajian Xin Luming Li Xiaoran Jin Jacques Fleuriot Wenda Li AIMat 48 0 0 27 Apr 2025
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification Balaji Rao William Eiers Carlo Lipizzi 22 0 0 23 Apr 2025
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning Haiming Wang Mert Unsal Xiaohan Lin Mantas Baksys J. Liu ... Zhouliang Yu Z. Wang Zhilin Yang Zhengying Liu Jia-Nan Li AIMat ReLM AI4TS LRM 49 4 0 15 Apr 2025
SkillWeaver: Web Agents can Self-Improve by Discovering and Honing Skills Boyuan Zheng Michael Y. Fatemi Xiaolong Jin Z. Wang Apurva Gandhi ... Yu Gu Jayanth Srinivasa Gaowen Liu Graham Neubig Yu Su CLL 29 0 0 09 Apr 2025
Lemmanaid: Neuro-Symbolic Lemma Conjecturing Yousef Alhessi Sólrún Halla Einarsdóttir George Granberry Emily First Moa Johansson Sorin Lerner Nicholas Smallbone 14 1 0 07 Apr 2025
Attention-Aware Multi-View Pedestrian Tracking Reef Alturki Adrian Hilton Jean-Yves Guillemaut 26 0 0 03 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 56 0 0 12 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 66 0 0 03 Mar 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 55 0 0 25 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 61 0 0 20 Feb 2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity Dylan Zhang Justin Wang Tianran Sun 36 0 0 17 Feb 2025
ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data Xiaoyang Liu Kangjie Bao Jiashuo Zhang Yunqi Liu Yu Chen Yuntian Liu Yang Jiao Tao Luo AIMat 50 0 0 08 Feb 2025
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation Quinn Dougherty Ronak Mehta ALM 49 0 0 08 Feb 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 77 20 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 96 1 0 18 Dec 2024
Inference Scaling fLaws: The Limits of LLM Resampling with Imperfect Verifiers Benedikt Stroebl Sayash Kapoor Arvind Narayanan LRM 80 6 0 26 Nov 2024
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically Kefan Dong Arvind V. Mahankali Tengyu Ma ReLM LRM 23 5 0 04 Nov 2024
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction Liao Zhang David M. Cerna C. Kaliszyk 18 0 0 02 Nov 2024
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency Zenan Li Yifan Wu Zhaoyu Li Xinming Wei Xian Zhang Fan Yang Xiaoxing Ma 30 2 0 28 Oct 2024
Library Learning Doesn't: The Curious Case of the Single-Use "Library" Ian Berlot-Attwell Frank Rudzicz Xujie Si 37 1 0 26 Oct 2024
Cobblestone: Iterative Automation for Formal Verification Saketh Ram Kasibatla Arpan Agarwal Yuriy Brun Sorin Lerner Talia Ringer Emily First 13 0 0 25 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 31 0 0 21 Oct 2024
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes Sean Lamont Christian J. Walder Amir Dezfouli Paul Montague Michael Norrish 12 0 0 14 Oct 2024
Mars: Situated Inductive Reasoning in an Open-World Environment Xiaojuan Tang Jiaqi Li Yitao Liang Song-chun Zhu Muhan Zhang Zilong Zheng LM&Ro LRM LLMAG 13 1 0 10 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 37 3 0 09 Oct 2024
Consistent Autoformalization for Constructing Mathematical Libraries Lan Zhang Xin Quan André Freitas AI4CE 22 2 0 05 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 25 7 0 19 Sep 2024
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving Xueliang Zhao Lin Zheng Haige Bo Changran Hu Urmish Thakker Lingpeng Kong LRM 37 1 0 20 Aug 2024
Benchmarking Large Language Models for Math Reasoning Tasks Kathrin Seßler Yao Rong Emek Gözlüklü Enkelejda Kasneci LRM 20 3 0 20 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 39 45 0 15 Aug 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Zijian Wu Jiayu Wang Dahua Lin Kai-xiang Chen 16 12 0 24 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 61 22 0 14 Jul 2024
GenArtist: Multimodal LLM as an Agent for Unified Image Generation and Editing Zhenyu Wang Aoxue Li Zhenguo Li Xihui Liu MLLM DiffM 30 25 0 08 Jul 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 33 4 0 20 Jun 2024
miniCodeProps: a Minimal Benchmark for Proving Code Properties Evan Lohn Sean Welleck 27 2 0 16 Jun 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 24 61 0 23 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 22 3 0 03 May 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 42 21 0 15 Apr 2024
Stepwise Self-Consistent Mathematical Reasoning with Large Language Models Zilong Zhao Yao Rong Dongyang Guo Emek Gözlüklü Emir Gülboy Enkelejda Kasneci LRM 18 3 0 24 Feb 2024
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data Yinya Huang Xiaohan Lin Zhengying Liu Qingxing Cao Huajian Xin Haiming Wang Zhenguo Li Linqi Song Xiaodan Liang ALM 23 16 0 14 Feb 2024
TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Tasks Zhiruo Wang Daniel Fried Graham Neubig 9 18 0 23 Jan 2024
Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challenges Qingyao Li Lingyue Fu Weiming Zhang Xianyu Chen Jingwei Yu Wei Xia Weinan Zhang Ruiming Tang Yong Yu AI4Ed ELM 20 16 0 27 Dec 2023
A Survey of Reasoning with Foundation Models Jiankai Sun Chuanyang Zheng E. Xie Zhengying Liu Ruihang Chu ... Xipeng Qiu Yi-Chen Guo Hui Xiong Qun Liu Zhenguo Li ReLM LRM AI4CE 14 74 0 17 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 11 15 0 16 Oct 2023
An In-Context Learning Agent for Formal Theorem-Proving Amitayush Thakur George Tsoukalas Yeming Wen Jimmy Xin Swarat Chaudhuri LLMAG 17 7 0 06 Oct 2023
MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models L. Yu Weisen Jiang Han Shi Jincheng Yu Zhengying Liu Yu Zhang James T. Kwok Zheng Li Adrian Weller Weiyang Liu OSLM LRM 26 317 0 21 Sep 2023
Generative Agents: Interactive Simulacra of Human Behavior J. Park Joseph C. O'Brien Carrie J. Cai Meredith Ringel Morris Percy Liang Michael S. Bernstein LM&Ro AI4CE 204 1,701 0 07 Apr 2023