Los grandes modelos de lenguaje (LLMs) han mejorado notablemente en razonamiento matemático mediante el uso del lenguaje natural, alcanzando mejores resultados en pruebas como MATH y AIME. Sin embargo, entrenar estos modelos con aprendizaje por refuerzo (RL) presenta un gran desafío: verificar la corrección de las demostraciones en lenguaje natural es complicado y requiere revisar manualmente cada paso del razonamiento. Esto limita el uso del RL en la formación de modelos para pruebas de teoremas matemáticos.
Aunque los lenguajes formales como Lean permiten verificar automáticamente la validez de las pruebas, los sistemas actuales basados en LLMs tienen limitaciones. Los demostradores que generan código paso a paso necesitan estructuras especiales y carecen de capacidades para razonamientos de alto nivel.
Para superar estas dificultades, el equipo Seed de ByteDance ha desarrollado Seed-Prover, un modelo que razona sobre pruebas completas siguiendo un estilo basado en lemas. Este sistema mejora las demostraciones de forma iterativa, apoyándose en la retroalimentación de Lean, lemas ya establecidos y la auto-resumición. Seed-Prover incorpora tres estrategias especializadas de inferencia en tiempo de prueba que le permiten aplicar métodos profundos y amplios para resolver problemas del nivel de las Olimpiadas Internacionales de Matemáticas (IMO). Su principal innovación es dar el protagonismo a los lemas en el proceso de razonamiento, en lugar de depender únicamente en la generación paso a paso o en la prueba completa de un solo tirón. Además, junto con Seed-Prover se presenta Seed-Geometry, un motor especializado en razonamiento geométrico que supera las limitaciones que tiene Lean para este tipo de problemas.
Para la interacción entre Seed-Prover y Lean se utiliza un aprendizaje por refuerzo multi-etapa y multi-tarea basado en VAPO. El conjunto de datos para el entrenamiento combina bases de datos públicas con problemas formales generados internamente, donde un generador crea versiones simplificadas de tareas complicadas y se excluyen problemas demasiado simples —con tasas de demostración por encima del 25%. El backend de Seed-Geometry permite generar problemas a gran escala, identificando más de 230 millones de problemas únicos en siete días y mejorando ocho veces la eficiencia de búsqueda. Aunque se entrena un modelo separado para política y valor, las pruebas muestran que el modelo de valor puede disminuir el rendimiento debido a errores en la estimación; por eso, finalmente se opta por la generación paso a paso con búsqueda en haz en configuraciones distribuidas.
Seed-Prover ha logrado resultados punteros en múltiples benchmarks matemáticos. Para la IMO 2025, resolvió completamente 5 de los 6 problemas; Seed-Geometry solucionó al instante el problema 2, mientras que Seed-Prover pudo derivar las demostraciones del resto utilizando distintas estrategias de inferencia. En problemas previos de la IMO, demostró 121 de 155 tareas, alcanzando un éxito del 78.1% en todos los niveles de dificultad. Detallando por categorías, resolvió 47 de 55 problemas fáciles, 47 de 56 de nivel medio y 27 de 44 difíciles; y por materia, 72 de 85 en álgebra, 42 de 55 en teoría de números y 7 de 14 en combinatoria.
En MiniF2F, alcanzó un 99.6% de tasa de demostración en conjuntos de validación y prueba en configuraciones medianas, resolviendo problemas complejos como el problema 3 de la IMO de 1990. En PutnamBench, mejoró los problemas resueltos de 201 a 331 de 657 al pasar de configuraciones ligeras a medianas, superando ampliamente a sistemas previos de razonamiento matemático a nivel universitario. En CombiBench, Seed-Prover resolvió 30 de 100 problemas combinatorios, sobresaliendo frente a otros métodos aunque reconoce que aún existen retos en razonamientos combinatorios. Además, logró un 81.8% de éxito en MiniCTX-v2, mostrando buena capacidad de generalización fuera de problemas competitivos y superando el 44.3% del modelo baseline o4-mini en Pass@8.
En resumen, ByteDance Seed presenta dos métodos formales que combinan las capacidades de los LLMs: Seed-Geometry, que acelera la verificación y mejora la búsqueda, y Seed-Prover, que utiliza refinamiento iterativo y estrategias complejas de inferencia. Resolver 5 de 6 problemas en la IMO 2025 demuestra la eficacia práctica de estos enfoques en competencias matemáticas de alto nivel. La adopción de lenguajes formales como Lean permite verificar pruebas rápidamente, de forma más económica que con expertos humanos y con mayor confiabilidad que los jueces basados en LLMs. En el futuro, el equipo planea integrar aún más los sistemas formales con LLMs para abordar conjeturas abiertas en matemáticas.
