Diseñan AlphaProof Nexus, una nueva herramienta de IA para abordar demostraciones matemáticas

Este trabajo muestra que una arquitectura abierta basada en agentes de inteligencia artificial (IA) ha sido capaz de resolver de forma autónoma nueve problemas abiertos de Erdős y 44 conjeturas de la On-Line Encyclopedia of Integer Sequences. Más allá de los resultados concretos, el valor de lo que presentan los autores es una metodología que permite producir descubrimientos matemáticos potentes de manera sistemática. Esta capacidad estaba prácticamente monopolizada por los laboratorios frontera.  

Desde principios de año hemos asistido a una sucesión de resultados cada vez más impresionantes obtenidos por la IA en matemáticas. La catarsis llegó en septiembre con el anuncio, no exento de polémica, de la resolución de uno de los ‘problemas del milenio’ (ecuaciones de Navier-Stokes) mediante modelos especializados en matemáticas y miles de agentes trabajando colaborativamente. Quedan ya pocas dudas que estamos asistiendo al nacimiento de una nueva forma de explorar y hacer matemáticas.  

Las capacidades matemáticas de los LLM [grandes modelos de lenguaje] han mejorado de manera espectacular. Ahora bien, como ha advertido Terence Tao en varias ocasiones, los objetivos de los laboratorios de IA y los de la comunidad científica no siempre están alineados. Estos primeros quieren resolver el mayor número de problemas para poner en valor su tecnología, mientras que la comunidad quiere aumentar su comprensión de las matemáticas. Tao señala que la automatización en la resolución de problemas puede ir en detrimento de la práctica profesional. El valor no está únicamente en conseguir demostrar un teorema, sino en todo el proceso que te lleva a conseguir la demostración. Según él, una IA elimina parte del conocimiento que normalmente produce un matemático al intentar resolver el problema, y este conocimiento es igual de valioso que la propia demostración para la práctica de las matemáticas.

Cuando leemos titulares sobre sistemas de inteligencia artificial (IA) "resolviendo problemas abiertos de matemáticas que llevaban décadas estancados", es fácil dejarse llevar por la narrativa del progreso inevitable. Sin embargo, al analizar con lupa los detalles técnicos del artículo sobre AlphaProof Nexus, publicado en Science por investigadoras e investigadores de Google DeepMind, nos encontramos con un patrón tristemente habitual en el panorama actual de la IA: una demostración deslumbrante de capacidad técnica empañada por importantes inconsistencias metodológicas y un severo problema de sobreingeniería.  

El artículo presenta a AlphaProof Nexus como un marco avanzado para la búsqueda de demostraciones formales en Lean. Los autores construyeron un agente ‘completo’ (Agente D) que combina un bucle básico de generación-verificación, integración con el probador AlphaProof mediante aprendizaje por refuerzo y un algoritmo evolutivo guiado por un sistema de votación y ratings Elo entre subagentes. Sobre el papel, la cifra impresiona: resolución autónoma de nueve problemas abiertos de la célebre lista de Erdős, 44 conjeturas del OEIS y descubrimientos aplicados en optimización y teoría de grafos.  

Pero cuando uno profundiza en la metodología y en el análisis post hoc del propio estudio, la estructura conceptual empieza a agrietarse.   

Primero. El propio análisis de ablación de los autores revela un dato demoledor: el Agente A (un bucle básico y simple tipo "Ralph loop" que alterna la generación del LLM con la verificación del compilador de Lean) replicó los mismos nueve problemas de Erdős que resolvió el sofisticado Agente D. ¿Qué nos dice esto? Que la complejidad del framework no es la que impulsa el descubrimiento; lo que realmente mueve la aguja es la capacidad base del LLM (en este caso, Gemini 3.1 Pro) combinada con el feedback directo e inflexible del compilador formal.  

