En el artículo «DeepMind’s latest: An AI for handling mathematical proofs», se presenta a AlphaProof, un sistema de inteligencia artificial capaz de razonar y realizar demostraciones matemáticas complejas. En la Olimpiada Internacional de Matemáticas de 2024, el sistema alcanzó el nivel de un medallista de plata, quedándose a un solo punto de obtener el oro.

El desafío del razonamiento lógico

Históricamente, los ordenadores han sido excelentes calculando, pero mediocres "entendiendo" la lógica necesaria para las demostraciones matemáticas. Los modelos de lenguaje actuales (como ChatGPT) funcionan mediante estadística y predicción de palabras, lo que a menudo resulta en respuestas que "suenan" bien pero son matemáticamente incorrectas. Para solucionar esto, DeepMind necesitaba un sistema que garantizase certeza absoluta.

Cómo funciona: La combinación de tres elementos

Para lograr este hito, AlphaProof combinó varias estrategias:

• Lenguaje formal (Lean): Utilizaron Lean, un software que permite escribir y verificar demostraciones matemáticas. Como había pocos datos de entrenamiento en este formato, usaron una versión de Gemini para traducir millones de problemas de lenguaje natural a Lean.

• Aprendizaje por refuerzo (Estilo AlphaZero): Emplearon una arquitectura similar a la que domina el ajedrez o el Go. Una red neuronal aprende mediante prueba y error, recompensando las demostraciones correctas y elegantes, combinada con un algoritmo de búsqueda en árbol para explorar posibles pasos lógicos.

• Aprendizaje en tiempo de prueba (TTRL): Esta es la gran innovación. Ante un problema muy difícil, la IA genera variaciones del mismo (algunas más simples, otras más generales) para "practicar" y aprender sobre la marcha, emulando cómo un humano intenta resolver versiones simplificadas de un problema antes de atacar el original.

Resultados

AlphaProof logró resolver el problema más difícil de la competición (el sexto), algo que solo consiguieron 6 de los 609 participantes humanos. En conjunto con AlphaGeometry 2 (que se encargó de un problema de geometría para el que AlphaProof no estaba optimizado), el sistema sumó 28 puntos.

Las limitaciones: Tiempo y coste

A pesar del éxito, el sistema tiene desventajas significativas frente a los humanos:

• Recursos desproporcionados: Mientras que los estudiantes tienen 4,5 horas por sesión, AlphaProof tardó días en resolver los problemas, utilizando una inmensa potencia de cálculo (cientos de días de procesamiento TPU).

• Coste prohibitivo: Actualmente, el coste de ejecutar este sistema es inviable para la mayoría de los investigadores.

• Dependencia humana: Los problemas tuvieron que ser traducidos manualmente a Lean antes de que la IA pudiera procesarlos.

El futuro

El objetivo de DeepMind no es ganar concursos como la IMO, sino optimizar esta tecnología para que sea menos costosa y pueda contribuir a la investigación matemática profesional, ayudando a descubrir nuevos conceptos en lugar de solo resolver los ya conocidos.