En una noticia impactante para el mundo de las matemáticas, un grupo de antiguos alumnos de Tsinghua, con la ayuda de la IA, ha logrado demostrar 162 teoremas matemáticos que antes nadie había podido resolver. Lo que es aún más impresionante es que este agente inteligente, llamado LeanAgent, ¡incluso ha resuelto el problema de formalización de la conjetura de Freiman-Ruzsa de polinomios de Terence Tao! Esto nos hace reflexionar sobre cómo la IA está revolucionando completamente los métodos de investigación en ciencias básicas.
Como todos sabemos, los actuales modelos de lenguaje extenso (LLM) son, aunque impresionantes, en su mayoría estáticos, incapaces de aprender conocimientos nuevos en línea, y demostrar teoremas de matemáticas superiores es una tarea casi imposible. Sin embargo, LeanAgent, desarrollado conjuntamente por equipos de investigación del Instituto Tecnológico de California, la Universidad de Stanford y la Universidad de Washington, es un asistente de IA con capacidad de aprendizaje permanente, capaz de aprender y demostrar teoremas continuamente.
LeanAgent utiliza una ruta de aprendizaje cuidadosamente diseñada para abordar diferentes niveles de dificultad matemática, utilizando una base de datos dinámica para gestionar un flujo constante de conocimientos matemáticos, garantizando que no olvida las habilidades ya adquiridas al aprender cosas nuevas. Los experimentos demuestran que ha logrado demostrar 162 teoremas matemáticos previamente irresueltos a partir de 23 repositorios de código Lean diferentes, con un rendimiento 11 veces superior al de los grandes modelos tradicionales. ¡Simplemente asombroso!
Estos teoremas abarcan numerosos campos de las matemáticas superiores, incluyendo problemas complejos de álgebra abstracta y topología algebraica. LeanAgent no solo puede abordar conceptos simples para luego superar temas complejos, sino que también muestra un rendimiento excelente en estabilidad y transferencia inversa.
Sin embargo, el desafío de Terence Tao sigue siendo un obstáculo para la IA. Aunque los probadores interactivos de teoremas (ITP), como Lean, juegan un papel importante en la formalización y verificación de demostraciones matemáticas, construir este proceso de demostración suele ser complejo y lento, requiriendo pasos meticulosos y una gran cantidad de bibliotecas de código matemático. Incluso modelos avanzados como o1 y Claude cometen errores con demostraciones no formalizadas, lo que pone de manifiesto las deficiencias de los LLM en cuanto a la precisión y fiabilidad de las demostraciones matemáticas.
Estudios anteriores han intentado utilizar LLM para generar pasos de demostración completos. Por ejemplo, LeanDojo es un demostrador de teoremas creado entrenando grandes modelos en un conjunto de datos específico. Sin embargo, los datos para la demostración formal de teoremas son extremadamente escasos, lo que limita la aplicabilidad generalizada de este método. Otro proyecto, ReProver, es un modelo optimizado para la biblioteca de código de demostración de teoremas Lean mathlib4. Si bien abarca más de 100.000 teoremas y definiciones matemáticas formalizadas, se limita al ámbito de las matemáticas de grado universitario, por lo que su rendimiento es deficiente ante problemas más complejos.
Cabe destacar que la naturaleza dinámica de la investigación matemática plantea un desafío aún mayor para la IA. Los matemáticos suelen trabajar simultáneamente o alternativamente en varios proyectos. Terence Tao, por ejemplo, trabaja en varios campos de investigación al mismo tiempo, incluyendo la conjetura PFR y la media simétrica de números reales. Estos ejemplos muestran una deficiencia clave en los métodos actuales de demostración de teoremas de IA: la falta de un sistema de IA capaz de aprender y mejorar de forma adaptativa en diferentes campos de las matemáticas, especialmente con datos Lean limitados.
Por ello, el equipo de LeanDojo creó LeanAgent, un nuevo marco de aprendizaje permanente diseñado para resolver estos problemas. El flujo de trabajo de LeanAgent incluye la deducción de la complejidad de los teoremas para elaborar un plan de estudios, el entrenamiento gradual para equilibrar la estabilidad y la flexibilidad durante el aprendizaje, y la búsqueda de árbol de prioridad óptima para encontrar teoremas aún no demostrados.
LeanAgent se utiliza con cualquier gran modelo, utilizando la "recuperación" para mejorar su capacidad de generalización. Su innovación radica en el uso de una base de datos dinámica personalizada para gestionar el creciente conocimiento matemático, y en una estrategia de aprendizaje basada en la estructura de demostración de Lean, que facilita el aprendizaje de contenidos matemáticos más complejos.
Para abordar el problema del olvido catastrófico de la IA, los investigadores utilizaron un método de entrenamiento gradual que permite a LeanAgent adaptarse continuamente a nuevos conocimientos matemáticos sin olvidar los conocimientos previos. Este proceso implica un entrenamiento incremental en cada nuevo conjunto de datos, asegurando un equilibrio óptimo entre estabilidad y flexibilidad.
Gracias a este entrenamiento gradual, LeanAgent ha demostrado un rendimiento excelente en la demostración de teoremas, logrando demostrar 162 problemas aún no resueltos por humanos, especialmente en los desafiantes teoremas de álgebra abstracta y topología algebraica. Su capacidad para demostrar nuevos teoremas es 11 veces superior a la de ReProver, un modelo estático, y mantiene su capacidad para demostrar teoremas conocidos.
LeanAgent ha demostrado las características del aprendizaje gradual en el proceso de demostración de teoremas, pasando de teoremas simples a teoremas más complejos, lo que demuestra la profundidad de su comprensión del conocimiento matemático. Por ejemplo, ha demostrado teoremas de estructuras algebraicas básicas relacionadas con la teoría de grupos y la teoría de anillos, mostrando una profunda comprensión de las matemáticas. En general, LeanAgent, con su potente capacidad de aprendizaje continuo y mejora, ofrece perspectivas emocionantes para el mundo de las matemáticas.
Enlace al artículo: https://arxiv.org/pdf/2410.06209
