英文标题：TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
作者：Burak S. Akbudak, Zeynel A. UluÅan, Can S. Erer, Gözde Gül Åahin
arXiv ID：2607.11258 | 分类：cs.CL | 发表：2026-09-08
许可：CC-BY-SA
摘要 树搜索算法能够系统性地探索神经定理证明中的证明空间。现有的LLM树搜索库主要针对{{NL}}自然语言推理，并未提供与形式验证器的原生集成，而定理证明系统通常依赖于特定任务的搜索{{NL}}实现。我们推出了TreeThink，这是一个开源的Python库，用于神经定理证明中的模块化、完全异步树搜索。它将成熟的树搜索方法与基于vLLM的推理流水线以及多种节点评估技术（从轻量级启发式方法到神经评估器）集成在一起。我们支持Lean 4、Rocq和Isabelle/HOL以及自然语言。它直接连接到每种语言的读取-求值-打印循环（REPL）服务器，用于实时验证和证明状态提取。我们在{{NL}}min
Tree search algorithms enable systematic exploration of the proof space in neural theorem proving. Existing LLM tree search libraries primarily target natural language reasoning and do not provide native integration with formal verifiers, while theorem proving systems often rely on task-specific search implementations. We introduce TreeThink, an open-source Python library for modular, fully asynchronous tree search in neural theorem proving. It integrates established tree search methods with vLLM-based inference pipelines and diverse node evaluation techniques, ranging from lightweight heuristics to neural evaluators. We support Lean~4, Rocq, and Isabelle/HOL alongside natural language. It connects directly to each language's Read-Eval-Print Loop (REPL) server for real-time verification and proof state extraction. We evaluate TreeThink on miniF2F and MATH500, demonstrating cross-language formal proof search, natural language reasoning support, and up to 8.0$\times$ wall-clock speedup from asynchronous execution. Source code is released under the MIT license at https://github.com/GGLAB-KU/treethink , and the library is accessible as a downloadable package at https://pypi.org/project/treethink/ .
查看完整双语翻译 →
正在跳转到翻译阅读页… 如果没有自动跳转，请点击这里。