En un reciente artículo de la revista Nature, se detalla el funcionamiento de un nuevo sistema de inteligencia artificial diseñado para resolver complejas teorías matemáticas. Este sistema, llamado AlphaProof y creado por Google DeepMind, ha logrado obtener resultados comparables a los de un ganador de medalla de plata en la Olimpiada Internacional de Matemáticas (IMO) del año 2024, considerado uno de los torneos más difíciles del mundo en este campo.
Google DeepMind, desde su creación, ha estado en la vanguardia de la inteligencia artificial, alcanzando logros significativos como el desarrollo de AlphaGo, el sistema que derrotó a los mejores jugadores humanos del antiguo juego de go. A diferencia de los primeros algoritmos que necesitaban datos y supervisión humana, DeepMind demostró que sus sistemas podrían aprender de forma autónoma usando el aprendizaje por refuerzo, tal como lo hizo AlphaGo Zero, que aprendió a jugar go sin intervención humana, solo con las reglas básicas del juego. Este método representó un avance importante, donde las máquinas no solo imitan las decisiones humanas sino que mejoran su capacidad de análisis y estrategia, anticipando movimientos y optimizando resultados mediante autoexperimentación.
La era matemática de la IA
AlphaProof utiliza el aprendizaje por refuerzo para probar proposiciones matemáticas, habiendo formalizado de manera automática más de 80 millones de proposiciones durante su fase de entrenamiento. Este sistema ha superado a modelos anteriores y ha resuelto cuatro de los seis problemas presentados en la IMO 2024, en colaboración con otro sistema de DeepMind, AlphaGeometry, que se especializa en geometría.
Tradicionalmente, los matemáticos han utilizado herramientas computacionales para resolver problemas y demostrar teoremas. Sin embargo, la implementación de sistemas de IA como AlphaProof introduce un cambio significativo: la capacidad de verificar automáticamente el razonamiento matemático. Hasta la fecha, grandes modelos de lenguaje habían mostrado potencial, pero enfrentaban el desafío de operar sobre texto en lenguaje natural, complicando la garantía de corrección lógica.
El equipo de DeepMind ha logrado integrar el aprendizaje por refuerzo en un entorno de software matemático formal llamado Lean, que permite generar demostraciones verificables de manera automática. Este desempeño habría sido suficiente para conseguir una medalla de plata, un logro sin precedentes para una IA en una competencia de tal calibre.
La indispensable colaboración humana
Para Carles Sierra, director del Instituto de Investigación en Inteligencia Artificial (IIIA-CSIC), AlphaProof “es un sistema robusto porque ofrece garantías formales de las pruebas y no presenta alucinaciones como los Grandes Modelos de Lenguaje [como ChatGPT]”.
“Este es un avance conceptual crucial: demuestra que los modelos de razonamiento pueden alcanzar la verificación formal, eliminando el riesgo de errores factuales que plagan a otros sistemas de inteligencia artificial», explica. No obstante, Sierra advierte sobre los riesgos: “Si el sistema formal (Lean) tiene axiomas inconsistentes, podría generar verdades ‘formales’ pero incorrectas matemáticamente. Es un gran progreso, pero requiere conocimiento técnico para ser utilizado correctamente”, afirma el investigador a Science Media Centre España (SMC).
Ramón López de Mántaras, pionero de la IA en España y profesor emérito del CSIC, señala que se trata de “un resultado excelente” que “muestra que los problemas que pueden ser formalizados mediante aprendizaje por refuerzo y con el apoyo de demostradores de teoremas, están empezando a ser accesibles para la inteligencia artificial”, según declaró a SMC.
Además, enfatiza en sus limitaciones: “Estos logros no implican que la IA sea comparable a un matemático, ya que no ‘comprende’ los conceptos matemáticos ni puede generar soluciones para problemas completamente nuevos. Lo que AlphaProof logra es expandir significativamente las herramientas automáticas que pueden ayudar a los matemáticos humanos, pero nunca reemplazarlos”, concluye.
Hola, soy María, parte del equipo de MuyMac. Me dedico a analizar las tendencias que marcan nuestro día a día, desde innovaciones tecnológicas hasta nuevas modas, para mantenerte siempre actualizado.
