arXiv:2502.13137v1 宣布类型: 新 摘要: 由于合成数据有望增强大型语言模型（LLM）的数学能力，对合成数据的需求增加。然而，确保中间推理步骤的有效性仍然是一个重大挑战，影响数据质量。虽然使用定理证明器的形式验证可以有效验证LLM的推理，但数学证明的自动形式化仍存在错误。为应对这一挑战，我们引入了迭代自动形式化，这是一种方法，通过迭代细化定理证明器的形式化来减轻错误，从而将Lean证明器的执行率从60%提高到87%。在此基础上，我们引入了《定理证明器作为裁判》（TP-as-a-Judge）方法，该方法利用定理证明器的形式化来严格评估LLM的中间推理，有效将自动形式化与合成数据生成结合在一起。最后，我们提出了《基于定理证明器反馈的强化学习框架》（RLTPF），该框架用定理证明器反馈替代了基于人类反馈的强化学习中的手动注释。在多种LLM上应用TP-as-a-Judge和RLTPF仅需3,508样本，分别在Mistral-7B（MultArith）上的准确率为5.56%，在Llama-2-7B（SVAMP）上的准确率为6.00%，在Llama-3.1-8B（AQUA）上的准确率为3.55%。