研究者らは、ニューラル定理証明におけるモジュール型かつ完全な非同期の木探索のために設計されたオープンソースのPythonライブラリであるTreeThinkを発表しました。これは、確立された探索手法とvLLMベースの推論パイプライン、および多様なノード評価技術を統合しています。

  • Lean~4、Rocq、Isabelle/HOL、自然言語推論をサポートします。
  • リアルタイム検証と証明状態の抽出のために、各言語のREPLサーバーに直接接続します。
  • miniF2FおよびMATH500ベンチマークにおいて、非同期実行により最大6.3倍のウォールクロックスピードアップを示しました。

このライブラリは、クロス言語形式証明検索と自然言語推論サポートを可能にし、ソースコードはMITライセンスの下で公開されています。