Durante la Olimpiada Internacional de Matemáticas de 2024, un participante sorprendió a todos al lograr resultados dignos de una medalla de plata. No era un adolescente genio ni un prodigio desconocido. Era una inteligencia artificial desarrollada por Google DeepMind, conocida como AlphaProof. Aunque las reglas del certamen impiden que una máquina reciba una medalla, su desempeño dejó claro que las fronteras entre el razonamiento humano y el artificial están cambiando rápidamente.Más que cálculos: precisión lógica absolutaA diferencia de muchos modelos de lenguaje actuales que pueden resolver ecuaciones o responder preguntas matemáticas, AlphaProof no se conforma con llegar a una solución. Su principal virtud es que sus respuestas están garantizadas como 100% correctas, gracias a un entorno de trabajo especial llamado Lean. Este sistema, originalmente desarrollado por Microsoft Research, actúa como un severo profesor que revisa cada paso del razonamiento matemático.En el mundo de la inteligencia artificial, lograr respuestas correctas no siempre significa entender el problema. Muchos modelos ofrecen soluciones plausibles, pero sus fundamentos lógicos pueden tambalearse si se los analiza con lupa. Lean evita este problema, porque no solo ejecuta, sino que verifica rigurosamente cada paso. Como quien revisa una receta paso a paso y asegura que no se ha olvidado ni un solo ingrediente, AlphaProof no da nada por supuesto.El proceso de entrenamiento: aprender como un estudiante brillanteCrear una IA capaz de razonar como un matemático de élite requirió un entrenamiento en tres fases, similar al camino de aprendizaje de un estudiante que pasa de la educación básica al doctorado.Primero, se le expuso a 300.000 millones de tokens de textos que combinaban código y matemáticas, lo que le permitió adquirir una comprensión general del lenguaje formal y la lógica. Esto fue como aprender el idioma en el que están escritas las matemáticas.Luego vino la práctica guiada. AlphaProof estudió 300.000 demostraciones matemáticas previamente verificadas en Lean. En este punto, se trataba de aprender observando a los expertos: ver cómo otros resolvieron problemas complejos, asimilar patrones, estructuras y estrategias.Pero el salto más importante llegó con la práctica autónoma. Se le asignó una gigantesca tarea de resolver 80 millones de problemas matemáticos formales por sí mismo. Utilizando aprendizaje por refuerzo (Reinforcement Learning), la IA era recompensada cada vez que lograba una prueba exitosa. Como un estudiante que prueba distintas estrategias hasta encontrar la mejor, AlphaProof fue descubriendo nuevas formas de razonar, sin copiar directamente a los humanos.Una estrategia para lo imposible: Test-Time RLCuando se enfrenta a problemas especialmente complejos, AlphaProof usa una técnica llamada Test-Time Reinforcement Learning (TTRL). Esta estrategia consiste en crear millones de versiones simplificadas del problema original, resolviéndolas una a una hasta encontrar un camino que sirva para abordar el caso real.Es como si un alpinista, antes de escalar una montaña gigantesca, entrenara subiendo colinas de distinta dificultad hasta encontrar la mejor ruta. Esta capacidad de experimentar con versiones reducidas del reto permite a AlphaProof encontrar soluciones que incluso expertos humanos podrían tardar años en alcanzar.Una herramienta para la comunidad matemáticaMás allá del impacto en olimpiadas o competencias, el valor de AlphaProof está en su aplicación práctica para matemáticos e investigadores. Puede actuar como un asistente que no solo resuelve problemas, sino que detecta errores en demostraciones existentes o ayuda a desarrollar nuevas teorías.En campos donde una equivocación mínima puede invalidar años de trabajo, contar con una herramienta que valida la solidez de una prueba con absoluta certeza es revolucionario en términos de eficiencia y confiabilidad. No sustituye la creatividad humana, pero puede potenciarla al eliminar errores y sugerir caminos alternativos.El inicio de una nueva etapa en la matemática formalLos investigadores que lideraron este proyecto, publicado en la revista Nature, destacan que este avance demuestra que el aprendizaje a gran escala basado en la experiencia formal puede producir sistemas con estrategias de razonamiento muy complejas.A diferencia de otros modelos que simplemente imitan patrones de texto, AlphaProof razona de forma estructurada, con pasos que pueden ser seguidos, revisados y comprendidos. En cierto sentido, transforma la intuición difusa de otros sistemas en pensamiento matemático transparente.Esto podría marcar el inicio de una nueva forma de hacer matemáticas, donde humanos y máquinas colaboran como colegas: uno aporta la creatividad, el otro garantiza la precisión. Y quizá, en un futuro no tan lejano, AlphaProof o sus sucesores contribuyan a resolver conjeturas que llevan siglos esperando una solución.La noticia Una IA que no se equivoca: así es AlphaProof, la mente matemática de DeepMind fue publicada originalmente en Wwwhatsnew.com por Natalia Polo.