En su conferencia de ayer "AlphaProof: When RL meets formal maths", Thomas Hubert de Google DeepMind presentó AlphaProof, un sistema de inteligencia artificial que aplica los principios del aprendizaje por refuerzo (RL, del inglés "Reinforcement learning") al dominio de las matemáticas formales. El concepto fundamental radica en que los asistentes de demostración como Lean proporcionan el entorno perfecto para el RL: un espacio de experimentación masiva con retroalimentación inequívoca (una prueba matemática es correcta o incorrecta, sin ambigüedades). Siguiendo el paradigma exitoso de sistemas como AlphaGo Zero, AlphaProof está diseñado para generar conocimiento matemático de forma autónoma, trascendiendo la mera imitación de demostraciones humanas preexistentes.

La arquitectura de AlphaProof se estructura en un proceso de múltiples fases que combina diferentes técnicas de aprendizaje automático. Inicialmente, emplea modelos de lenguaje para autoformalizar problemas matemáticos expresados en lenguaje natural hacia el código formal de Lean, generando así un extenso conjunto de datos de entrenamiento. Su modelo demostrador experimenta dos etapas: primero, un entrenamiento supervisado utilizando la biblioteca mathlib, seguido de un refinamiento intensivo mediante RL que resuelve millones de problemas matemáticos. Para desafíos particularmente complejos —como los de la Olimpiada Internacional de Matemáticas (IMO)—, el sistema implementa una estrategia de adaptación en tiempo real, generando y resolviendo múltiples variantes de un problema para desarrollar gradualmente la intuición necesaria.

Los resultados validan el potencial transformador de AlphaProof como herramienta matemática colaborativa. El sistema alcanzó una puntuación equivalente a una medalla de plata en la IMO y, durante una demostración en vivo durante la conferencia, asistió exitosamente a un matemático a completar los pasos de una prueba compleja relacionada con la función zeta de Riemann. Hubert enfatiza que el objetivo trasciende las competiciones académicas: la meta fundamental es contribuir significativamente a la investigación matemática contemporánea, convirtiendo AlphaProof en una útil para la comunidad matemática que facilite el descubrimiento y verificación de nuevas verdades matemáticas.