Una red neuronal resolvió el 97 % de los problemas de olimpiadas; la clave de su éxito resultó ser inesperadamente simple.

La IA matemática logró un resultado casi impecable en una prueba estándar gracias a una técnica inesperada: la reducción de su propio historial de razonamiento. En el trabajo daVinci-Prover el modelo Qwen3.5 de 9 000 millones de parámetros resolvió el 97,1% de los problemas de MiniF2F con verificación automática de las pruebas. Los autores también informaron de una ganancia media de 13,7 puntos porcentuales tras una etapa especial de entrenamiento.

A diferencia de los sistemas que entregan la prueba completa, daVinci-Prover trabaja paso a paso. El agente busca los teoremas necesarios, anota fragmentos de la solución, envía el código a Lean 4 y corrige errores según los comentarios del programa verificador. El agente dispone de siete herramientas. El éxito solo se considera tras la verificación estricta de la afirmación original, y no por la apariencia convincente de la respuesta de la red neuronal.

Para el entrenamiento, el equipo reunió un corpus de 33 700 millones de tokens. En los ejemplos se muestra la búsqueda de enunciados intermedios, el análisis de errores, la comprobación de hipótesis y llamadas reales a herramientas. Luego los desarrolladores prepararon unas 36 000 cadenas de acciones exitosas para el ajuste adicional del modelo. Gracias a esa preparación la IA aprendió no solo las respuestas correctas, sino también el camino para llegar a ellas.

En Qwen3-8B la nueva metodología elevó la proporción de tareas resueltas de 73,4% a 85,3% en MiniF2F, de 68% a 85,3% en FATE-M y de 28,4% a 40,4% en ProofNet. La ganancia media fue de 13,7 puntos en los tres conjuntos con el mismo protocolo de pruebas. Además, un corpus de entrenamiento mayor no garantizó ventaja: el sistema superó a OProver-8B, entrenado con 65 000 millones de tokens.

El trabajo con la memoria del agente tuvo aún más impacto. Cuando el diálogo alcanzaba los 200 000 tokens, el sistema comprimía las acciones antiguas, conservando el enunciado, el código actual y los resultados de las comprobaciones. En este modo con compresión Qwen3.5-9B subió del 90,1% al 97,1% en MiniF2F. En el mucho más difícil FATE-H el mismo modelo obtuvo 28%, y la versión con 35 000 millones de parámetros alcanzó 42%.

Los desarrolladores publicaron por separado el código del entorno daVinci-Prover con acceso a las bibliotecas de Lean y la comprobación de resultados. En el repositorio se muestran otras pruebas, ya con DeepSeek-V4.1-Flash y un límite de 200 interacciones por tarea: 93% en FATE-H y 47% en FATE-X. También utilizaron una versión nueva de Lean. Estas cifras no pueden atribuirse al entrenamiento de Qwen, ya que el modelo y las condiciones del experimento difieren.

El 97,1% no implica que la IA pueda resolver por sí sola casi cualquier problema de olimpiada. MiniF2F contiene condiciones de problemas ya formalizadas previamente. Una auditoría independiente de 2025 encontró discrepancias entre el texto y las formalizaciones en más de la mitad de los ejercicios de la versión antigua. Leer el enunciado, traducirlo a Lean y la demostración posterior siguen siendo pruebas distintas.

El trabajo se presentó el 12 de noviembre como una publicación científica preliminar, y los resultados del entrenamiento aún no han recibido reproducción independiente. Los autores prometieron hacer públicos los datos de entrenamiento y los pesos de los modelos tras la finalización de la revisión anónima por pares. Esa verificación formal ya se aplica no solo en matemáticas, sino también al análisis del código y de los circuitos digitales.