8 3 weeks ago

ByteDance Seed’s BFS-Prover-V2 is a 32B Qwen2.5-based Lean4 tactic generator trained with multi-turn off-policy RL plus multi-agent best-first search on Mathlib, Lean GitHub, and NuminaMath.

1d748211adad · 50B
{
"num_ctx": 131072,
"temperature": 0.2,
"top_p": 0.95
}