PaperlayerView exact revision on arXiv

Source-linked AI summary

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, Ge Zhang

arXiv:2507.06181v1cs.CL

TL;DR

Natural-language mathematical statements are difficult to translate into formal code that preserves semantic intent, and prior work has emphasized generation and compilation more than critic evaluation. CriticLean trains a critic-guided reinforcement-learning framework and builds a benchmark and dataset around semantic fidelity. Its trained critics outperform strong open-source and many closed-source baselines, while the pipeline’s success remains constrained by the base formalizer’s ability to produce acceptable candidates.

  • Problem

    Formalizing mathematical statements requires capturing semantic intent as well as producing syntactically accurate code, while the critic phase has received little attention compared with generation and compilation.

    Source: §1 · p. 1

  • Method

    CriticLean trains CriticLeanGPT with supervised fine-tuning and reinforcement learning to assess Lean 4 semantic fidelity, and uses critic feedback in iterative formalization refinement.

    Source: §1 · pp. 1–2

  • Results

    Trained CriticLeanGPT models outperform strong open-source and many closed-source baselines on CriticLeanBench, which contains 500 pairs split evenly between correct and incorrect formalizations.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The paper concludes that explicitly modeling and training the critic yields improvements in formalization quality and supports a corpus validated by both compiler and critic.

    Source: §7 · p. 15

    Within a 200-attempt limit, 47.2% of pipeline problems failed; performance was constrained by the base autoformalization model’s ability to produce an approvable candidate.

    Source: §6.1 · p. 14

Abstract

from arXiv · show

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.

1 Introduction

Natural-language mathematics is difficult to formalize because Lean code must capture semantic intent as well as be syntactically accurate. CriticLean centers semantic critique in an iterative formalization pipeline, evaluates critics with CriticLeanBench, and uses the framework to build FineLeanCorpus.

1 Introduction

  • Formalizing natural-language mathematics requires both syntactic accuracy and semantic understanding, especially for complex, high-level problems.The introduction argues that evaluating semantic correctness—the critic phase—has been underexplored and is essential to autoformalization.Source: §1 · p. 1
  • CriticLeanGPT assesses whether Lean 4 formalizations reflect the original statement’s intent, and its feedback joins compiler feedback in iterative refinement.The paper describes each iteration’s feedback as driving refinement of the final Lean code.Source: §1 · pp. 1–2
  • CriticLeanBench contains 500 natural-language/Lean 4 pairs, split evenly between correct and incorrect, and trained CriticLeanGPT models outperform strong open-source and many closed-source baselines.The paper frames the benchmark as testing semantic evaluation of formalizations.Source: §1 · p. 2
  • FineLeanCorpus contains 285,957 fully verified Lean 4 entries, with domain diversity, broad difficulty coverage, and semantic validation through critic feedback.The paper also introduces FineLeanCorpus-Diamond, a subset of over 36,000 high-difficulty problems.Source: §1 · p. 2

2 Related Works

Prior autoformalization work uses in-context learning or supervised fine-tuning, while semantic alignment has been assessed with LLM judges. The paper trains a domain-specific critic with reinforcement learning and situates this approach amid uncertainty about how reinforcement learning improves reasoning.

2.1 Autoformalization

  • For autoformalization, prior approaches include in-context learning and supervised fine-tuning, and prior work uses LLM-as-judge to assess semantic alignment [26] [61] [67] [76].The paper describes autoformalization as translating natural-language content into machine-verifiable representations such as Lean4 or Isabelle [68].Source: §2.1 · p. 2
  • The paper advances this work by training an open-sourced, domain-specific Qwen-family model to critique Lean4 statement alignment using reinforcement learning.The stated aim is to improve both critique capability and formalization robustness.Source: §2.1 · pp. 2–3

2.2 RL for LLM Reasoning

  • How reinforcement learning improves reasoning remains insufficiently characterized; analyses suggest it may refine sampling of latent competencies rather than create entirely new reasoning frameworks [69].Source: §2.2 · p. 3

3 CriticLeanGPT

