OpenProver 用 Lean 4 实现智能交互式定理证明

背景

形式化验证和自动定理证明（ATP）是计算机科学和数学领域的重要研究方向。近年来，大型语言模型（LLM）的快速发展为自动定理证明带来了新的范式，将自然语言理解与符号推理相结合。Lean 4 作为新兴的交互式定理证明器，因其强大的形式化验证能力而受到关注。已有一些基于 LLM 的 ATP 系统（如 Aletheia）展示了 agentic 架构的潜力，但多数系统闭源或难以复现。OpenProver 正是在这一背景下提出的开源解决方案，旨在融合 LLM 的推理能力与 Lean 4 的形式化验证，同时提供可交互的人机协同证明搜索环境。

核心内容

OpenProver 是一个开源系统，结合了大型语言模型驱动的自动定理证明（ATP）与 Lean 4 形式化验证。其核心架构采用 Planner-Worker-Verifier 模式，灵感来源于近期基于 agent 的 ATP 系统（如 Aletheia）。具体来说，Planner agent 维护一个紧凑的 Whiteboard 暂存区以及一个无界 Repository 来存储中间发现，并将数学任务分解为可并行执行的 Worker。

OpenProver 完全开源，通过自动形式化验证生成的证明来实现可复现的评估。此外，系统提供交互式终端界面，支持人类引导的证明搜索。在交互模式下，操作员可以监控并引导证明搜索过程——这一设计借鉴了交互式代码生成中已被验证的人机协同理念。

为了展示自动形式化验证在定量消融实验中的潜力，研究者在 ProofNet 数据集上评估了 OpenProver，并与一个简单基线进行了对比。OpenProver 的源代码和更多信息可参见其 GitHub 仓库（原文提供了相关 URL）。

关键要点

• OpenProver 是一个开源系统，结合 LLM 驱动和 Lean 4 形式化验证，旨在实现自动定理证明。
• 采用 Planner-Worker-Verifier 架构：Planner agent 维护 Whiteboard 暂存区和 Repository 仓库，并将任务分解为并行 Worker。
• 支持两种模式：全自动模式（无需人工干预）和交互模式（允许人类监控并引导证明搜索过程）。
• 通过自动形式化验证保证生成证明的正确性，从而使评估过程可复现。
• 在 ProofNet 数据集上进行了定量消融实验，与简单基线进行对比（原文未提供具体数值）。
• 系统完全开源，鼓励社区复现和扩展。

意义与影响

OpenProver 的发布对自动定理证明领域具有多重意义。首先，作为完全开源的系统，它填补了当前 LLM 驱动的 ATP 系统中可复现性不足的空白，使得其他研究者可以基于其代码进行消融实验和改进。其次，Planner-Worker-Verifier 架构提供了一种模块化的 agentic 设计方案，有助于后续研究探索更复杂的分解与验证策略。第三，交互式界面的引入重申了人机协同在复杂推理任务中的价值——类似交互式代码生成中的经验可迁移到定理证明中，使得人类专家能够参与到自动化证明的关键决策中。最后，通过对 ProofNet 的基准测试，OpenProver 为定量评估 ATP 系统提供了可复现的范例，这将推动该领域更加严谨的实证研究。