Los investigadores del Departamento de Matemáticas David Roe y Andrew Sutherland buscan avanzar en la demostración automatizada de teoremas; otros cuatro ex alumnos del MIT también recibieron el premio.
Los investigadores del Departamento de Matemáticas del MIT David Roe ’06 y Andrew Sutherland ’90, PhD ’07 se encuentran entre los primeros destinatarios de las subvenciones AI for Math de Renaissance Philanthropy y XTX Markets .
Cuatro exalumnos adicionales del MIT: Anshula Gandhi ’19, Viktor Kunčak SM ’01, PhD ’07; Gireeja Ranade ’07; y Damiano Testa PhD ’05, también fueron honrados por proyectos separados.
Los primeros 29 proyectos ganadores apoyarán a matemáticos e investigadores de universidades y organizaciones que trabajan para desarrollar sistemas de inteligencia artificial que ayuden a avanzar en el descubrimiento y la investigación matemática en varias tareas clave.
Roe y Sutherland, junto con Chris Birkbeck de la Universidad de East Anglia, utilizarán su subvención para impulsar la demostración automatizada de teoremas mediante la creación de conexiones entre la base de datos de funciones L y formas modulares (LMFDB) y la biblioteca de matemáticas Lean4 (mathlib).
“Los demostradores automáticos de teoremas son bastante complejos técnicamente, pero su desarrollo carece de recursos suficientes”, afirma Sutherland. Con tecnologías de IA como los grandes modelos de lenguaje (LLM), la barrera de entrada a estas herramientas formales está disminuyendo rápidamente, lo que hace que los marcos de verificación formal sean accesibles para los matemáticos en activo.
Mathlib es una gran biblioteca matemática, impulsada por la comunidad, para el demostrador de teoremas Lean , un sistema formal que verifica la corrección de cada paso de una demostración. Mathlib contiene actualmente alrededor de 10⁻¹ resultados matemáticos (como lemas, proposiciones y teoremas). La LMFDB, un recurso en línea masivo y colaborativo que funciona como una especie de «enciclopedia» de la teoría de números moderna, contiene más de 10⁻¹ enunciados concretos. Sutherland y Roe son los editores jefe de la LMFDB.
La subvención de Roe y Sutherland se destinará a un proyecto que busca ampliar ambos sistemas, haciendo que los resultados de la LMFDB estén disponibles en Mathlib como afirmaciones aún no demostradas formalmente y proporcionando definiciones formales precisas de los datos numéricos almacenados en la LMFDB. Esta conexión beneficiará tanto a matemáticos como a agentes de IA, y proporcionará un marco para conectar otras bases de datos matemáticas a sistemas formales de demostración de teoremas.
Los principales obstáculos para la automatización del descubrimiento y la demostración matemáticos son la cantidad limitada de conocimiento matemático formalizado, el alto coste de formalizar resultados complejos y la brecha entre lo computacionalmente accesible y lo factible de formalizar.
Para superar estos obstáculos, los investigadores utilizarán la financiación para desarrollar herramientas que permitan acceder a la LMFDB desde mathlib, lo que permitirá que una gran base de datos de conocimiento matemático no formalizado sea accesible a un sistema de prueba formal. Este enfoque permite a los asistentes de prueba identificar objetivos específicos para la formalización sin necesidad de formalizar previamente todo el corpus de la LMFDB.
“Hacer que una gran base de datos de hechos teóricos de números no formalizados esté disponible dentro de mathlib proporcionará una técnica poderosa para el descubrimiento matemático, porque el conjunto de hechos que un agente podría querer considerar mientras busca un teorema o una prueba es exponencialmente más grande que el conjunto de hechos que eventualmente necesitan formalizarse para realmente probar el teorema”, dice Roe.
Los investigadores señalan que demostrar nuevos teoremas en la frontera del conocimiento matemático a menudo implica pasos que dependen de un cálculo no trivial. Por ejemplo, la demostración del Último Teorema de Fermat de Andrew Wiles utiliza lo que se conoce como el «truco 3-5» en un punto crucial de la demostración.
“Este truco depende del hecho de que la curva modular X_0(15) tiene solo un número finito de puntos racionales, y ninguno de ellos corresponde a una curva elíptica semiestable”, según Sutherland. “Este hecho se conocía mucho antes del trabajo de Wiles y es fácil de verificar con las herramientas computacionales disponibles en los sistemas de álgebra computacional modernos, pero no es algo que se pueda demostrar de forma realista con lápiz y papel, ni es necesariamente fácil de formalizar”.
Si bien se están conectando demostradores formales de teoremas a los sistemas de álgebra computacional para una verificación más eficiente, aprovechar los resultados computacionales de las bases de datos matemáticas existentes ofrece otras ventajas.
El uso de resultados almacenados aprovecha los miles de años de CPU de tiempo de cálculo ya invertidos en la creación de la LMFDB, ahorrando el dinero que se necesitaría para rehacer estos cálculos. Disponer de información precalculada también permite buscar ejemplos o contraejemplos sin saber de antemano la amplitud de la búsqueda. Además, las bases de datos matemáticas son repositorios seleccionados, no simplemente una colección aleatoria de datos.
“El hecho de que los teóricos de números enfatizaran el papel del conductor en bases de datos de curvas elípticas ya ha demostrado ser crucial para un descubrimiento matemático notable realizado utilizando herramientas de aprendizaje automático: las murmuraciones ”, dice Sutherland.
“Nuestros próximos pasos son formar un equipo, colaborar con las comunidades de LMFDB y Mathlib, empezar a formalizar las definiciones que sustentan las secciones de curva elíptica, cuerpo numérico y forma modular de LMFDB, y posibilitar la ejecución de búsquedas en LMFDB desde Mathlib”, afirma Roe. “Si eres estudiante del MIT y te interesa participar, ¡no dudes en contactarnos!”
MIT News. S. M. Traducido al español
