treethink

• What is TreeThink?
• Core Concepts
• Installation
• Quick Start
• Documentation
• Extending TreeThink
• Project Structure
• License

TreeThink wraps an LLM-powered generation loop inside a tree search. Starting from a problem statement (root node), the system repeatedly:

1. Expands promising nodes by asking the LLM to generate candidate next proof steps (via Policies)
2. Scores each new node to estimate its quality (via Evaluators)
3. Selects the best node(s) for further expansion based on the search strategy (via Methods)
4. Terminates branches when a complete proof is found or a branch is exhausted (via Termination — REPL-based proof verification)

Methods determine how the search tree is explored. Each method inherits from BaseMethod and implements a simulate() loop.

All methods are available in sync and async variants (auto-converted via --async).

Detailed docs · treethink help methods

Policies wrap an LLM (via vLLM) to produce candidate next proof steps.

Detailed docs · treethink help policies

Evaluators assign scores to guide the search toward promising branches.

Detailed docs · treethink help evaluators

Two-phase verification system:

1. On encounter — verifies a proof immediately when a termination node is found during search (fast path)
2. On paths — batch-verifies all termination leaves after search completes (fallback)

Detailed docs · treethink help termination

Fully asynchronous tree search for maximum throughput. Auto-converts methods, policies, and evaluators to async equivalents when --async is passed.

➡️ Detailed docs · treethink help async

• Python 3.12+
• uv (package manager)

# Core only (vLLM + base utilities)
uv pip install treethink

# With Lean 4 support
uv pip install treethink[lean]

# With Rocq (Coq) support
uv pip install treethink[rocq]

# With Isabelle support
uv pip install treethink[isabelle]

# Everything (all languages + dev tools)
uv pip install treethink[full]

# Clone the repository
git clone https://github.com/GGLAB-KU/treethink.git
cd treethink

# Create a virtual environment and install everything for development
uv sync --all-extras

# Verify the CLI works
uv run treethink help --list

To install only a subset of extras during development:

# Core + Lean only
uv sync --extra lean

# Core + Rocq only
uv sync --extra rocq

• Lean 4: A running Kimina Lean server (typically http://localhost:8000).
• Rocq: A running rocq-ml-server on localhost:5000.
• Isabelle: Not yet available.

# config.yaml
treethink:
  method_name: "MCTS"
  max_children: 4
  expansion_count: 64
  timeout: 120
  termination_str: "```"
  language: "lean4"
  repl_args:
    lean_server_url: "http://localhost:8000"

policy:
  func_name: "vllm_policy"
  model:
    model: "internlm/internlm2-7b"
    tensor_parallel_size: 1
  sampling:
    max_tokens: 2048
    temperature: 1.0
    n: 4
    stop: ["\n"]

evaluator:
  func_name: "cumulative_logprob_evaluator"

# Sync mode
uv run treethink run --config config.yaml

# Async mode (auto-converts components)
uv run treethink run --config config.yaml --async

# With a dataset configuration
uv run treethink run \
  --config config.yaml \
  --data-config-path configs/dataset_configs.toml \
  --data-config-name my_experiment

# Inspect a saved tree
uv run treethink graph info output/tree_20240607_120000.txt

# Render to PNG
uv run treethink graph visualize output/tree_20240607_120000.txt \
  --output tree.png --format png

All documentation is available via the CLI and as markdown files in docs/.

# List all topics
treethink help --list

# Read a specific topic
treethink help methods
treethink help evaluators
treethink help termination
treethink help config

TreeThink is designed to be easily extended. Here is where to look:

For detailed instructions, see docs/extending.md or run treethink help extending.

treethink/
├── src/treethink/
│   ├── cli/              # CLI commands (run, help, graph)
│   │   ├── commands/     # Command implementations
│   │   └── helpers/      # Config parsing, iteration logic
│   ├── clients/          # REPL proof assistant clients
│   │   ├── lean/         # Lean 4 (Kimina)
│   │   ├── coq/          # Rocq (rocq-ml-server)
│   │   └── isabelle/     # Isabelle (not yet implemented)
│   ├── methods/          # Tree search algorithms
│   │   ├── mcts.py       # Monte Carlo Tree Search
│   │   ├── bfts.py       # Breadth-First Tree Search
│   │   └── beam.py       # Beam Search
│   ├── evaluators.py     # Node scoring
│   ├── policies.py       # Child generation
│   ├── termination.py    # Proof verification
│   ├── treethink.py      # Main orchestrator
│   └── sampler.py        # Batch processing
├── docs/                 # Documentation markdown files
├── examples/             # Example scripts and configs
├── tests/                # pytest test suite
├── pyproject.toml        # Project metadata and dependencies
└── ruff.toml             # Linter/formatter configuration

This project is licensed under the terms of the LICENSE file.

If you use TreeThink in your research, please consider citing: