Skip to content
← Models
Open weightsByteDance Seed / Stanford University/10 trustVerified

BFS-Prover-V1-7B

A 7B Lean 4 tactic prover showing scaled best-first search beats MCTS — 72.95% on miniF2F with no critic network.

Visit official page →

About

BFS-Prover makes a contrarian bet: the theorem-proving field over-rotated to Monte Carlo tree search and learned critics, and plain best-first search, scaled properly, works better. The ByteDance Seed and Stanford team built an expert-iteration flywheel around a 7B Qwen2.5-Math policy model driving a LeanDojo environment, with three concrete tricks — filtering out beam-search-solvable problems each round, DPO on Lean compiler-error feedback, and length normalization so the search doesn't shy away from deep proofs.

It worked: 72.95% on the miniF2F test set, ahead of DeepSeek-Prover-V1.5, InternLM2.5-StepProver and HunyuanProver. Unlike whole-proof generators, it emits tactics step by step inside Lean, which makes its proofs easier to inspect and its failures easier to debug. The 7B model is open on Hugging Face under Apache 2.0.

Specs

Context window

Not officially published (Qwen2.5-Math-7B base)

Pricing

Free / open weights

Free quota

Fully open — no API

API access

No official API — self-host from Hugging Face (ByteDance-Seed/BFS-Prover-V1-7B)

Weights

Open weights

Released

Not disclosed

Benchmarks

  • Paper-reported (arXiv 2502.03438): 72.95% on miniF2F-test (accumulative), ahead of DeepSeek-Prover-V1.5 (63.5%), InternLM2.5-StepProver (65.9%) and HunyuanProver (68.4%)

Provider-reported unless a source says otherwise. Benchmarks are marketing-adjacent by nature — treat them as directional.

Use cases

theorem-provingformal-verificationlean4proof-search

Trust score — 8/10

/10 trustVerified

Scored 8/10 (TIER verified, metrics-v1). Evidence: paper (arXiv 2502.03438) from ByteDance Seed + Stanford with miniF2F-test comparisons against named baselines; Apache-2.0 license confirmed via HF API; open 7B weights. Strengths: clear methodological contribution, permissive license, tactic-level transparency. Docked for: (1) headline numbers are author-reported; (2) smaller community footprint than DeepSeek-Prover. License: Apache-2.0.

How the trust score is built

Full methodology →
Adoption · stars/downloads, log-scaled vs peers
7.0/10
Maintenance · recency, releases, issue load
7.0/10
Openness · license + docs
9.0/10
Manual review · sanity read + red-flag check
8.0/10
  • · ByteDance Seed + Stanford; released 2025-02-23
  • · Paper arXiv 2502.03438; 72.95% miniF2F-test vs named baselines
  • · Benchmarks are author-reported

Sources