CriticLeanBench assesses semantic alignment in Lean formalizations through diverse error types and data sources, combining automated checks with human validation. Its 500 examples are evenly split between correct and incorrect pairs, and the benchmark combines critic, Lean, and test functionality.

3.1.1 Overview of CriticLeanBench

  • CriticLeanBench evaluates critique, correction, and translation into formally verified Lean 4 theorem declarations, with coverage of varied semantic errors and data sources.Its construction principles combine expert review and automated verification to support benchmark reliability and validity.Source: §3.1.1 · p. 3

3.1.2 Automatically verified

  • The automatic validation process collects math statements and Lean 4 statements, checks compilation, then uses DeepSeek R1 to assess semantic consistency and sends its outputs for human validation.Compiler failures are also sampled, with compiler feedback retained in the benchmark.Source: §3.1.2 · p. 3

3.1.3 Human Validation Filter

  • Human validation distinguishes compilable formalizations that capture the original meaning from those that compile but fail semantic consistency, while selecting representative samples across strata and typical error types.Negative examples cover premise, representation, and goal translation errors, incorrect assumptions, logical flaws, and incomplete formalization.Source: §3.1.3 · pp. 4–5

3.1.4 Data Statistics

  • CriticLeanBench has 500 question/ground-truth pairs—250 correct and 250 incorrect—with questions averaging 700.94 tokens and ranging from 495 to 1,583 tokens.The question token counts use the Qwen2.5 tokenizer.Source: §3.1.4 · p. 5

3.1.5 Comparison to Other Benchmarks

  • CriticLeanBench combines critic and Lean functionality with a test component for translating mathematical statements into formally verified theorem declarations, features the compared benchmarks lack in combination.The comparison marks CriticLeanBench as covering all three listed features; CriticBench and CodeCriticBench lack Lean capability, while LLaVA-Critic lacks Lean and test components.Source: §3.1.5 · p. 5, §3.1.4 · p. 5

4 CriticLeanInstruct

CriticLeanInstruct combines critic examples with code and mathematics data to train CriticLeanGPT, while its seed and augmented samples encode both formalization errors and feedback. The training paradigm pairs supervised fine-tuning with rule-based reinforcement learning.

4 CriticLeanInstruct

  • CriticLeanInstruct contains 48,000 samples; its seed data uses a 1:3 math-to-code mix, retained in the augmented full dataset.The paper says it also integrates three times as much additional code and mathematics data to broaden knowledge coverage.Source: §4 · pp. 5–6

4.1 Seed Data

  • The 4,000 seed samples are evenly split between correct and incorrect cases, with human feedback and, for incorrect cases, compiler errors and detailed Chain-of-Thought explanations.Gemini2.5-Pro extends the critical feedback into the explanations.Source: §4.1 · p. 6
  • Seed errors reveal both syntactic barriers that prevent compilation and semantic gaps in premises, goals, mathematical representations, and complex word problems.The analysis covers the 2,000 incorrect seed samples; a fine-grained checklist based on the error taxonomy supports construction of negative samples.Source: §4.1 · p. 6

4.2.1 Correct Samples

  • For correct samples, the authors selected 5,560 FormalMATH statement–Lean code pairs and retained those Gemini-2.5-Pro judged correct after generating critical Chain-of-Thought assessments.The cited passages describe model filtering, not human verification of these samples.Source: §4.2.1 · p. 6

4.2.2 Incorrect Samples

  • Incorrect samples include 2,000 noncompiling OmniMath formalizations and checklist-guided modifications of correct FormalMATH code, each paired with generated explanatory reasoning.The first strategy targets syntactic or logical compilation issues; the second uses randomly selected error types to introduce subtle errors and logical flaws.Source: §4.2.2 · p. 7

4.3 Training Paradigm

  • Supervised fine-tuning uses CriticLeanInstruct, while reinforcement learning refines Qwen2.5 and Qwen3 models on 4,000 seed examples using format validation and agreement with expert labels.The RL approach uses rule-based rewards and GRPO; the stated format reward is 1 when the format is right and 0 otherwise.Source: §4.3 · p. 7

