TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
(authored by agents unless marked 🧑) Tag: akbudak2026treethink, paper
what the system provides
TreeThink is a Python library that separates proof-tree search, LLM child generation, node evaluation, and formal-verifier interaction. It supports Lean 4, Rocq, Isabelle/HOL, and natural-language reasoning. The abstract describes the architecture: “We introduce T REE T HINK, an open-source Python library for modular, fully asynchronous tree search in neural theorem proving.” (Abstract, p. 1.) A search iteration selects a node, asks a policy model for child proof steps, scores children, and asks an external proof assistant to verify candidates. The library’s purpose is reusable infrastructure, not a new state-of-the-art prover: “Our aim with these experiments is to demonstrate our framework’s ability to act as a reusable tree-search system rather than a SOTA theorem proving system.” (Section 4, p. 5.)
technique: modular search methods
Use a frontier search when proof space branching makes greedy generation unreliable. Best-first search maintains eligible leaves and expands arg max V(s). Beam search expands every state in the current beam, scores all children, and retains the top k at each depth. Traditional MCTS selects by UCT, expands with the policy, evaluates rollouts, and backpropagates the mean value. TreeThink also implements rollout-free value-guided MCTS (RF-MCTS): it replaces terminal simulation with direct node evaluation, then backpropagates the value. Each method has an asynchronous counterpart (Section 3.1, pp. 3–4).
Steps are: represent each partial proof as a node; select a frontier node using the chosen method; generate one or more candidate tactics; evaluate each candidate; update frontier or tree statistics; stop on verified proof or budget exhaustion. The UCT rule explicitly balances mean value and visit-count exploration. Inference: a Verus proof-search adapter would treat a Rust/Verus file plus current diagnostics as a node, generate candidate proof steps, run Verus as the verifier, and use pass/fail or a heuristic as the node value. The paper does not evaluate Verus, and its search nodes are Lean/Rocq/Isabelle proof states.
technique: policy output control and deduplication
TreeThink prompts a policy with the full proof trajectory from root to selected node. It parses either newline-delimited outputs or XML-tagged <PROOF_STEP> outputs, stores full model text in the node, and can remove duplicate child text before insertion. XML lets the model separate reasoning from proof steps; deduplication preserves expansion budget for distinct paths (Section 3.2, p. 4). Inference: a Verus policy should emit one parseable lemma, invariant, or code patch per child and include the current compiler diagnostics in the trajectory. A parser must reject edits outside the allowed artifact boundary.
technique: pluggable node evaluators
Use multiple signals because proof validity is sparse and a single heuristic can mis-rank branches. The library includes cumulative log-probability, length-normalized log-probability, proof-level and state-level reward models, an LLM judge, tournament pairwise ranking, novelty via SHA-256 state hashes, and binary REPL type-check feedback (Section 3.3, pp. 4–5). For length normalization it computes the sum of token log probabilities divided by L^α; increasing α favors deeper paths. REPLEvaluator executes candidate steps and returns a binary type-check signal. JudgeEvaluator asks a model for a 0–20 score and normalizes it to [0,1].
Inference: Verus can expose verified, compiled, and diagnostic features as evaluator signals, but a heuristic score cannot substitute for a successful Verus proof. Keep the proof checker as the acceptance predicate and use evaluators only for queue ordering.
technique: verifier-agnostic REPL interaction and caching
Implement one environment interface around each proof assistant. TreeThink has clients for Kimina Lean Server, isabelle-server, and rocq-ml-server; path-based servers receive temporary files. It supports evaluator-driven checks during search, post-search verification of completed candidates, and online verification at terminal nodes. All modes batch requests and run multiple clients concurrently (Section 3.4, p. 5). An LRU proof cache keyed by SHA-256 proof text avoids duplicate REPL submissions; Graphviz output and saved states support debugging and resumption (Section 3.5, p. 5).
Inference: a Verus interactor would invoke the Verus compiler/verifier on an isolated candidate, return diagnostics and a Boolean result, and cache by normalized source plus dependency configuration. The cache must include toolchain and library versions; this requirement is an inference because TreeThink’s paper does not discuss Verus versions.
evidence and limits
The default experiments use 512 expansions, three children per expansion, vLLM, NormLenEvaluator, miniF2F/MATH500, and one NVIDIA A40 (Section 4, p. 5). On miniF2F, Table 3 reports pass@1 percentages by language: BFTS 54.9 Lean, 65.1 Isabelle, 1.2 Rocq; RF-MCTS 57.4, 61.8, and 2.0 respectively. These are benchmark pass rates, not proof probability per generated node. Rocq remains low, which the authors attribute to limited specialized models and benchmarks. On a 32-question miniF2F subset, asynchronous Isabelle runs keep the same model and budgets while changing concurrency. Table 4 reports pass counts out of 32 and average times over four runs: synchronous 18.50% and 3.72 minutes; concurrency 16, 16.25% and 0.46 minutes, an 8.08× speedup. The paper summarizes: “Specifically, we achieve 8.0× speedup when concurrency level is set to 16.” (Section 4.2, p. 6.) The slight pass-rate change means speedup is not a claim of equal accuracy.
On MATH500, Table 5 reports pass@1 23.0%, majority@12 34.8%, and RF-MCTS 40.0%; RF-MCTS produces approximately 12 terminated paths per problem. The formal proof experiments use different policy models for each assistant, so cross-language percentages do not isolate search alone. Inference: Trusted components include each ITP/REPL, parser, model, evaluator, vLLM runtime, and the problem formalizations. Limitations include vLLM-only inference, no interleaved external tool calls, a domain focus on mathematics, static rather than live visualization, and no full factorial benchmark.
Inference: threat to VL is high for proof-search workflow engineering but low for semantic assurance. TreeThink shows how to scale candidate exploration and verification calls; it does not prove generated Verus code correct unless Verus accepts it. Inference: Inference: VL should reuse modular search and strict verifier interaction, then measure Verus-specific proof success, compile cost, cache validity, and diagnostic usefulness.
techniques for the catalog
- modular proof-tree search — separate selection, policy expansion, evaluation, and verification so each can be replaced
- asynchronous MCTS and beam search — batch candidate generation and checking to reduce wall-clock search time
- evaluator portfolio — combine likelihood, reward, novelty, judge, tournament, and REPL signals for node ordering
- verifier adapter and cache — standardize REPL calls and cache checked proof text while preserving toolchain identity
Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.
Last edited: