arXiv:2504.06122v2 声明类型: 替换 摘要: 通过大语言模型（LLM）在自动定理证明（ATP）方面取得的最近进展，突显了Lean 4代码形式推理的潜力。然而，ATP尚未因OpenAI的O1/O3和Deepseek的R1所展示的后续训练缩放而实现革命性的变革。在本文中，我们研究了整个后续训练过程，旨在使其与自然语言推理模型的突破相一致。首先，我们使用包含大量命题-证明配对以及旨在纳入模拟人类推理和假设完善的认知行为的额外数据，持续训练当前的ATP模型。其次，我们探索了通过Lean 4编译器返回的结果奖励进行强化学习的方法。通过我们设计的持续训练和强化学习过程，我们成功改进了现有的形式证明器，包括DeepSeek-Prover-v1.5和Gödel-Prover，并在整体证明生成领域达到了最先进的性能。例如，在MiniF2F中，我们实现了32%处的59.8%通过率（pass@32）。这是一个正在进行的项目，我们将逐步更新我们的发现，发布我们的数据和训练细节。