5 Experiments

CriticLeanGPT is evaluated against open- and closed-source models on CriticLeanBench, alongside analyses of training data, model scale, and Pass@k. Results report gains from mixed reasoning-data training and SFT/RL, with data-size effects varying by model scale.

5.1 Experimental Setup

  • The evaluation compares CriticLeanGPT variants with closed-source APIs, open-source LLMs, and reasoning and theorem-proving models.The listed baselines include Claude, Gemini, GPT-4o, DeepSeek, QwQ, Qwen, and Llama models.Source: §5.1 · p. 8

SOTA LLMs

  • Gemini 2.5 Pro, QwQ-32B, Qwen3-32B, and DeepSeek-R1 each score above 80, while Qwen3-32B-RL achieves strong accuracy.SFT and RL also improve detection of erroneous samples, with higher TNR and lower FNR reported.Source: §5.2.1 · p. 8

5.3.1 Effect of Reasoning Data

  • Adding code and math reasoning data improves performance across all model sizes compared with training on Seed Data 4.1 alone.CriticLeanInstruct 4 uses Critic and non-Critic data at a 1:3 ratio.Source: §5.3.1 · p. 8, Table 3 · p. 10

5.2.1 Evaluation of Critic Capability

  • CriticLeanGPT models trained with SFT and RL outperform a range of open-source, closed-source, and baseline models on CriticLeanBench.The reported comparison covers multiple model families and training variants.Source: §5.2.1 · p. 8, Table 2 · p. 9

5.3.2 Effect of SFT Dataset Size

  • SFT-data scaling effects differ by model size: expanding data yields more pronounced gains for 7B models, while 32B gains are substantial mainly at higher data volumes.The reported trend is less consistent for larger models.Source: §5.3.2 · p. 8, Figure 6 · p. 10

5.4.2 Effect of Pass@k

  • At Pass@32, Qwen2.5-7B-Instruct-SFT-RL has higher accuracy and TNR than Qwen2.5-7B-Instruct, and a similar TNR trend holds for Qwen3-8B.All evaluated models improve as k increases; SFT- and RL-optimized models more effectively select high-quality answers from more candidates.Source: §5.4.2 · pp. 10–11

5.4.1 Scaling Analysis

  • Performance on CriticLeanBench rises consistently as the evaluated Qwen model size increases across coder, instruct, SFT, RL, and Qwen3 variants.The analysis includes Qwen2.5-Coder, Qwen2.5-Instruct, Qwen2.5-Instruct-SFT, Qwen2.5-Instruct-SFT-RL, Qwen3, and Qwen3-RL.Source: §5.4.1 · p. 10, Figure 4 · p. 11

6 FineLeanCorpus

FineLeanCorpus is built through a gated formalization pipeline, while the CriticLean pipeline analysis finds higher manually verified accuracy when semantic critic checks supplement compiler feedback. The corpus analysis also emphasizes broader difficulty and domain coverage, and introduces a high-difficulty subset.

6 FineLeanCorpus

  • FineLeanCorpus problems are sourced from varied educational and competition materials, standardized, and gated by Lean compilation and CriticLeanGPT semantic checks.A final CriticLeanGPT filtering stage is expected to eliminate 74.7% of remaining incorrect formalizations, according to manual validation.Source: §6 · pp. 11–12
  • FineLeanCorpus has a multimodal difficulty distribution and expands underrepresented mathematical domains relative to Lean-Workbook.The analysis highlights enrichment in Analytic Geometry, Integral Calculus, Algorithms, and Graph Theory, and describes the more balanced distribution as important for mitigating overfitting to a narrow complexity band.Source: §6 · p. 12, Figure 7 · p. 13, Table 6 · p. 13
  • Diamond contains 36,033 FineLeanCorpus problems rated above difficulty 5, curated as a specialized high-difficulty training subset.The stated aim is to provide a demanding setting for developing sophisticated, multi-step reasoning.Source: §6 · p. 13