Segundo. Desde una perspectiva de gestión de datos y recursos, la evaluación financiera del estudio es, como mínimo, opaca. En sus métricas de coste de inferencia (en USD), el estudio muestra que los agentes simplificados son más rentables en la mayoría de problemas, mientras que el Agente D solo justifica su coste en casos puntuales como Erdős #125. El artículo omite dos detalles relevantes: los cálculos solo contabilizan la inferencia en las ejecuciones exitosas y los costes reportados para los agentes B y D excluyen el coste de inferencia de AlphaProof.  

Tercero. Existe la falsa percepción de que, al utilizar un lenguaje formal como Lean, la ‘alucinación’ queda erradicada. Lean garantiza que la demostración es lógicamente válida para el enunciado escrito en Lean, pero no garantiza que dicho enunciado traduzca fielmente el problema matemático real. El artículo reconoce varios escenarios en los que los agentes alucinan y/o incurren en vulnerabilidades de formalización errónea. Esto demuestra que el sistema sigue necesitando una supervisión humana experta intensiva para validar que lo que el agente ha demostrado es realmente lo que se quería demostrar.  

La verdadera lección que nos deja este trabajo (aunque los autores intenten matizarla) es que el mercado y la investigación deben inclinarse hacia la simplicidad: bucles agénticos limpios, potentes modelos de lenguaje y entornos de retroalimentación estricta (compiladores, ejecuciones de código, pruebas unitarias y supervisión humana experta), aunque probablemente no al alcance de todas las universidades e institutos de investigación. Todo lo demás, de momento, son fuegos artificiales evolutivos que aportan más complejidad arquitectónica que resultados tangibles.

Por una parte, la incorporación de la IA a la investigación en matemáticas tiene un gran potencial y este potencial va a aumentar a medida que estas nuevas herramientas se van perfeccionando. Pero, por otra parte, también plantea preguntas muy importantes sobre muchos de los procesos asociados a la investigación, incluyendo la evaluación de resultados científicos, el uso de los datos que introducimos en los LLMs o la formación de jóvenes investigadores en la era de la IA.   

Por encima de todo, hay un tema de fondo muy importante sobre la comprensión de los resultados de investigación producidos. El objetivo principal (posiblemente único) de la investigación matemática es el avance del conocimiento matemático: la comprensión de los objetos y las estructuras, el desarrollo de nuevas teorías, etc. La resolución de problemas, por muy importantes que estos sean, es una medida de este avance, pero nunca el fin en sí mismo. Ahora nos encontramos en un momento histórico en el que se produce un cambio de paradigma curioso: la existencia de toda una batería de resultados que sabemos que son ciertos, porque vienen acompañados de una certificación de validez, pero que, en cambio, nadie comprende del todo.   

Como comunidad, debemos continuar insistiendo en la necesidad de comprender los avances que se realizan y también respetar y fomentar los espacios, las estructuras y los procesos que garanticen que esto sea posible.

El artículo es de buena calidad. Se trata de alimentar a modelos grandes de lenguaje (LLM) con lo que se denomina RAG (Generación Aumentada por Recuperación).  

Lo del RAG es lo que ha motivado que mejorasen en los últimos tiempos los no tan buenos resultados en sus inicios que proporcionó la IA generativa, como ChatGPT. A grandes rasgos, se crearon modelos especializados a base de entrenarlos con RAG especializados en ciertos ámbitos (por ejemplo, derecho, medicina, etc.). A partir de aquí, fue cuando se empezaron a ver resultados mucho mejores.  

Esto es lo mismo: se crea o se ajusta un modelo alimentado con demostraciones matemáticas, con la esperanza de que genere (IA generativa) resultados satisfactorios ante problemas nuevos o no vistos por el sistema. Según los autores, ha sido útil para algunos retos, pero ha fracasado para otros muchos.  

Por este motivo, creo que este artículo está bien como uno de los primeros intentos de aplicar la IA a la demostración matemática, pero los resultados dicen que hay todavía un gran margen de mejora en este campo.