Seed Prover от ByteDance — это специализированная ИИ-модель для решения сложнейших математических задач. На олимпиаде IMO 2025 нейросеть показала результат уровня серебряной медали, успешно справившись с формальными доказательствами и набрав 30 баллов.
By official invitation, the ByteDance Seed team participated in IMO (The International Mathematical Olympiad) 2025, deploying our specialized formal mathematical reasoning model, Seed Prover. After three days of sustained effort, Seed Prover fully solved 4 out of 6 problems and partially solved 1, receiving an IMO-certified score of 30 points, equivalent to a silver medal performance (scores per problem: 2/7/7/7/7/0). Our subsequent extended search efforts resulted in the successful completion of proofs for the first five problems. Seed Prover is constructed upon the Lean proof assistant and trained using multi-stage reinforcement learning. It guarantees the absolute reliability of mathematical proofs by facilitating interaction between natural language reasoning and formally verified code. Through extended chain-of-thought reasoning and computational scaling via multi-agent interaction, Seed Prover is capable of deeply analyzing individual mathematical problems continuously over several days. In addition to its outstanding performance at IMO, Seed Prover has achieved record-breaking outcomes on various benchmark tests for formal mathematical reasoning.