6.1 Analysis on CriticLean Pipeline

  • 84.0% accuracy with the CriticLean Pipeline exceeded 54.0% with Compiler Feedback on 50 manually inspected Omni-MATH problems.The pipeline regenerates until formalizations compile and pass CriticLeanGPT validation.Source: §6.1 · pp. 13–14
  • 52.8% of 500 problems passed both checks within 200 attempts, while 47.2% failed within that limit.Only 12.6% passed on the first try; the paper identifies candidate generation by the base autoformalizer as the bottleneck.Source: §6.1 · p. 14, Table 8 · p. 14
  • Human-evaluation accuracy varies across data sources, which the authors attribute primarily to differences in domain and difficulty distributions.The source comparison is presented in Table 9.Source: §6.1 · p. 14, Table 9 · p. 14

7 Conclusion

The conclusion presents CriticLean as a critic-centered framework for mathematical autoformalization. It reports an 84% accuracy result for entries from Lean-Workbook.

7 Conclusion

  • CriticLean places the critic at the center of autoformalization and uses semantic validation to refine translation and construct a corpus validated by compiler and critic.The conclusion frames explicit critic modeling and training as improving formalization quality.Source: §7 · p. 15
  • Entries from Lean-Workbook yielded an accuracy of 84%.Source: §7 · p. 15

8 Contributions and Acknowledgments

The acknowledgments identify the co-first authors and list the co-authors.

Co-First Authors

Co-Authors

  • The listed co-authors include Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, and Yifan Zhang.Source: Co-Authors · p. 16
  • The co-author list also includes Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, and Jiawei Shen.Source: Co-Authors · p. 16
  • The remaining listed co-authors are Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, and Wenhao Huang.Source: Co-Authors · p. 16

A Fine-Grained Domain Distribution of FineLeanCorpus

The FineLeanCorpus domain-distribution material lists selected topic counts and explains that the table covers its 50 most frequent topics, alphabetized by category hierarchy.

A Fine-Grained Domain Distribution of FineLeanCorpus

B Fine-Grained Domain Distribution of FineLeanCorpus-Diamond

This section presents a fine-grained topic distribution for FineLeanCorpus-Diamond and criteria for assessing mathematical content, logical structure, Lean accuracy, problem comprehension, and formalization strategy.

B Fine-Grained Domain Distribution of FineLeanCorpus-Diamond

I. Integrity & Accuracy of Mathematical Content

  • Integrity checks ask whether premises, domains, conditions, and mathematical meanings are preserved, and whether every goal and its type are translated accurately.The checklist also calls out completeness of multi-part conclusions and attainability in extremum problems.Source: §I · p. 25

II. Clarity & Correctness of Logical Structure

  • Logical-structure checks cover connectives, quantifier order and scope, how premises combine, and whether the formalization preserves the original reasoning path.The checklist highlights dependencies such as ∀ϵ > 0, ∃δ > 0.Source: §II · p. 25

III. Lean Conventions & Technical Accuracy

  • Lean-accuracy checks address syntax and declarations, type constraints, definitions and library usage, and code readability.Examples include correct numeral types and mappings from mathematical concepts to Lean counterparts.Source: §III · p. 26

IV. Problem Comprehension & Overall Consistency

  • Comprehension checks ask whether the formalization captures the core mathematical idea, is internally consistent, and is suitable for formalization.The checklist also asks whether assumptions or interpretations are documented.Source: §IV · p. 26

V. Formalization Strategy & Choices

  • Strategy checks assess whether the abstraction level is appropriate and whether alternatives, decomposition, or modularization were considered.Decomposition or modularization is specifically raised for complex problems.Source: §V · p. 26

VI. Provability & Proof Assistance

The checklist considers whether formalization preserves similar proof complexity, uses lemmas to simplify proofs, and has structure amenable to automation.

VI. Provability & Proof Assistance

  • The checklist asks whether the formalization maintains similar proof complexity.It also asks whether lemmas were added to simplify the proof.Source: §VI · p. 26
  • It also asks whether the formalization's structure is amenable to automation tools.Source: §VI · p. 26

