Seed-Prover de ByteDance: SOTA en Demostración Matemática Automatizada

Los Grandes Modelos de Lenguaje (LLM) han demostrado avances significativos en el razonamiento matemático, a menudo aprovechando sus capacidades de lenguaje natural para mejorar el rendimiento en puntos de referencia como MATH y AIME. Sin embargo, un desafío clave en el entrenamiento de estos modelos con aprendizaje por refuerzo (RL) es la dificultad de verificar la corrección de las pruebas en lenguaje natural, lo que normalmente requiere una revisión manual meticulosa de cada paso. Esta limitación obstaculiza la aplicación más amplia del RL en el desarrollo de modelos de demostración de teoremas matemáticos. Si bien lenguajes formales como Lean proporcionan verificación automática de la corrección, los probadores formales actuales basados en LLM aún encuentran limitaciones. Por ejemplo, los probadores a nivel de paso generan código de forma incremental, pero a menudo requieren un soporte estructural específico y tienen dificultades con el razonamiento de alto nivel.

En respuesta, el equipo Seed de ByteDance ha introducido Seed-Prover, un novedoso modelo de razonamiento de prueba completa estilo lema. Seed-Prover refina iterativamente las pruebas incorporando retroalimentación de Lean, utilizando lemas previamente establecidos y empleando la auto-resumir. Integra tres estrategias de inferencia especializadas en el momento de la prueba, lo que permite capacidades de razonamiento profundas y amplias para abordar problemas complejos, incluidos los encontrados en la Olimpiada Internacional de Matemáticas (OMI). Su innovación central radica en la adopción de un enfoque de prueba estilo lema, que centra el proceso de razonamiento en los lemas en lugar de los métodos tradicionales de generación de pruebas paso a paso o monolíticas de prueba completa. Complementando esto, también se presenta Seed-Geometry, un motor de razonamiento geométrico especializado diseñado para superar las limitaciones de Lean en el manejo de problemas geométricos.

La interacción entre Seed-Prover y Lean se facilita mediante un marco de aprendizaje por refuerzo multietapa y multitarea basado en VAPO. El conjunto de datos de entrenamiento combina conjuntos de datos disponibles públicamente con problemas formales internos de ByteDance. Se utiliza un componente de “proponente” para generar variaciones más simples de tareas difíciles, mientras que los problemas excesivamente simples (con tasas de prueba superiores al 25%) se excluyen. El backend de Seed-Geometry admite la generación de problemas a gran escala, habiendo identificado más de 230 millones de problemas únicos en siete días, lo que demuestra una mejora de ocho veces en la eficiencia de búsqueda. Aunque se entrenan modelos de política y valor separados, pruebas exhaustivas indicaron que los modelos de valor a veces podrían reducir el rendimiento debido a errores de estimación, lo que llevó a la adopción de la generación paso a paso con búsqueda en haz en configuraciones distribuidas.

Seed-Prover ha logrado resultados de vanguardia en varios puntos de referencia matemáticos. En la OMI 2025, Seed-Prover resolvió con éxito 5 de 6 problemas; específicamente, Seed-Geometry resolvió instantáneamente el Problema 2, y Seed-Prover derivó pruebas para los problemas restantes utilizando varias configuraciones de inferencia. En problemas anteriores de la OMI, probó 121 de 155 tareas, logrando una tasa de éxito del 78.1% en todos los niveles de dificultad. Este rendimiento incluye la resolución de 47 de 55 problemas fáciles, 47 de 56 problemas medianos y 27 de 44 problemas difíciles. Las tasas de éxito específicas por materia también fueron sólidas, con 72 de 85 en álgebra, 42 de 55 en teoría de números y 7 de 14 en combinatoria.

En el punto de referencia MiniF2F, los investigadores informaron una tasa de prueba del 99.6% tanto para los conjuntos de validación como de prueba bajo configuraciones medias, resolviendo con éxito problemas desafiantes como el OMI 1990 P3. Los resultados de PutnamBench mostraron una mejora significativa de 201 a 331 problemas resueltos de 657 al actualizar de configuraciones de inferencia ligeras a medias, lo que marca un notable salto de rendimiento sobre los sistemas de razonamiento matemático de nivel universitario anteriores. Si bien Seed-Prover resolvió 30 de 100 problemas de combinatoria en CombiBench, superando los métodos existentes, los resultados también destacaron los desafíos actuales en el razonamiento combinatorio. Además, Seed-Prover logró una tasa de éxito del 81.8% en MiniCTX-v2, demostrando fuertes capacidades de generalización más allá de los problemas específicos de la competencia y superando el 44.3% de la línea base o4-mini en Pass@8.

En resumen, el equipo Seed de ByteDance ha introducido Seed-Geometry y Seed-Prover, dos métodos de razonamiento formal que integran eficazmente las capacidades de los LLM. Seed-Geometry proporciona verificación acelerada y mecanismos de búsqueda mejorados para problemas geométricos, mientras que Seed-Prover utiliza refinamiento iterativo y estrategias complejas de inferencia en tiempo de prueba para pruebas matemáticas generales. El logro de resolver 5 de 6 problemas en la OMI 2025 subraya la eficacia práctica de estos métodos para abordar competiciones matemáticas de élite. La adopción de lenguajes formales como Lean proporciona una verificación rápida de pruebas que es más rentable que los expertos humanos y más confiable que los jueces basados en LLM. La investigación futura se centrará en combinar aún más los sistemas formales con los LLM para abordar conjeturas matemáticas abiertas.