arXiv:2504.06122v1 宣传类型: 新 摘要: 通过大型语言模型（LLM）推进自动化定理证明（ATP）的最新进展突显了Lean 4代码形式推理的潜力。然而，ATP尚未通过Open AI的O1/O3和Deepseek的R1所展示的后训练扩展得到革命性的改变。在这项工作中，我们研究了整个后训练的ATP，旨在使其与自然语言推理模型的突破相一致。首先，我们使用由大量命题-证明对以及旨在模拟人类推理和假说改进的认知行为的附加数据构成的混合数据集，对当前的ATP模型进行持续训练。接着，我们探索使用Lean 4编译器返回的结果奖励的强化学习。通过我们设计的持续训练和强化学习过程，我们成功地改进了现有的形式证明器，包括DeepSeek-Prover-v1.5和Goedel-Prover，实现了整个证明生成领域的最先进性能。例如，在MiniF2F上，我们达到了59.8%的通过率（pass@32）。这是一个持续的项目，我们将逐步更新我们的发现，发布我们的数据和训练细节。