Leanabell-Prover：形式推理中的训练后扩展

通过 LLM 实现的自动定理证明 (ATP) 的最新进展突显了使用 Lean 4 代码进行形式化推理的潜力。然而，正如 Open AI O1/O3 和 Deepseek R1 所证明的那样，ATP 尚未被最近的后训练扩展所彻底改变。在这项工作中，我们研究了 ATP 的整个后训练过程，旨在使其与自然语言推理模型的突破保持一致。首先，我们使用混合数据集持续训练当前的 ATP 模型，该数据集由大量语句-证明对以及旨在结合模拟人类推理和假设改进的认知行为的附加数据组成。接下来，我们探索了强化学习，使用了 Lean 4 编译器返回的结果奖励。通过我们设计的持续训练和强化学习过程，我们成功地改进了现有的形式化证明器，包括 DeepSeek-Prover-v1.5 和 Goedel-Prover，在全证明生成领域取得了最先进的性能。例如，我们在 MiniF2F 上实现了 59.8% 的通过率 (pass@32)。这是一个正在进行的项目，我们将逐步更新我们的发现，发布我们的数据和训练详细信息。