TreeThink让大模型在数学证明中高效搜索，支持多语言实时验证。
TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
- 模块化异步树搜索，集成vLLM推理与多种评估方法。
- 在miniF2F和MATH500上实现跨语言形式化证明，提速6.3倍。
- 适配Lean4、Isabelle/HOL等系统，支持自然语言与正式语言。
树搜索算法可系统探索神经定理证明中的证明空间。现有大模型树搜索库主要面向自然语言推理，缺乏与形式化验证器的原生集成；而定理证明系统通常依赖特定任务的搜索实现。我们提出TreeThink，一个开源的Python库，支持神经定理证明中的模块化、全异步树搜索。它将成熟的树搜索方法与基于vLLM的推理管道及多样化的节点评估技术（从轻量启发式到神经评估器）相结合。支持Lean~4、Rocq和Isabelle/HOL，以及自然语言。通过直接连接各语言的读-求值-打印循环（REPL）服务器，实现实时验证与证明状态提取。我们在miniF2F和MATH500数据集上评估了TreeThink，展示了跨语言形式化证明搜索能力、自然语言推理支持，以及异步执行带来的最高6.3倍壁挂时间加速。代码以MIT许可证发布于https://github.com/GGLAB-KU/treethink，可通过https://pypi.org/project/treethink/ 下载使用。
原文摘要 · Abstract (English)
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 6.3$\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/ .
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。