El sistema AlphaProof de DeepMind resolvi\u00f3 cuatro de seis problemas en la Olimpiada Internacional de Matem\u00e1ticas 2024, generando demostraciones formalmente verificadas mediante aprendizaje por refuerzo entrenado con millones de problemas autoformalizados. Ese resultado, reportado en un estudio reciente en Nature, se\u00f1ala un cambio m\u00e1s amplio. La inteligencia artificial no solo est\u00e1 ayudando a los matem\u00e1ticos, sino que est\u00e1 reformando activamente la mec\u00e1nica de c\u00f3mo se redactan, verifican y descubren las demostraciones.<\/p>\n
AlphaProof se inspira en AlphaZero, el agente jugador que domin\u00f3 el ajedrez y el Go. Pero en lugar de posiciones de tablero, explora estados formales de prueba en el asistente de demostraciones Lean. El sistema aprende a encontrar demostraciones formales mediante aprendizaje por refuerzo, entrenando con millones de problemas que fueron traducidos autom\u00e1ticamente al lenguaje matem\u00e1tico formal. Cada prueba candidata es comprobada por un motor de verificaci\u00f3n, creando un bucle de retroalimentaci\u00f3n en el que el modelo mejora al confirmar qu\u00e9 pasos de razonamiento realmente se sostienen.<\/p>\n
El desempe\u00f1o en la IMO 2024 es llamativo porque los problemas de competici\u00f3n se sit\u00faan en el l\u00edmite de lo que los competidores humanos entrenados pueden manejar bajo presi\u00f3n de tiempo. AlphaProof oper\u00f3 en un entorno formal, lo que significa que cada paso que produjo era verificable por m\u00e1quina en lugar de basarse en los saltos intuitivos que caracterizan las demostraciones manuscritas. Esa distinci\u00f3n importa. Una demostraci\u00f3n verificada formalmente no deja huecos para errores ocultos, que es exactamente el est\u00e1ndar que los matem\u00e1ticos esc\u00e9pticos exigen antes de confiar en un razonamiento generado por una m\u00e1quina.<\/p>\n
El pipeline de entrenamiento de AlphaProof tambi\u00e9n sugiere c\u00f3mo podr\u00edan construirse los sistemas futuros. Al autoformalizar un gran n\u00famero de problemas y luego usar aprendizaje por refuerzo para navegar el espacio de b\u00fasqueda resultante, los desarrolladores sortearon la escasez de demostraciones formales escritas a mano. El sistema aprendi\u00f3 efectivamente una pol\u00edtica para la construcci\u00f3n de pruebas, guiada no por demostraciones humanas sino por las r\u00edgidas restricciones de un verificador de pruebas. En ese sentido, la demostraci\u00f3n en la IMO es menos un truco publicitario y m\u00e1s una prueba de que la b\u00fasqueda de pruebas formales puede escalar hasta matem\u00e1ticas genuinamente desafiantes.<\/p>\n
AlphaProof no es el \u00fanico sistema que empuja estos l\u00edmites. AlphaGeometry, publicado como un estudio revisado por pares en Nature, present\u00f3 un marco neuro-simb\u00f3lico<\/a> que empareja un modelo de lenguaje neuronal entrenado con datos sint\u00e9ticos con un motor de deducci\u00f3n simb\u00f3lica. El componente neuronal propone construcciones geom\u00e9tricas y pasos intermedios, mientras que el motor simb\u00f3lico hace cumplir la consistencia l\u00f3gica verificando cada movimiento deductivo. Esta divisi\u00f3n del trabajo permite al modelo explorar ideas geom\u00e9tricas creativas sin sacrificar el rigor del razonamiento formal.<\/p>\n Su sucesor, AlphaGeometry2, ampli\u00f3 este enfoque y fue evaluado en conjuntos hist\u00f3ricos de problemas de geometr\u00eda de olimpiadas. Seg\u00fan un preprint en arXiv<\/a>, el sistema igual\u00f3 el rendimiento de los mejores medallistas de oro humanos, resolviendo una fracci\u00f3n comparable de problemas en condiciones similares, y lo hizo sin depender de trazas de soluciones humanas durante el entrenamiento. Ese resultado sugiere que, al menos en dominios estructurados como la geometr\u00eda euclidiana, la IA puede internalizar heur\u00edsticas de resoluci\u00f3n de problemas que antes se consideraban requer\u00edan a\u00f1os de pr\u00e1ctica humana especializada.<\/p>\n En el lado de la combinatoria, FunSearch sigui\u00f3 un camino diferente. En lugar de demostrar teoremas directamente, emple\u00f3 un modelo de lenguaje grande dentro de un bucle de b\u00fasqueda evolutiva para generar programas candidatos, que luego fueron evaluados por su calidad matem\u00e1tica. Este enfoque, descrito en un art\u00edculo de Nature sobre nuevas construcciones combinatorias<\/a>, produjo ejemplos novedosos de conjuntos cap y heur\u00edsticas mejoradas para el problema del empaquetamiento. El punto clave es que el sistema descubri\u00f3 objetos matem\u00e1ticos y algoritmos que no hab\u00edan sido catalogados previamente por humanos, subrayando que los modelos generativos pueden aportar ideas genuinamente nuevas en lugar de limitarse a remezclar las existentes.<\/p>\n A pesar de estos avances, un desaf\u00edo persistente es la brecha entre c\u00f3mo piensan los matem\u00e1ticos y c\u00f3mo funcionan los asistentes de pruebas. Las soluciones escritas por humanos, especialmente al nivel de las olimpiadas, a menudo se basan en ideas de alto nivel, sustituciones ingeniosas y diagramas informales. Convertir ese razonamiento en una prueba verificable por m\u00e1quina suele requerir descomponer el argumento en muchos lemas peque\u00f1os, cada uno expresado en la sintaxis r\u00edgida de un asistente de pruebas. Un reciente an\u00e1lisis en arXiv<\/a> de problemas de olimpiadas encontr\u00f3 que una sola pregunta de competici\u00f3n puede expandirse a docenas de pasos formales cuando se traduce a Lean, lo que ilustra lo r\u00e1pido que explota la complejidad.<\/p>\n Este proceso de descomposici\u00f3n es laborioso, y la escasez de corpus formales grandes y de alta calidad ha limitado la rapidez con la que los demostradores neuronales pueden mejorar. DeepSeek-Prover, un sistema centrado en la autoformalizaci\u00f3n para las matem\u00e1ticas formales, apunta directamente a este cuello de botella al traducir afirmaciones matem\u00e1ticas informales a formales a gran escala. Al generar pares alineados de texto informal y formal, tales sistemas aspiran a crear los datos de entrenamiento que los modelos de lenguaje modernos necesitan para aprender estrategias de prueba robustas.<\/p>\n Por su parte, Lean-STaR adopta otro enfoque: en lugar de insistir en razonamientos puramente formales desde el principio, su modelo genera comentarios informales intercalados con pasos de prueba en Lean. Este estilo mixto ha mostrado un mejor rendimiento en el benchmark miniF2F, que agrega problemas de competiciones como la AMC, AIME y la IMO en m\u00faltiples asistentes de pruebas. La idea es que permitir que el modelo \u201cpiense en voz alta\u201d en lenguaje natural puede guiarlo hacia mejores jugadas formales, al igual que los matem\u00e1ticos humanos bosquejan ideas en prosa antes de llevarlas al rigor completo.<\/p>\nEl cuello de botella de la formalizaci\u00f3n<\/h2>\n
Los matem\u00e1ticos son cautelosos por buenas razones<\/h2>\n