Title
Improving Autoformalization Using Direct Dependency Retrieval Shaoqi Wang Lu Yu Chunjie Yang 53 0 0 15 Nov 2025
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels Jiedong Jiang Wanyi He Yuefeng Wang Guoxiong Gao Yongle Hu ... Nailing Guan Peihao Wu Chunbo Dai Liang Xiao Bin Dong AIMat ELM LRM 278 0 0 04 Nov 2025
RLMEval: Evaluating Research-Level Neural Theorem Proving Auguste Poiroux Antoine Bosselut Viktor Kuncak AIMat OffRL 256 0 0 29 Oct 2025
ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization Guoxin Chen Jing Wu Xinjie Chen Wayne Xin Zhao Ruihua Song Chengxi Li Kai Fan Dayiheng Liu Minpeng Liao AIMat OffRL 251 0 0 28 Oct 2025
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings Prithwish Jana Kaan Kale Ahmet Ege Tanriverdi Cruise Song S. Vishwanath Vijay Ganesh AIMat 268 0 0 17 Oct 2025
GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving Ruida Wang Jiarui Yao Rui Pan Shizhe Diao Tong Zhang 59 0 0 13 Oct 2025
Trustworthy Retrosynthesis: Eliminating Hallucinations with a Diverse Ensemble of Reaction Scorers Michal Sadowski Maria Wyrzykowska Lukasz Sztukiewicz Tadija Radusinović Jan Rzymkowski Paweł Włodarczyk-Pruszyński Mikołaj Sacha Piotr Kozakowski Ruard van Workum Stanislaw Jastrzebski 76 0 0 12 Oct 2025
DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems Meiru Zhang Philipp Borchert Milan Gritta Gerasimos Lampouras AIMat 375 0 0 12 Oct 2025
MASA: LLM-Driven Multi-Agent Systems for Autoformalization Lan Zhang Marco Valentino André Freitas LLMAG AI4CE 64 0 0 10 Oct 2025
Lean Finder: Semantic Search for Mathlib That Understands User Intents Jialin Lu Kye Emond Kaiyu Yang Swarat Chaudhuri Weiran Sun Wuyang Chen 90 2 0 08 Oct 2025
Benchmarking Foundation Models with Retrieval-Augmented Generation in Olympic-Level Physics Problem Solving Shunfeng Zheng Yudi Zhang Meng Fang Zihan Zhang Zhitan Wu Mykola Pechenizkiy Ling-Hao Chen ReLM RALM LRM 176 0 0 01 Oct 2025
Aristotle: IMO-level Automated Theorem Proving Tudor Achim Alex Best Kevin Der Mathïs Fédérico Sergei Gukov ... Matyas Tamas Vlad Tenev Jonathan Thomm Harold Williams Lawrence Wu LRM 114 2 0 01 Oct 2025
A benchmark for vericoding: formally verified program synthesis Sergiu Bursuc Theodore Ehrenborg Shaowei Lin Lacramioara Astefanoaei Ionel Emilian Chiosa ... Adem Bizid Quinn Dougherty Miranda Zhao Max Tan Max Tegmark 56 1 0 26 Sep 2025
Hilbert: Recursively Building Formal Proofs with Informal Reasoning Sumanth Varambally Thomas Voice Yanchao Sun Zhifeng Chen Rose Yu Ke Ye AIMat ReLM LRM 165 7 0 26 Sep 2025
FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory Xiao-Wen Yang Zihao Zhang Jianuo Cao Zhi Zhou Zenan Li Lan-Zhe Guo Yuan Yao Taolue Chen Yu-Feng Li Xiaoxing Ma ALM LRM 92 1 0 26 Sep 2025
EngiBench: A Benchmark for Evaluating Large Language Models on Engineering Problem Solving Xiyuan Zhou Xinlei Wang Yirui He Yang Wu Ruixi Zou ... Wenxuan Liu Huan Zhao Yan Xu Jinjin Gu Junhua Zhao ELM LRM 72 1 0 22 Sep 2025
Deploying AI for Signal Processing education: Selected challenges and intriguing opportunities Jarvis Haupt Qin Lu Yanning Shen Jia Chen Yue Dong Dan McCreary Mehmet Akçakaya G. Giannakis 101 0 0 10 Sep 2025
Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure Seiji Hattori Takuya Matsuzaki Makoto Fujiwara 40 0 0 10 Sep 2025
Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers Ran Xin Zeyu Zheng Yanchen Nie Kun Yuan Xia Xiao OffRL LRM 138 2 0 08 Sep 2025
Towards Repository-Level Program Verification with Large Language Models Si Cheng Zhong Xujie Si ALM 53 1 0 31 Aug 2025
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants Barış Bayazıt Yao Li Xujie Si 52 1 0 26 Aug 2025
Automated Formalization via Conceptual Retrieval-Augmented LLMs Wangyue Lu Lun Du Sirui Li Ke Weng Haozhe Sun Hengyu Liu Minghe Yu Tiancheng Zhang Ge Yu 120 3 0 09 Aug 2025
Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction Yong Lin Shange Tang Bohan Lyu Ziran Yang Jui-Hui Chung ... Hongzhou Lin Yejin Choi Danqi Chen Sanjeev Arora Chi Jin MoE LRM 130 35 0 05 Aug 2025
Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs Aryan Gulati Brando Miranda Eric Chen Emily Xia Kai Fronsdal Bruno Dumont Elyas Obbad Sanmi Koyejo AIMat ReLM LRM 278 5 0 05 Aug 2025
The SMeL Test: A simple benchmark for media literacy in language models Gustaf Ahdritz Anat Kleiman 173 0 0 04 Aug 2025
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving L. Chen J. Gu Daigang Xu Wenhao Huang Z. L. Jiang ... Ge Zhang Tianyun Zhao Jianqiu Zhao Yichi Zhou Thomas Hanwen Zhu AIMat LRM 182 28 0 31 Jul 2025
Solving Formal Math Problems by Decomposition and Iterative Reflection Yichi Zhou Jianqiu Zhao Yongxin Zhang Bohan Wang Siran Wang ... Rong Ye Phan Nhat Hoang Huishuai Zhang Peng Sun Hang Li 111 13 0 21 Jul 2025
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4 Matěj Kripner Michal Šustr Milan Straka LRM 140 1 0 19 Jul 2025
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs Kaito Baba Chaoran Liu Shuhei Kurita Akiyoshi Sannai LLMAG 276 9 0 24 Jun 2025
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving Chuxue Cao Mengze Li Juntao Dai Jinluan Yang Zijian Zhao Shengyu Zhang Weijie Shi Chengzhong Liu Sirui Han Wenhan Luo LRM 124 3 0 20 Jun 2025
AlphaEvolve: A coding agent for scientific and algorithmic discovery Alexander Novikov Ngan Vu Marvin Eisenberger Emilien Dupont Po-Sen Huang ... George Holland Alex Davies Sebastian Nowozin Pushmeet Kohli Matej Balog 204 166 0 16 Jun 2025
Domain Specific Benchmarks for Evaluating Multimodal Large Language Models Khizar Anjuma Muhammad Arbab Arshad Kadhim Hayawi Efstathios Polyzos A. Tariq ... Nishith Reddy Mannuru Ravi Varma Kumar Bevara Taslim Mahbub Muhammad Zeeshan Akram Sakib Shahriar ELM LRM 300 2 0 15 Jun 2025
Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning Lan Zhang Marco Valentino André Freitas 228 0 0 12 Jun 2025
A Survey on Large Language Models for Mathematical Reasoning Peng-Yuan Wang Tian-Shuo Liu Chenyang Wang Yi-Di Wang Shu Yan ... Xu-Hui Liu Xin-Wei Chen Jia-Cheng Xu Ziniu Li Yang Yu LRM 184 13 0 10 Jun 2025
LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs Manooshree Patel Rayna Bhattacharyya Thomas Lu Arnav Mehta Niels Voss Narges Norouzi Gireeja Ranade 165 1 0 10 Jun 2025
Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models Daniel Koh Yannic Noller C. Păsăreanu Adrians Skapars Youcheng Sun 151 0 0 09 Jun 2025
Premise Selection for a Lean Hammer Thomas Zhu Joshua Clune Jeremy Avigad Albert Qiaochu Jiang Sean Welleck 133 2 0 09 Jun 2025
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems? Zhitao He Zongwei Lyu Dazhong Chen Dadi Guo Yi R. Fung LRM 184 5 0 06 Jun 2025
LeanExplore: A search engine for Lean 4 declarations Justin Asher 112 1 0 04 Jun 2025
Using Reasoning Models to Generate Search Heuristics that Solve Open Instances of Combinatorial Design Problems Christopher D. Rosin LRM 148 2 0 29 May 2025
DINGO: Constrained Inference for Diffusion LLMs Tarun Suresh Debangshu Banerjee Shubham Ugare Sasa Misailovic Gagandeep Singh DiffM 156 3 0 29 May 2025
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Nikita Khramov Nikita Khramov Gleb Solovev Anton Podkopaev 171 1 0 28 May 2025
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement Jilin Hu Jianyu Zhang Yongwang Zhao Talia Ringer 129 2 0 21 May 2025
Generalizable Process Reward Models via Formally Verified Training Data Ryo Kamoi Yusen Zhang Nan Zhang Sarkar Snigdha Sarathi Das Rui Zhang OffRL LRM 212 2 0 21 May 2025
Pass@K Policy Optimization: Solving Harder Reinforcement Learning Problems Christian Walder Deep Karkhanis OffRL 255 16 0 21 May 2025
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 418 8 0 20 May 2025
FOL-Traces: Verified First-Order Logic Reasoning Traces at Scale Isabelle Lee Sarah Liaw Dani Yogatama OffRL LRM 147 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 303 5 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 229 1 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 247 8 0 16 May 2025