LeanTree：基于因子化状态加速 White-Box 证明搜索
机器学习
2025-07-22 v1 人工智能
摘要
自动化定理证明（ATP）是人工智能领域的经典问题，由于其庞大的状态与动作空间，仍面临挑战。大语言模型（LLM）最近作为 ATP 的热门启发式方法出现，但缺乏正确性保证，因而需要与证明验证器交互。这种交互通常遵循两种方法之一：黑盒交互不利用中间证明状态，或白盒方法允许逐步证明构建并检查中间状态。虽然黑盒方法直接受益于最近的 LLM 进展，但白盒方法相对滞后。在本文中，我们通过引入 LeanTree 来弥补这一差距。LeanTree 包括 (i) 基于 Lean 4 语言构建的用于将复杂证明状态分解为更简单、独立分支的工具，以及 (ii) 这些因子化中间状态的数据集。我们的白盒工具相对于黑盒方法具有若干优势：简化评估、减少必要上下文、生成更丰富的训练数据、支持跨多个状态的并行搜索、实现状态的高效复用，以及在出错时提供反馈。我们的初步结果暗示在某些情境下，白盒方法优于黑盒方法。
引用
@article{arxiv.2507.14722,
title = {LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4},
author = {Matěj Kripner and Michal Šustr and Milan Straka},
journal= {arXiv preprint arXiv:2507.14722},
year = {2025}
}