論文の概要: TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs

• arxiv url: http://arxiv.org/abs/2607.11258v1
• Date: Mon, 13 Jul 2026 08:40:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-14 17:47:21.399525
• Title: TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
• Title（参考訳）: TreeThink: LLMを用いた数学的推論のためのモジュラーツリー検索ライブラリ
• Abstract要約: TreeThinkは、ニューラルネットワークの定理証明において、モジュール化された完全に非同期なツリー検索のためのPythonライブラリである。 確立された木探索手法をvLLMベースの推論パイプラインと多様なノード評価手法と統合する。 TreeThinkは自然言語とともにLean4、Rocq、Isabelle/HOLをサポートしている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: 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/ .
• Abstract（参考訳）: 木探索アルゴリズムは、ニューラル定理証明における証明空間の体系的な探索を可能にする。 既存のLLM木探索ライブラリは主に自然言語の推論を対象とし、形式的検証器とのネイティブ統合を提供していないが、定理証明システムはタスク固有の探索実装に依存していることが多い。 TreeThinkは、ニューラルネットワークの定理証明において、モジュール化された完全に非同期なツリー探索のためのオープンソースのPythonライブラリである。 確立された木探索手法とvLLMベースの推論パイプライン、軽量ヒューリスティックからニューラル評価まで多様なノード評価技術を統合する。 自然言語とともにLean~4、Rocq、Isabelle/HOLをサポートします。 各言語のread-Eval-Print Loop(REPL)サーバに直接接続し、リアルタイムの検証と証明状態の抽出を行う。 我々は、 miniF2F と MATH500 上で TreeThink を評価し、言語間の形式的証明探索、自然言語推論サポート、非同期実行から最大6.3$\times$ Wall-clock の高速化を実証した。 ソースコードはMITライセンスでhttps://github.com/GGLAB-KU/treethinkでリリースされている。

関連論文リスト

• Novelty-based Tree-of-Thought Search for LLM Reasoning and Planning [0.22917707112773592]
  思考のツリーは、連続した考えや思考の"パス"を構築することに依存している。 探索木に見られるノードと比較して,新しいノード(思考)の特異性を記述する,ノベルティの計測可能な概念が提案されている。
  論文  参考訳（メタデータ） (2026-05-07T11:28:53Z)
• LiTS: A Modular Framework for LLM Tree Search [3.48949373776636]
  LiTSは、木探索によるLLM推論のためのモジュール化されたPythonフレームワークである。 ツリー検索を3つの再利用可能なコンポーネントに分解する。 デコレータベースのレジストリにより、ドメインの専門家が新しいドメインに拡張できる。
  論文  参考訳（メタデータ） (2026-02-28T12:54:37Z)
• Bringing Structure to Naturalness: On the Naturalness of ASTs [9.100580570005407]
  我々は、コードの構造的表現が同様に統計的に予測可能であること、すなわち、コードの構造的ビューも自然であることを示す。 このような自然性信号が、ジャスト・イン・タイム欠陥予測の最先端結果にどのように利用されるかを示す。
  論文  参考訳（メタデータ） (2025-04-11T03:43:46Z)
• Don't Get Lost in the Trees: Streamlining LLM Reasoning by Overcoming Tree Search Exploration Pitfalls [83.89771461061903]
  検証者による木探索アルゴリズムの最近の進歩は、大規模言語モデル(LLM)の推論能力を大幅に向上させた。 検証者による木探索アルゴリズムの最近の進歩は、大規模言語モデル(LLM)の推論能力を大幅に向上させた。 意味論的に等価なコンテンツを持つ冗長な状態による$textitover-Exploration$と、検証器のスコアリングにおける高いばらつきに起因する$textitunder-Exploration$である。 各種木探索アルゴリズムに適合するフレキシブルなプラグアンドプレイシステムであるFETCHを提案する。
  論文  参考訳（メタデータ） (2025-02-16T16:12:01Z)
• Tree-of-Traversals: A Zero-Shot Reasoning Algorithm for Augmenting Black-box Language Models with Knowledge Graphs [72.89652710634051]
  知識グラフ(KG)は、信頼性があり、構造化され、ドメイン固有であり、最新の外部知識を提供することで、Large Language Models(LLM)を補完する。 そこで本研究では,ゼロショット推論アルゴリズムであるTree-of-Traversalsを導入する。
  論文  参考訳（メタデータ） (2024-07-31T06:01:24Z)
• PyTreeNet: A Python Library for easy Utilisation of Tree Tensor Networks [0.0]
  この作業はPythonライブラリPyTreeNetのユーザガイドです。 ライブラリの機能を導入するためのコード例と演習が含まれている。 主な焦点は量子系の時間発展である。
  論文  参考訳（メタデータ） (2024-07-18T08:03:38Z)
• LiteSearch: Efficacious Tree Search for LLM [70.29796112457662]
  本研究では,動的ノード選択とノードレベルの探索予算を備えた新しいガイド付き木探索アルゴリズムを提案する。 GSM8KおよびTabMWPデータセットを用いて行った実験により,本手法はベースライン法に比べて計算コストが大幅に低いことを示した。
  論文  参考訳（メタデータ） (2024-06-29T05:14:04Z)
• Recursive Speculative Decoding: Accelerating LLM Inference via Sampling Without Replacement [11.91629418177851]
  投機的復号法(英: Speculative decoding)は、大規模言語モデルの推論・加速度法である。 近年の作業では、草稿の伐採によってこの方法が進歩している。 再帰的投機的復号法(Recursive Speculative Decoding:RSD)を提案する。
  論文  参考訳（メタデータ） (2024-02-21T22:57:49Z)
• Autonomous Tree-search Ability of Large Language Models [58.68735916408101]
  大規模言語モデルは、高度なプロンプト技術で顕著な推論能力に優れています。 近年の研究では、LLMがより困難な推論タスクを解くために受動的木探索を行えるように、検索ロジックを定義するために外部プログラムを活用することが提案されている。 我々は,LLMの自律木探索能力という新しい概念を提案し,正しい解を求める探索軌跡を含む応答を自動生成する。
  論文  参考訳（メタデータ） (2023-10-14T14:14:38Z)
• Alphazero-like Tree-Search can Guide Large Language Model Decoding and Training [37.79247073276239]
  ToT(Tree-of-Thought)やRAP(Reasoning via Planning)といった最近の研究は、LLMの推論能力を強化することを目的としている。 LLMのためのAlphaZeroライクな木探索学習フレームワーク(TS-LLM)を提案する。 学習価値関数を用いた木探索がLLM復号を導出する方法を示す。
  論文  参考訳（メタデータ） (2023-09-29T12:20:19Z)
• RNNs can generate bounded hierarchical languages with optimal memory [113.73133308478612]
  RNNは、自然言語構文の足場を反映した境界階層言語を効率的に生成できることを示す。 Dyck-($k$,$m$)は、よくネストされた括弧($k$型)と$m$バウンドされたネスト深さの言語である。 明示的な構成により,$O(m log k)$ hidden units の RNN がメモリの指数的削減に十分であることを示す。
  論文  参考訳（メタデータ） (2020-10-15T04:42:29Z)
• Recursive Top-Down Production for Sentence Generation with Latent Trees [77.56794870399288]
  自然および合成言語に対する文脈自由文法の生成特性をモデル化する。 潜伏二分木構造にN$の葉を持つ動的プログラミングアルゴリズムを提案する。 また,Multi30kデータセットを用いたドイツ語と英語の翻訳実験を行った。
  論文  参考訳（メタデータ） (2020-10-09T17:47:16Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。