Abstract
CriticLean is a critic-guided training framework for checking whether a Lean 4 formalization preserves the meaning of a natural-language mathematics problem. The work trains CriticLeanGPT variants with supervised fine-tuning and GRPO reinforcement learning, using a 48,000-example mixture of critic, code, and mathematics data plus a 4,000-example expert-labeled RL seed. CriticLeanBench supplies 500 balanced correct and incorrect statement pairs for measuring semantic classification, while syntax is checked independently by the Lean compiler. The trained critic is then placed inside an iterative autoformalization loop: compilation or semantic errors trigger regeneration. That loop produces FineLeanCorpus, 285,957 verified statement pairs, including more than 36,000 high-difficulty Diamond examples. Reported results analyze accuracy, class-specific error rates, model scale, data scale, and Pass@k rather than defining a public model leaderboard.
Contributions
- Introduces CriticLeanGPT, a family of Qwen-based semantic critics trained with supervised fine-tuning and rule-reward GRPO to judge natural-language-to-Lean 4 alignment.
- Builds CriticLeanBench with 500 long-form examples balanced between 250 correct and 250 incorrect formalizations, validated by compiler checks, model screening, and human review.
- Constructs CriticLeanInstruct as a 48,000-example 1:3 mixture of critic data and general code/mathematics reasoning data, anchored by 4,000 expert-labeled seed examples with detailed critique traces.
- Uses compiler and critic feedback in an iterative autoformalization pipeline to create FineLeanCorpus with 285,957 entries and a 36,000-plus-example high-difficulty FineLeanCorpus-Diamond subset.
Method & evaluation
- CriticLeanBench draws mathematical statements from sources including Omni-MATH, AIME, U-MATH, DEMI-MathAnalysis, HARDMath, OlympiadBench, and BlueMO. Lean compilation and DeepSeek-R1 screening precede human validation; the final set has 250 semantically correct and 250 incorrect pairs averaging 700.94 Qwen2.5 tokens.
- The 4,000-example seed set is split evenly between correct and incorrect cases. Human experts provide critique feedback, compiler messages accompany incorrect code, and Gemini 2.5 Pro expands the feedback into detailed reasoning traces.
- Supervised fine-tuning uses CriticLeanInstruct, a 48,000-example mixture with one part critic data to three parts code and mathematics data. Qwen2.5 models at 7B, 14B, and 32B are compared with critic-only SFT and the mixed-data recipe.
- GRPO training uses the 4,000 seed examples. The reward checks both whether the predicted judgment matches the expert label and whether the response obeys the required format; the final binary reward is the minimum of the two checks.
- At inference, an autoformalizer proposes a Lean statement, the Lean compiler tests syntax and elaboration, and CriticLeanGPT tests semantic fidelity. Either a compilation error or critique error sends the example back for another generation attempt.
- Evaluation reports single-response ACC, TPR, FPR, TNR, and FNR on CriticLeanBench, plus Pass@8 and Pass@32 analyses. The paper compares base, SFT, RL, and SFT-plus-RL variants alongside open and API baselines.
Evaluation metrics
Accuracy (ACC) — Higher is better. Percentage of the 500 CriticLeanBench pairs assigned the correct semantic-consistency label. Score range: [0, 100].
True Positive Rate (TPR) — Higher is better. Recall on the 250 semantically correct formalizations. Score range: [0, 100].
True Negative Rate (TNR) — Higher is better. Recall on the 250 incorrect formalizations; especially relevant when the critic is used to reject bad autoformalizations. Score range: [0, 100].
False Negative Rate (FNR) — Lower is better. Percentage of incorrect formalizations mislabeled as correct; equal to 100 − TNR under the paper's class convention. Score range: [0, 100].
Figures & tables
