mlsanityData to 7 Oct 2026

Process-Driven Autoformalization in Lean 4

arXiv 2406.01940 ↗First posted 4 Jun 2024cs.CL cs.LG cs.LOcited by 45

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing efforts are limited to formal languages with substantial online corpora and struggle to keep pace with rapidly evolving languages like Lean 4. To bridge this gap, we propose a new benchmark Formalization for Lean~4 (name) designed to evaluate the autoformalization capabilities of large language models (LLMs). This benchmark encompasses a comprehensive assessment of questions, answers, formal statements, and proofs. Additionally, we introduce a Process-Supervised Verifier (PSV) model that leverages the precise feedback from Lean 4 compilers to enhance autoformalization. Our experiments demonstrate that the PSV method improves autoformalization, enabling higher accuracy using less filtered training data. Furthermore, when fine-tuned with data containing detailed process information, PSV can leverage the data more effectively, leading to more significant improvements in autoformalization for Lean 4. Our dataset and code are available at urlhttps://github.com/rookie-joe/PDA.

Key facts. Cited by 45 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 56 of its 82 references that are in the map. First posted on arXiv 4 Jun 2024.

Builds on

56 of 82 references.

Closest ancestors · 6

Same direction, newest first

  1. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data14 Feb
  2. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning9 Feb
  3. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models5 Feb
  4. 2023Llemma: An Open Language Model For Mathematics16 Oct
  5. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models16 Oct
  6. 2023Scaling Relationship on Learning Mathematical Reasoning with Large Language Models3 Aug

Other references · 50

  1. 2023GPT-4 Technical Reportcited by 18,132
  2. 2022Training language models to follow instructions with human feedbackcited by 15,712
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  4. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  5. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  6. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  7. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,601
  8. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  9. 2022Large Language Models are Zero-Shot Reasonerscited by 4,323
  10. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  11. 2023Let's Verify Step by Stepcited by 3,598
  12. 2023Self-Refine: Iterative Refinement with Self-Feedbackcited by 3,317
38 more
  1. 2023Mistral 7Bcited by 3,065
  2. 2022Constitutional AI: Harmlessness from AI Feedbackcited by 2,950
  3. 2022Large Language Models Are Human-Level Prompt Engineerscited by 1,020
  4. 2023Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotationscited by 895
  5. 2022Solving math word problems with process- and outcome-based feedbackcited by 871
  6. 2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 751
  7. 2023Textbooks Are All You Needcited by 561
  8. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  9. 2023Fine-Grained Human Feedback Gives Better Rewards for Language Model Trainingcited by 399
  10. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  11. 2023Orca: Progressive Learning from Complex Explanation Traces of GPT-4cited by 369
  12. 2021Recursively Summarizing Books with Human Feedbackcited by 287
  13. 2022RARR: Researching and Revising What Language Models Say, Using Language Modelscited by 286
  14. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  15. 2022Generating Sequences by Learning to Self-Correctcited by 271
  16. 2022Autoformalization with Large Language Modelscited by 252
  17. 2022Making Large Language Models Better Reasoners with Step-Aware Verifiercited by 231
  18. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  19. 2022The Unreliability of Explanations in Few-shot Prompting for Textual Reasoningcited by 169
  20. 2022Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanationscited by 159
  21. 2022UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expressioncited by 137
  22. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  23. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  24. 2023Large Language Models as Analogical Reasonerscited by 107
  25. 2023Let's reward step by step: Step-Level reward model as the Navigators for Reasoningcited by 96
  26. 2023Improving Language Models via Plug-and-Play Retrieval Feedbackcited by 87
  27. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  28. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 52
  29. 2024Multi-step Problem Solving Through a Verifier: An Empirical Analysis on Model-induced Process Supervisioncited by 51
  30. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  31. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  32. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  33. 2023Multilingual Mathematical Autoformalizationcited by 38
  34. 2024Learning From Correctness Without Prompting Makes LLM Efficient Reasonercited by 15
  35. 2023MLFMF: Data Sets for Machine Learning for Mathematical Formalizationcited by 10
  36. 2024YODA: Teacher-Student Progressive Learning for Language Modelscited by 10
  37. 2019Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programmingcited by 1
  38. 2020Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languagescited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 6; 2025: 20; 2026: 19.

45 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  2. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  3. 2024OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modelingcited by 66
  4. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  5. 2024MR-Ben: A Meta-Reasoning Benchmark for Evaluating System-2 Thinking in LLMscited by 30
  6. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  7. 2024Reliable Evaluation and Benchmarks for Statement Autoformalizationcited by 25
  8. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  9. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 20
  10. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  11. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  12. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
33 more
  1. 2025Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verificationcited by 16
  2. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 16
  3. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15
  4. 2025Theorem Prover as a Judge for Synthetic Data Generationcited by 13
  5. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  6. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 9
  7. 2025Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Provingcited by 8
  8. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 8
  9. 2025Towards a Common Framework for Autoformalizationcited by 7
  10. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  11. 2025Diverse Inference and Verification for Advanced Reasoningcited by 6
  12. 2026Faithful Autoformalization via Roundtrip Verification and Repaircited by 6
  13. 2026Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalizationcited by 4
  14. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematicscited by 4
  15. 2025Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairscited by 3
  16. 2026Theory-Scale Auto-Formalization of Logics for Computer Sciencecited by 3
  17. 2026Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Provingcited by 2
  18. 2026FormalRx: Rectify and eXamine Semantic Failures in Autoformalizationcited by 2
  19. 2026SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalizationcited by 2
  20. 2025Hierarchical Attention Generates Better Proofscited by 1
  21. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generationcited by 1
  22. 2025Conjecturing: An Overlooked Step in Formal Mathematical Reasoningcited by 1
  23. 2026Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discoverycited by 1
  24. 2026The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalizationcited by 1
  25. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  26. 2026Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchycited by 0
  27. 2026Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalizationcited by 0
  28. 2026CAM-Bench: A Benchmark for Computational and Applied Mathematics in Leancited by 0
  29. 2026FVSpec: Real-World Property-Based Tests as Lean Challengescited by 0
  30. 2026Human agency in initial human-AI proof formalization workflowscited by 0
  31. 2026Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Searchcited by 0
  32. 2026From Atomic to Agentic: Towards Interpretable Evaluation of LLMs' Agentic Mathematical Capabilitiescited by 0
  33. 2026Sage: Formalization with Semantic Correctioncited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning
  2. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
  3. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
  4. 2025FMC: Formalization of Natural Language Mathematical Competition Problems
  5. 2025Autoformalization in the Era of Large Language Models: A Survey
  6. 2024Herald: A Natural Language Annotated Lean 4 Dataset
  7. 2025Autoformalizer with Tool Feedback
  8. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency