mlsanityData to 14 Oct 2026

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

arXiv 2507.06181 ↗First posted 8 Jul 2025cs.CLcited by 16

On the map: Deep reinforcement learning methods → RL training of language and agent models

Abstract (arXiv)

Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving. While prior work has focused on generation and compilation success, little attention has been paid to the critic phase-the evaluation of whether generated formalizations truly capture the semantic intent of the original problem. In this paper, we introduce CriticLean, a novel critic-guided reinforcement learning framework that elevates the role of the critic from a passive validator to an active learning component. Specifically, first, we propose the CriticLeanGPT, trained via supervised fine-tuning and reinforcement learning, to rigorously assess the semantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench, a benchmark designed to measure models' ability to distinguish semantically correct from incorrect formalizations, and demonstrate that our trained CriticLeanGPT models can significantly outperform strong open- and closed-source baselines. Building on the CriticLean framework, we construct FineLeanCorpus, a dataset comprising over 285K problems that exhibits rich domain diversity, broad difficulty coverage, and high correctness based on human evaluation. Overall, our findings highlight that optimizing the critic phase is essential for producing reliable formalizations, and we hope our CriticLean will provide valuable insights for future advances in formal mathematical reasoning.

Key facts. Cited by 16 papers in the map (data through 14 Oct 2026). Placed in RL training of language and agent models, one of 15 directions in Deep reinforcement learning methods. Builds on 53 of its 84 references that are in the map. First posted on arXiv 8 Jul 2025.

Builds on

53 of 84 references.

Closest ancestors · 2

Same direction, newest first

  1. 2025Reinforcement Learning Optimization for Large-Scale Learning: An Efficient and User-Friendly Scaling Library6 Jun
  2. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search15 Aug

Other references · 51

  1. 2024The Llama 3 Herd of Modelscited by 14,715
  2. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  3. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
  4. 2023Judging LLM-as-a-Judge with MT-Bench and Chatbot Arenacited by 8,626
  5. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,944
  6. 2023Qwen Technical Reportcited by 3,344
  7. 2025DAPO: An Open-Source LLM Reinforcement Learning System at Scalecited by 2,810
  8. 2024HybridFlow: A Flexible and Efficient RLHF Frameworkcited by 2,057
  9. 2024LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Modelscited by 1,464
  10. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  11. 2025s1: Simple test-time scalingcited by 1,341
  12. 2024Qwen2.5-Coder Technical Reportcited by 1,203
38 more
  1. 2024OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problemscited by 1,136
  2. 2023LIMA: Less Is More for Alignmentcited by 1,100
  3. 2025Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?cited by 982
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  5. 2025Seed1.5-VL Technical Reportcited by 373
  6. 2025Reinforcement Learning for Reasoning in Large Language Models with One Training Examplecited by 295
  7. 2025VAPO: Efficient and Reliable Reinforcement Learning for Advanced Reasoning Taskscited by 285
  8. 2024Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Modelscited by 284
  9. 2025DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoningcited by 280
  10. 2022Autoformalization with Large Language Modelscited by 263
  11. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  12. 2025ProRL: Prolonged Reinforcement Learning Expands Reasoning Boundaries in Large Language Modelscited by 194
  13. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  14. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  15. 2024LLaVA-Critic: Learning to Evaluate Multimodal Modelscited by 134
  16. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  17. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  18. 2025A Comprehensive Survey on Long Context Language Modelingcited by 117
  19. 2024CriticBench: Benchmarking LLMs for Critique-Correct Reasoningcited by 88
  20. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 81
  21. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  22. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  23. 2023Reinforcement Learning with Human Feedback: Learning Dynamic Choices via Pessimismcited by 69
  24. 2024MAP-Neo: Highly Capable and Transparent Bilingual Large Language Model Seriescited by 67
  25. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 55
  26. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 48
  27. 2024Process-Driven Autoformalization in Lean 4cited by 45
  28. 2025Can Large Language Models Detect Errors in Long Chain-of-Thought Reasoning?cited by 44
  29. 2024HARDMath: A Benchmark Dataset for Challenging Problems in Applied Mathematicscited by 32
  30. 2025Leveraging Online Olympiad-Level Math Problems for LLMs Training and Contamination-Resistant Evaluationcited by 29
  31. 2024DDK: Distilling Domain Knowledge for Efficient Large Language Modelscited by 26
  32. 2024U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMscited by 24
  33. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learningcited by 24
  34. 2024M2rc-Eval: Massively Multilingual Repository-level Code Completion Evaluationcited by 21
  35. 2025Think-J: Learning to Think for Generative LLM-as-a-Judgecited by 21
  36. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  37. 2025CodeCriticBench: A Holistic Code Critique Benchmark for Large Language Modelscited by 14
  38. 2025Generating Symbolic World Models via Test-time Scaling of Large Language Modelscited by 12

50 most cited of 51 All 51 (JSON)

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 8; 2026: 8.

16 papers.

Sort:

By area:

  1. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 101
  2. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 44
  3. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 20
  4. 2025ReLook: Vision-Grounded RL with a Multimodal LLM Critic for Agentic Web Codingcited by 14
  5. 2026MerLean: An Agentic Framework for Autoformalization in Quantum Computationcited by 10
  6. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 7
  7. 2025MASA: LLM-Driven Multi-Agent Systems for Autoformalizationcited by 6
  8. 2026Reinforcement Learning for LLM-based Multi-Agent Systems through Orchestration Tracescited by 5
  9. 2025Conjecturing: An Overlooked Step in Formal Mathematical Reasoningcited by 2
  10. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  11. 2025Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Trainingcited by 1
  12. 2026GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learningcited by 1
4 more
  1. 2026FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalizationcited by 1
  2. 2026JURY-RL: Votes Propose, Proofs Dispose for Label-Free RLVRcited by 1
  3. 2026ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimizationcited by 0
  4. 2026AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harnesscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Theorem Prover as a Judge for Synthetic Data Generation
  2. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
  3. 2026FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
  4. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
  5. 2025Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection
  6. 2026PhysProver: Advancing Automatic Theorem Proving for Physics
  7. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
  8. 2026VERIFY-RL: Verifiable Recursive Decomposition for Reinforcement Learning in Mathematical Reasoning