Research map / Large language models / Agents, code and math
Formal verification and proof data
Synthesize proof data and use autoformalization and Lean to verify LLM mathematical reasoning.
25 accepted papers at ICML, NeurIPS, ICLR, CVPR and AAAI (2022–2026) · an approach in Agents, code and math, keyword cluster “theorem · proof · proving”
State History Tried Checklist Preprints Who Export
Where it stands
Not enough benchmark data Fewer than four papers report the same benchmark, so there is no record to follow.
5 papers in 2023–24 and 19 in 2025–26 (at ICML, NeurIPS, ICLR, CVPR and AAAI); its share of the topic held steady, from 1.4% to 1.5%.
How this is decided
A benchmark is tracked when at least four papers of this approach report their own method on the same dataset and metric in at least two different years. Its record is the best number reported up to 2024 compared with the best reported in 2025–26: still improving means at least 1% better, flat means at most 0.2% better with at least two papers from 2025–26 trying. Numbers on a different scale from the rest (a fraction among percentages) and far outliers are left out. Results come from different papers with different setups, so they are signals, not head-to-head comparisons. The share of papers is counted at ICML, NeurIPS, ICLR, CVPR and AAAI.
How it got here
Most cited paper of each year
- 2022 · Autoformalization with Large Language Models (NeurIPS 2022 · 42 citations)
- 2023 · Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples (NeurIPS 2023 · 16 citations)
- 2024 · Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization (ICLR 2024 · 3 citations)
- 2025 · Learning Theorem Rationale for Improving the Mathematical Reasoning Capability of Large Language Models (AAAI 2025 · 2 citations)
- 2026 · BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs (ICML 2026 · 3 citations)
Earliest papers here
- Autoformalization with Large Language Models (NeurIPS 2022 · 42 citations)
- Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples (NeurIPS 2023 · 16 citations)
- Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization (ICLR 2024 · 3 citations)
What has been tried
12 papers here report 134 measured changes (a component added, removed or swapped, compared with a baseline): helped 70%, no clear effect 12%, hurt 14%, mixed 4%. Papers mostly publish changes that helped, so "helped" is over-represented.
Ablations in recent papers
| What was changed | Measured on | Result | Effect | Paper |
|---|---|---|---|---|
| add formal solution sketches | MATH Number Theory · problem solve rate | 29.2% -> 31.9% | Helped | Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization (ICLR 2024 · 3 citations) |
| Use TR-only training data instead of CoT-only data | GSM8k · accuracy | 61.1 -> 74.7 | Helped | Learning Theorem Rationale for Improving the Mathematical Reasoning Capability of Large Language Models (AAAI 2025 · 2 citations) |
| Add Syntax Refiner | miniF2F-test · accuracy | 7.0% -> 7.4% | Helped | APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · 2 citations) |
| Use log combination instead of linear or quadratic combination | MATH and miniF2F · autoformalization accuracy | Helped | Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · 2 citations) | |
| Add a prompt encouraging reasoning by examples | CounterMath · F1 (macro) | 38.3 -> 39.4 | Helped | One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs (ICML 2025 · 1 citation) |
| Add scaling tactics | ChenNEQ · problems proved | 3 out of 41 -> 39 out of 41 | Helped | Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning (ICLR 2025 · 0 citations) |
| Add 1 prover-feedback correction | Theorem proving, elementary, 1 seed concept · pass@1 | 26.0 -> 48.0 (+22.0) | Helped | MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · 0 citations) |
What reviewers will expect
Datasets and baselines named in the 8 papers of this approach from 2025–2026 that have a full-text summary. Leaving out the common ones is a frequent review question.
Datasets
- ProofNet · 2 of 8 papers
Baselines
- GPT-4o · 3 of 8 papers
- o3-mini · 3 of 8 papers
- OpenAI o1-preview · 2 of 8 papers
- Deepseek-R1 · 2 of 8 papers
- Gemini2.5-pro · 2 of 8 papers
- o1 · 2 of 8 papers
- o4-mini · 2 of 8 papers
Recent preprints
Loading recent arXiv preprints…
Who publishes on it
Institutions on the most papers of this approach since 2023 (of 24 papers; from OpenAlex and the papers' affiliations).
- Huawei · 4 papers
- Sun Yat-sen University · 3 papers
- City University of Hong Kong · 2 papers
- University of Edinburgh · 2 papers
- Peking University · 2 papers
- The Chinese University of Hong Kong · 2 papers
Use it
Download BibTeX of 22 key papersOpen the topic in the interactive map
Get alerts. Describe your idea in scime atlas and save it (free scime account): you get a weekly email when new preprints land close to it.
Related approaches
Same keyword cluster
- Retrieval-augmented formal theorem proving (62 papers)
Elsewhere in the topic
- Mathematical and structural reasoning benchmarks (304 papers)
- Agent instruction-following benchmarks (176 papers)
- Inductive and abstract reasoning evaluation (158 papers)
- Long-horizon LLM agents (155 papers)
- LLMs for optimization and heuristics (147 papers)
- Software engineering agents (140 papers)
- LLMs for scientific discovery (100 papers)
- Code generation benchmarks (96 papers)
Benchmark numbers, ablations and baseline numbers are extracted by AI from each paper's full text and can be wrong; the paper is the authority. Data: results index of 2026-11-02, citation counts from OpenAlex (2026-10-09).