摘要
自动形式化旨在将自然语言数学文本翻译为 Lean4 等形式证明语言，以加速 AI 辅助数学研究。本文在 FineLeanCorpus 数据集上，利用 LoRA 微调 Qwen3.5-2B 模型，对比了三种训练策略：带课程学习的监督微调、无课程排序的监督微调，以及基于循环一致性奖励的强化学习（GRPO）。循环一致性通过衡量
AI 推荐理由
论文聚焦数学形式化，直接提升 LLM 的逻辑与数学推理能力，属核心研究。
研究机构
斯坦福大学计算机科学系
论文信息