摘要
本文介绍了 TreeThink，一个开源 Python 库，旨在为神经定理证明提供模块化且完全异步的树搜索功能。现有库多针对自然语言推理且缺乏形式验证器集成，而 TreeThink 集成了多种树搜索方法与基于 vLLM 的推理管道，支持从轻量级启发式到神经评估器的多样节点评估技术。该库支持 Lean 4、Rocq 和 Isabelle/HOL 等形式语言及自然语言，通过连接各语言的 REPL 服务器实现实时验证与证明状态提取。实验表明其在 miniF2F 和 MATH500 基准上实现了跨语言形式证明搜索，并通过异步执行获得了高达 6.3 倍的加速比。
AI 推荐理由
论文核心是构建用于数学推理的树搜索库，直接提升 LLM 在定理证明中的推理能力。
研究机构
Computer Engineering Department, Bogazici University, Istanbul, Turkey
Codeaway Studios
Friedrich-Alexander-Universität Erlangen-Nürnberg, Intelligent Language Systems
Computer Engineering Department, Koç University, Istanbul, Turkey
KUIS AI Lab, Istanbul, Turkey
论文信息