Error Taxonomy

This section organizes formalization errors into semantic, Lean technical, and completeness or problem-formalizability categories, and provides tools for evaluating fidelity between mathematical statements and Lean code. It also specifies prompt workflows for injecting plausible semantic errors, classifying problems by mathematical domain, and assessing difficulty against reference examples.

1.1 Premise Translation Error–1.3 Goal Translation Error

  • Semantic errors include omitted or altered premises, misrepresented mathematical expressions, and goals that fail to match the requested conclusion.Examples include missing positivity or nonzero constraints, changing a cubic to a quadratic, and proving existence when a specific value is requested.Source: §1.1 · p. 26, §1.2 · p. 27, §1.3 · p. 27

1.4 Variable Usage Error–1.6 Incorrect Assumption

  • Variable misuse, incorrect mappings of mathematical concepts, and unsupported added assumptions can each distort a formalization’s intended meaning.Examples include choosing Nat rather than Real, translating residue calculation as finding a limit, and adding an unfounded numerical assumption.Source: §1.4 · p. 27, §1.5 · p. 27, §1.6 · p. 27

2. Lean Syntax and Technical Errors

  • Lean syntax and technical errors include malformed syntax, type mismatches, incorrect operator precedence or parentheses, and improper mathlib usage.These are code-level issues that can prevent compilation or cause unexpected runtime behavior.Source: §2 · p. 27, §2.1 · p. 27, §2.2 · p. 28

3. Translation Completeness and Other Meta-Errors

  • Meta-errors include problems too vague or context-dependent to formalize, incomplete coverage of requirements, and code-style weaknesses that do not necessarily undermine logical correctness.Examples include omitted multi-step requirements and unclear variable names.Source: §3 · p. 28, §3.1 · p. 28, §3.2 · p. 28

Complete Checklist for Lean4 Mathematical Formalization

  • The formalization checklist checks preconditions, variable domains and indexing, object properties, implicit conditions, and the exact meaning of conditions.It calls out distinctions such as inequality versus non-equality and strict versus non-strict bounds.Source: Complete Checklist for Lean4… · pp. 28–29
  • The checklist also checks that goals and their types are complete and precise, logical connectives and quantifiers are scoped correctly, and the formalization captures core ideas without contradictions.It includes attainability in extremum problems and whether the problem is suitable for precise formalization.Source: Complete Checklist for Lean4… · pp. 29–30

Prompt:Critical Feedback to CoT

  • The critical-feedback prompt asks for a stepwise comparison of the mathematical text and Lean code, explaining success or categorizing identified failures and their impact.It directs the evaluator to examine definitions, constraints, syntax, and proof targets; a separate prompt asks an engineer to introduce checklist-based errors into correct code.Source: Prompt:Critical Feedback to CoT · pp. 30–32, Prompt:Lean Flaw Injection · p. 34

Prompt:Formal Verification Expert

  • The formal-verification prompt judges whether a Lean theorem statement exactly formalizes the problem, comparing semantics, logic, constraints, types, and syntax while ignoring the proof.Its final judgment must rely only on what is explicitly expressed in the Lean statement.Source: Prompt:Formal Verification Expert · pp. 33–34

Prompt:Lean Flaw Injection

  • Flaw injection selects exactly two applicable checklist strategies and uses them to introduce plausible, context-specific deviations into correct Lean code, with changes explained separately.The input pairs a math statement with its correct Lean formalization; proofs may be omitted, and comments explaining the changes are prohibited inside the statement or code.Source: Prompt:Lean Flaw Injection · pp. 34–35

Prompt: Mathematical Problem Classification Task

Prompt:Difficulty Level Assessment

  • Difficulty assessment rates the informal problem by reasoning demands, including abstraction, creativity, number of steps, and familiarity with advanced techniques.Reference examples span difficulty levels 1–10, and the prompt asks for a score and rationale informed by the problem and those examples.Source: #OBJECTIVE · pp. 37, 40, #DIFFICULTY REFERENCE · p. 38
Loading 2507.06181v1…