通过循环一致性改进 Lean4 自动形式化 微调

自动形式化——自动将自然语言数学文本翻译成正式的证明语言，例如 Lean4——可以帮助加速人工智能辅助的数学研究，无论是通过证明验证还是证明搜索。我将自然语言的 Qwen3.5-2B 与 LoRA 微调到 FineLeanCorpus 上的 Lean4 形式化，并考虑三种训练方案：带课程学习（难度 1 至 10）的监督 微调 (SFT)、无课程排序的 SFT，以及使用具有循环一致性奖励的组相对策略优化 (GRPO) 的强化学习。循环一致性衡量通过 NL 到 Lean4 到 NL' 循环保留语句含义的程度，计算为现成句子嵌入的余弦相似度。在 FineLeanCorpus (FLC) 和 PutnamBench 的一个看不见的子集上，RL 的性能显着优于两种 SFT 变体（FLC 上的平均循环一致性为 0.669 vs. 0.513；PutnamBench 上的平均循环一致性为 0.561 vs. 0.422），同时交叉熵损失仅增加了 0.011 nat，对形式化质量的影响最小。与随机训练相比，课程排序并没有提供可衡量的好处。