LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

📄 arXiv: 2507.14722v1 📥 PDF

作者: Matěj Kripner, Michal Šustr, Milan Straka

分类: cs.LG, cs.AI

发布日期: 2025-07-19

💡 一句话要点

LeanTree：利用因子化状态加速Lean 4中的白盒证明搜索

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动定理证明 白盒方法 Lean 4 因子化状态 并行搜索

📋 核心要点

  1. 自动定理证明面临状态空间巨大和缺乏有效利用中间状态的挑战。
  2. LeanTree通过因子化证明状态为独立分支，简化搜索和数据生成。
  3. 初步结果表明，LeanTree在某些场景下优于黑盒方法，具有潜力。

📝 摘要（中文）

自人工智能诞生以来，自动定理证明（ATP）一直是一个经典问题，但由于其巨大的状态和动作空间，它仍然具有挑战性。最近，大型语言模型（LLM）已成为ATP的一种有希望的启发式方法，但它们缺乏正确性保证，因此需要与证明验证器进行交互。这种交互通常遵循两种方法之一：黑盒交互，不利用中间证明状态；或白盒方法，允许增量证明构建和中间状态的检查。虽然黑盒方法直接受益于最近的LLM进展，但白盒方法相对滞后。在本文中，我们通过引入LeanTree来解决这一差距，LeanTree包括（i）一个用Lean 4语言构建的工具，将复杂的证明状态分解为更简单、独立的 branches，以及（ii）这些因子化中间状态的数据集。我们的白盒工具优于黑盒方法：简化评估，减少必要的上下文，生成更丰富的训练数据，支持跨多个状态的并行搜索，支持状态的有效重用，并在出现错误时提供反馈。我们的初步结果表明，在某些设置中，白盒方法优于黑盒替代方案。

🔬 方法详解

问题定义：自动定理证明（ATP）领域，特别是与大型语言模型（LLM）结合时，面临着状态空间巨大、探索效率低下的问题。现有的黑盒方法虽然受益于LLM的进步，但无法利用中间证明状态，导致信息损失和难以调试。白盒方法虽然可以检查中间状态，但复杂度高，难以有效利用。

核心思路：LeanTree的核心思路是将复杂的证明状态分解为更小、更独立的子问题（即“branches”），从而降低搜索空间维度，提高搜索效率。通过因子化状态，可以并行处理多个子问题，并更容易地重用已有的证明步骤。

技术框架：LeanTree包含两个主要组成部分：一是基于Lean 4语言开发的工具，用于将证明状态因子化为独立的branches；二是包含这些因子化中间状态的数据集，用于训练和评估模型。整体流程是：首先，使用Lean 4工具对原始证明状态进行分解；然后，利用分解后的状态进行并行搜索和证明；最后，将证明结果进行整合，完成整个定理的证明。

关键创新：LeanTree的关键创新在于其因子化状态表示方法。通过将复杂的证明状态分解为独立的branches，可以显著降低搜索空间，并允许并行搜索。此外，LeanTree还提供了一个包含大量因子化中间状态的数据集，可以用于训练更有效的证明策略。

关键设计：LeanTree工具使用Lean 4的元编程能力来实现证明状态的因子化。具体的因子化策略（如何选择分解点、如何保证分解后的子问题仍然可解等）是关键的设计细节，论文中可能没有详细描述（未知）。数据集的构建也需要仔细设计，以保证数据的质量和多样性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

论文的初步实验结果表明，在某些设置下，LeanTree的白盒方法优于黑盒替代方案。这表明因子化状态表示和并行搜索策略能够有效提升自动定理证明的效率。具体的性能提升幅度可能需要在后续实验中进一步验证。

🎯 应用场景

LeanTree具有广泛的应用前景，可用于提升自动定理证明器的性能，辅助数学家和计算机科学家进行定理证明，并可应用于形式化验证、软件验证等领域。通过与大型语言模型结合，LeanTree有望实现更智能、更高效的自动定理证明系统，加速科学发现和技术创新。

📄 摘要（原文）

Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Large language models (LLMs) have recently emerged as a promising heuristic for ATP, but they lack correctness guarantees and thus require interaction with a proof verifier. Such interactions typically follow one of two approaches: black-box interaction, which does not utilize intermediate proof states, or white-box approaches, which allow for incremental proof construction and examination of intermediate states. While black-box approaches have directly benefited from recent LLM advances, white-box methods have comparatively lagged behind. In this paper, we address this gap by introducing LeanTree, which consists of (i) a tool built in the Lean 4 language that factorizes complex proof states into simpler, independent branches, and (ii) a dataset of these factorized intermediate states. Our white-box tooling offers several advantages over black-box approaches: it simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient reuse of states, and provides feedback in case of errors. Our preliminary results hint that white-box approaches outperform black-box alternatives in some settings.