符号搜索并未穷尽：Lean4 中持久证明空间探索
Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4
浏览论文内容
中文总结 AI 辅助
提出ViaLean，通过持久证明状态图的受限探索组织符号推理，在miniF2F上无模型配置达到50.0% pass@1，并支持神经-符号智能体接口。
中文摘要 AI 辅助
形式定理证明日益将学习到的语义引导与经过验证的符号执行相结合。因此，符号搜索基础的质量决定了在有限推理预算下能够积累、重用和暴露多少有用的数学结构。我们提出了ViaLean，一个Lean4证明器，将符号推理组织为对持久证明状态图的受限探索。其搜索在互补的推理模式之间保持覆盖，合并语义等价的目标，保留经过验证的中间结构，并在提交转换之前观察短暂的符号未来。在完整的miniF2F测试分割上，无模型配置解决了122/244个问题（50.0% pass@1）。从Lean早期的tidy搜索到现代的grind和SMT支持的验证，历史和近期的符号参考点表明，证明空间组织仍然是能力的重要来源。相同的持久状态也为神经-符号智能体提供了自然接口：神经推理可以在经过验证的区域和中间对象上运行，而Lean持续扩展并验证局部证明空间。
英文摘要
Formal theorem proving increasingly combines learned semantic guidance with verified symbolic execution. The quality of the symbolic search substrate therefore determines how much useful mathematical structure can be accumulated, reused, and exposed under a finite inference budget. We introduce ViaLean, a Lean4 prover that organizes symbolic reasoning as bounded exploration of a persistent proof-state graph. Its search preserves coverage across complementary reasoning modes, merges semantically equivalent goals, retains verified intermediate structure, and observes short symbolic futures before committing to a transition. On the complete miniF2F test split, the model-free configuration solves 122/244 problems (50.0% pass@1). Historical and recent symbolic reference points range from Lean's earlier tidy search to modern grind and SMT-backed verification, showing that proof-space organization remains a substantial source of capability. The same persistent state also provides a natural interface for neural--symbolic agents: neural reasoning can operate over verified regions and intermediate objects while Lean continuously expands and validates the local proof space.
发表机构
- Xi’an Jiaotong-Liverpool University（西交利物浦大学）
机构由 AI 辅助整理，请以论文原文为准。
