该框架创新性地将评估模型置于核心位置。通过强化学习训练的CriticLeanGPT模型，能像数学专家一样精准判断形式化代码是否贴合原始语义，配合迭代优化机制，让生成的定理证明既符合语法规范，又忠实于数学逻辑。 将自然语言描述的数学命题转化为机器可验证的形式化代码（如Lean 4定理），是自动化定理证明领域的基础性难题，其核心挑战不仅在于语法层面的准确转换，更在于对数学语义的深度理解与忠实还原。 尽管现有研究在生成模型与编译有效性上取得一定进展，但在复杂问题的语义对齐上仍存在显著瓶颈，具体体现在以下三方面： 语义鸿沟：自然语言数学命题的隐含条件等难精准映射为形式逻辑，易出现前提翻译偏差等问题，过往方法因缺语义一致性校验，导致大量逻辑错误的形式化结果。评价缺位：对形式化结果的评价依赖编译检查或 LLM 简单判断，存在错误类型覆盖不全、评价可靠性不足的问题，难以识别逻辑矛盾等。数据瓶颈：现有数学形式化数据集规模和多样性不足、难度分布单一、语义校验缺失，制约了模型应对复杂数学命题的能力。 CriticLean框架将引入强化学习的 Critic 模型，通过训练专门的语义评价模型（CriticLeanGPT）、结合 Lean 4 编译器反馈进行迭代生成。系统性解决语义对齐、评价可靠性与数据质量问题，为数学自动化形式化提供了全新范式。 有监督微调（SFT）：在4.8万条包含：数学、代码以及数学语句-形式化代码对一致性相关的Critic数据CriticLeanInstruct数据集上训练，增强其针对语义判断的评估能力。强化学习优化（RL）：采用GRPO算法，以“判断是否准确”和“输出格式是否规范”作为奖励信号，让模型学会在评估中迭代提升。 CriticLeanBench是用于评估模型在数学形式化任务中关键推理能力的基准测试，旨在全面衡量模型将自然语言数学陈述转化为经形式验证的定理声明等方面的表现. CriticLeanBench 在数据收集阶段，从多个数据来源选取数学陈述及对应的Lean 4 陈述，提交Lean 4陈述到编译器。1）对于编译失败的语句，随机采样保留编译器反馈信息。2）对于编译成功的部分，通过使用 DeepSeek R1 结合专家校验的方式保留正确和错误的样本（错误的样本保留错误信息）。 数据来源多样：数学陈述选取了Omni-MATH、AIME、U-MATH等多个数据源，这些数据源涵盖了不同难度层次和数学领域的问题。有助于更全面准确地评估模型在不同数学内容上的表现。覆盖多种错误类型：CriticLeanBench 覆盖语法错误、语义错误、逻辑错误等多种问题，全面考察模型能力。确保评估可靠有效：通过专家审查和大模型验证相结合的方式来保证评估基准的可靠性和有效性。在不同类别中选取具有代表性的样本，确保涵盖各种错误类型，从而使评估结果更可靠。 核心指标：Qwen3-32B-RL版本准确率达87%，true negative rate（正确识别错误样本）达85.6%，远超GPT-4o的40.0%。对比优势：在相同模型规模下，经CriticLean训练的Qwen2.5-32B模型准确率（78.6%）较基础版（73.0%）提升5.6%，且对错误样本的识别能力提升明显。 规模与多样性：包含285,957条样本，覆盖从高中奥数到大学数学的16个领域，其中高难度子集（Diamond）含36,033条问题。质量保障：每条样本均通过编译器语法检查与CriticLeanGPT语义验证，人工抽检准确率达84%以上。结构优势：相比LeanWorkbook，其难度分布更均衡（多峰分布），领域覆盖更全面（如解析几何样本量提升300%）。 将该框架应用于自动形式化流程，配合Kimina-Autoformalizer-7B生成器，准确率从38%（单轮生成）提升至84%（多轮迭代优化），其中语义评估环节贡献了30个百分点的提升。
