La revista Nature describe en un artículo como funciona un sistema de inteligencia artificial capaz de demostrar teorías matemáticas complejas. El modelo, denominado AlphaProof y desarrollado por Google DeepMind, ha alcanzado una puntuación comparable a la de un medallista de plata en la Olimpiada Internacional de Matemáticas (IMO) de 2024, uno de los concursos más exigentes de este ámbito a nivel global.

PUBLICIDAD

Desde su fundación, Google DeepMind ha sido protagonista en el avance de la inteligencia artificial, logrando hitos históricos como el desarrollo de AlphaGo, el sistema capaz de vencer a los mejores jugadores humanos del milenario juego de go. Mientras los primeros algoritmos requerían la supervisión y los datos de expertos humanos, DeepMind demostró que sus sistemas podían aprender estrategias autónomas mediante aprendizaje por refuerzo, como demostró AlphaGo Zero, capaz de dominar el juego sin intervención humana, solo a partir de las reglas básicas. Este enfoque marcó un salto evolutivo: las máquinas no solo replican decisiones humanas, sino que potencian su capacidad analítica y estratégica, anticipándose a sus propios movimientos y optimizando resultados a través de la autoexperimentación. 

El turno de las matemáticas

El diseño de AlphaProof le permite demostrar enunciados matemáticos mediante aprendizaje por refuerzo, tras haber formalizado automáticamente más de 80 millones de enunciados utilizados en su entrenamiento. El sistema mejora los resultados de anteriores modelos de última generación y ha resuelto cuatro de los seis problemas de la Olimpiada de 2024, en combinación con otro sistema de DeepMind, AlphaGeometry, especializado en geometría.

Los matemáticos suelen utilizar herramientas computacionales para resolver problemas y demostrar teoremas, pero el uso de sistemas de IA introduce una novedad radical: la posibilidad de verificar automáticamente el razonamiento matemático. Hasta ahora, los grandes modelos de lenguaje habían mostrado cierto potencial, aunque con el obstáculo de operar sobre texto en lenguaje natural, donde la corrección lógica resulta difícil de garantizar.

El equipo de DeepMind ha conseguido integrar el aprendizaje por refuerzo en un entorno de software matemático formal, conocido como Lean, para generar demostraciones verificables de forma automática. Este rendimiento le habría permitido obtener una medalla de plata: un resultado inédito para una IA en una competición que enfrenta a algunos de los estudiantes más brillantes del mundo.

Los humanos, imprescindibles

Para Carles Sierra, profesor de investigación y director del Instituto de Investigación en Inteligencia Artificial (IIIA-CSIC), AlphaProof “parece un sistema potente porque da garantías formales de las pruebas, no ‘alucina’ como los Grandes Modelos de Lenguaje [como ChatGPT]”.

“Representa un avance conceptual fundamental: demuestra que los modelos de razonamiento pueden alcanzar la verificación formal, eliminando el riesgo de alucinaciones factuales que afecta a otros sistemas de inteligencia artificial”, explica. No obstante, Sierra advierte que el sistema no está exento de riesgos: “Si el sistema formal (Lean) contiene axiomas inconsistentes, puede producir verdades ‘formales’ pero matemáticamente falsas. Es un avance enorme, pero requiere dominio técnico para emplearlo con rigor”, asegura el investigador a Science Media Centre España (SMC).

Ramón López de Mántaras, profesor emérito del CSIC y pionero de la IA en España, considera que se trata de “un resultado excelente” que “demuestra que los problemas formalizables mediante aprendizaje por refuerzo y con apoyo de demostradores de teoremas comienzan a ser accesibles para la inteligencia artificial”, asegura en declaraciones a SMC.

Sin embargo, subraya también sus limitaciones: “ estos logros no significan que la IA sea comparable a un matemático, ya que no ‘entiende’ en absoluto los conceptos matemáticos ni puede crear soluciones para problemas completamente nuevos. Lo que AlphaProof demuestra es una notable ampliación de las herramientas automáticas que pueden asistir a los matemáticos humanos, pero nunca sustituirlos”, añade.

PUBLICIDAD