TreeThink：使用 LLM 进行数学推理的模块化树搜索库

树搜索算法能够系统地探索神经定理证明中的证明空间。现有的 LLM 树搜索库主要针对自然语言推理，不提供与形式验证器的本机集成，而定理证明系统通常依赖于特定于任务的搜索实现。我们介绍 TreeThink，一个开源 Python 库，用于神经定理证明中的模块化、完全异步树搜索。它将现有的树搜索方法与基于 vLLM 的推理管道和各种节点评估技术（从轻量级启发式到神经评估器）集成在一起。除了自然语言之外，我们还支持 Lean~4、Rocq 和 Isabelle/HOL。它直接连接到每种语言的读取-评估-打印循环 (REPL) 服务器，以进行实时验证和证明状态提取。我们在 miniF2F 和 MATH500 上评估 TreeThink，展示了跨语言形式证明搜索、自然语言推理支持以及异步执行高达 8.0$\times$ 的挂钟加速。源代码根据 MIT 许可证在 https://github.com/GGLAB-KU/treethink 发布，并且该库可作为可下载包在 https://pypi.org/project/treethink/ 访问。