BFS-Prover-V2-32B for Ollama

Lean4 tactic generator built by ByteDance Seed — BFS-Prover-V2 pairs the Qwen2.5-32B backbone with multi-turn off-policy reinforcement learning and multi-agent best-first search. The model ingests Lean proof states and proposes the next tactic, enabling high-throughput tree search in automated theorem proving pipelines.

Highlights

• Training recipe: Multi-turn off-policy RL + multi-agent best-first search leveraging Mathlib (LeanDojo), curated Lean GitHub proofs, and autoformalized NuminaMath problems.
• Performance: 95.08% miniF2F solve rate when paired with the BFS tree-search planner; 41.4% ProofNet accuracy without planning.
• Prompt format: Provide the Lean proof state and append :::. The model replies with a single Lean tactic. Example:

  a b c : ℝ
  h₀ : 0 < a ∧ 0 < b ∧ 0 < c
  h₁ : c < a + b
  h₂ : b < a + c
  h₃ : a < b + c
  ⊢ a ^ 2 * (b + c - a) + b ^ 2 * (c + a - b) + c ^ 2 * (a + b - c) ≤ 3 * a * b * c:::

• Context window: 131,072 tokens — long enough to stage deep Lean proof branches.

Available Builds

Each tag shares the same prompt template and system message; pick the quant level that fits your GPU or CPU budget.

Usage with Ollama

Install the desired tag and stream Lean tactics:

ollama pull richardyoung/bfs-prover-v2-32b:Q5_K_M
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M <<'PROMPT'
a b c : ℝ
h₀ : 0 < a ∧ 0 < b ∧ 0 < c
h₁ : c < a + b
h₂ : b < a + c
h₃ : a < b + c
⊢ a ^ 2 * (b + c - a) + b ^ 2 * (c + a - b) + c ^ 2 * (a + b - c) ≤ 3 * a * b * c:::
PROMPT

Pair the model with a planner (e.g., Llemma agent or custom BFS/UCT search) to explore alternative branches and stitch full proofs.

Sources & References

• Paper: Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
• Original checkpoint: ByteDance-Seed/BFS-Prover-V2-32B
• Lean ecosystem: leanprover-community/mathlib4

License

Apache-2.0 (matches upstream release). Contact ran.xin@bytedance.com or zeyuzhen@andrew.cmu.edu for upstream inquiries.