字节跳动Seed团队推出形式化数学推理专用模型Seed Prover 1.5

Core Insights - ByteDance's Seed team announced the launch of Seed Prover 1.5, a specialized model for formal mathematical reasoning, which claims significant improvements in reasoning capability and efficiency through large-scale Agentic RL training [1] Performance Metrics - Seed Prover 1.5 generated complete, compilable verification Lean proof code for the first five problems of IMO 2025 in 16.5 hours, achieving a score of 35 out of 42, which meets the gold medal threshold of the previous IMO scoring standard [1] - For the North American undergraduate mathematics competition Putnam, Seed Prover 1.5 took 9 hours to generate compilable verification Lean code for 11 out of 12 problems from the Putnam 2025 competition [1] Evaluation Results - In a comprehensive evaluation, Seed Prover 1.5 solved 88% of problems in the complete Putnam historical evaluation set, 80% in the Fate-H set representing master's level difficulty, and 33% in the Fate-X set representing doctoral level difficulty, setting new state-of-the-art (SOTA) performance for formal mathematical reasoning models in these evaluation sets [1] Future Developments - The technical report for Seed Prover 1.5 has been made public, and an API will be opened for interested mathematics and AI researchers to experience the model [1]