¡Un equipo de exalumnos de Tsinghua logró impresionantes avances matemáticos con la ayuda de la IA! El LeanAgent que desarrollaron, un asistente de inteligencia artificial con capacidades de aprendizaje permanente, demostró con éxito 162 teoremas matemáticos no resueltos previamente e incluso resolvió el problema formal de la conjetura polinómica de Freiman-Ruzsa propuesta por Terence Tao. Esto no sólo demuestra el enorme potencial de la IA en la investigación científica básica, sino que también marca una innovación en los métodos de investigación matemática. Los editores de Downcodes le brindarán una comprensión profunda de este apasionante desarrollo y la innovación tecnológica detrás de LeanAgent.
En la última noticia sensacional en el mundo de las matemáticas, un grupo de exalumnos de la Universidad de Tsinghua utilizó el poder de la IA para demostrar con éxito 162 teoremas matemáticos que nadie había podido resolver antes. Lo que es aún más sorprendente es que este agente llamado LeanAgent en realidad superó el problema de formalización de la conjetura polinómica de Freiman-Ruzsa planteada por Terence Tero. ¡Esto nos hace lamentar que los métodos de investigación de la ciencia básica hayan sido completamente transformados por la IA!
Como todos sabemos, aunque los modelos de lenguaje actuales (LLM) son geniales, la mayoría de ellos todavía son estáticos y no pueden aprender nuevos conocimientos en línea. Es aún más difícil probar teoremas matemáticos avanzados. Sin embargo, LeanAgent, desarrollado conjuntamente por equipos de investigación de Caltech, la Universidad de Stanford y la Universidad de Washington, es un asistente de inteligencia artificial con capacidades de aprendizaje permanente que puede aprender y probar teoremas continuamente.
LeanAgent responde a diferentes dificultades matemáticas a través de rutas de aprendizaje cuidadosamente diseñadas y utiliza una base de datos dinámica para gestionar un flujo continuo de conocimientos matemáticos para garantizar que no olvide las habilidades que ya domina al aprender nuevos conocimientos. Los experimentos muestran que demostró con éxito 162 teoremas matemáticos que nadie había podido resolver antes a partir de 23 bibliotecas de códigos Lean diferentes, y su rendimiento es 11 veces mayor que el de los modelos grandes tradicionales. ¡Es realmente sorprendente!
Estos teoremas cubren muchas áreas de las matemáticas superiores, incluidos problemas difíciles como el álgebra abstracta y la topología algebraica. LeanAgent no sólo es capaz de comenzar con conceptos simples y abordar gradualmente temas complejos, sino que también demuestra un rendimiento excelente en términos de estabilidad y migración inversa.
Sin embargo, el desafío de Terence Tao todavía hace que AI se sienta impotente. Aunque los demostradores de teoremas interactivos (ITP), como Lean, desempeñan un papel importante en la formalización y verificación de pruebas matemáticas, el proceso de creación de dichas pruebas suele ser complejo y requiere mucho tiempo, y requiere pasos meticulosos y extensas bibliotecas de códigos matemáticos. Los modelos grandes avanzados como o1 y Claude también son propensos a errores cuando se enfrentan a pruebas informales, lo que resalta las deficiencias de LLM en la precisión y confiabilidad de las pruebas matemáticas.
Investigaciones anteriores han intentado utilizar LLM para generar pasos de prueba completos, como LeanDojo, que es un demostrador de teoremas creado entrenando un modelo grande 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 enfoque. Otro proyecto, ReProver, es un modelo optimizado para la biblioteca de códigos de demostración de teoremas Lean mathlib4. Aunque cubre más de 100.000 teoremas y definiciones matemáticos formales, está limitado al ámbito de las matemáticas de pregrado, por lo que no funciona bien cuando se enfrenta a temas más complejos. problemas.bueno.
Vale la pena señalar que la naturaleza dinámica de la investigación matemática plantea mayores desafíos a la IA. Los matemáticos suelen trabajar en varios proyectos al mismo tiempo o alternativamente. Por ejemplo, Terence Tao está avanzando en múltiples áreas de investigación al mismo tiempo, incluida la conjetura PFR y el promedio simétrico de números reales. Estos ejemplos muestran una deficiencia clave de los métodos actuales de demostración de teoremas de IA: la falta de un sistema de IA que pueda aprender y mejorar de forma adaptativa en diferentes campos matemáticos, especialmente cuando los datos Lean son limitados.
Es por eso que el equipo de LeanDojo creó LeanAgent, un nuevo marco de aprendizaje permanente diseñado para resolver los desafíos mencionados anteriormente. El flujo de trabajo de LeanAgent incluye derivar la complejidad de los teoremas para formular cursos de aprendizaje, equilibrar la estabilidad y la flexibilidad en el proceso de aprendizaje a través de una capacitación progresiva y utilizar la búsqueda de árbol del mejor primero para encontrar teoremas aún no probados.
LeanAgent trabaja con cualquier modelo grande para mejorar sus capacidades de generalización mediante "recuperación". Su innovación radica en el uso de una base de datos dinámica personalizada para gestionar el conocimiento matemático en constante expansión y una estrategia de aprendizaje del curso basada en una estructura de prueba Lean para ayudar a aprender contenido matemático más complejo.
Para abordar el catastrófico problema del olvido de la IA, los investigadores adoptaron un método de entrenamiento progresivo para permitir a LeanAgent adaptarse continuamente a nuevos conocimientos matemáticos sin olvidar el aprendizaje previo. Este proceso implica un entrenamiento incremental en cada nuevo conjunto de datos, lo que garantiza un equilibrio óptimo entre estabilidad y flexibilidad.
A través de este tipo de entrenamiento progresivo, LeanAgent tiene un excelente desempeño en la demostración de teoremas, demostrando con éxito 162 problemas difíciles que no han sido resueltos por humanos, especialmente en teoremas desafiantes de álgebra abstracta y topología algebraica. Su capacidad para demostrar nuevos teoremas es 11 veces mayor que la del ReProver estático, al tiempo que mantiene su capacidad para demostrar teoremas conocidos.
LeanAgent muestra las características del aprendizaje progresivo durante el proceso de demostración de teoremas, pasando gradualmente de teoremas simples a teoremas más complejos, demostrando su profundidad en el dominio del conocimiento matemático. Por ejemplo, demuestra una comprensión profunda de las matemáticas al demostrar teoremas fundamentales de estructura algebraica relacionados con la teoría de grupos y la teoría de anillos. En general, LeanAgent ofrece perspectivas interesantes a la comunidad matemática con sus poderosas capacidades de mejora y aprendizaje continuo.
Dirección del artículo: https://arxiv.org/pdf/2410.06209
La aparición de LeanAgent indica que la IA desempeñará un papel cada vez más importante en el campo de la investigación matemática, y es posible que en el futuro haya más casos que utilicen el poder de la IA para resolver problemas matemáticos complejos. Sin duda, esto abre una nueva dirección para la investigación matemática y también proporciona nuevas ideas y métodos para la exploración en otros campos científicos. ¡Esperamos obtener más resultados sorprendentes en el futuro!