Los investigadores del Departamento de Matemáticas del MIT, David Roe ’06 y Andrew Sutherland ’90, PhD ’07 se encuentran entre los receptores inaugurales de la Filantropía Renacimiento y la IA de los mercados XTX ‘para subvenciones matemáticas.
Cuatro alumnos adicionales del MIT: Anshula Gandhi ’19, Viktor Kunčak SM ’01, PhD ’07; Greaja Ranade ’07; y Damiiano Testa PhD ’05, también fueron perfeccionados para proyectos Settle.
Los primeros 29 proyectos ganadores apoyarán a los matemáticos e investigadores en universidades y organizaciones que trabajan para desarrollar sistemas de inteligencia artificial que ayuden a avanzar en el descubrimiento matemático e investigar 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 prueba de teorema automatizado mediante la construcción de conexiones entre las funciones L y la base de datos de formas modulares (LMFDB) y la Biblioteca Lean4 Mathematics (Mathlib).
«Los retrocesos automatizados del teorema están muy involucrados técnicamente, pero su desarrollo no tiene recursos», dice Sutherland. Con tecnologías de inteligencia artificial como modelos de idiomas grandes (LLM), la barrera de entrada para estas herramientas formales está disminuyendo rápidamente, lo que hace que los marcos de verificación formales sean accesibles para los matemáticos de trabajo.
Mathlib es una gran biblioteca matemática impulsada por la comunidad para el Lean Teorem Prover, un sistema formal que verifica la corrección de cada paso en una prueba. Mathlib actualmente contiene en el orden de 105 Resultados matemáticos (como lemas, proposiciones y teoremas). El LMFDB, un recurso en línea masivo y colaborativo que sirve como una especie de «enciclopedia» de la teoría de números modernos, contiene más de 109 declaraciones concretas. Sutherland y Roe son editores administrativos del LMFDB.
La subvención de Roe y Sutherland se utilizará para un proyecto que tiene como objetivo aumentar ambos sistemas, haciendo que los resultados del LMFDB estén disponibles dentro de Mathlib como afirmaciones que aún no se han demostrado formalmente, y proporcionando definiciones formales precisas de los datos numéricos almacenados dentro del LMFDB. Este puente beneficiará tanto a los matemáticos humanos como a los agentes de IA, y proporcionará un marco para conectar otras bases de datos matemáticas con sistemas formales de administración del teorema.
Los principales obstáculos para automatizar el descubrimiento matemático y la prueba son la cantidad limitada de conocimiento matemático formal, el alto costo de formalizar resultados complejos y la brecha entre lo que es accesible computacionalmente y lo que es factible para formalizar.
Para abordar estos obstáculos, los investigadores utilizarán la financiación para crear herramientas para acceder al LMFDB desde Mathlib, haciendo una gran base de datos de conocimiento matemático no formalizado accesible a un sistema de prueba formal. Este enfoque permite a los asistentes de prueba identificar objetivos específicos para la formalización sin la necesidad de formalizar por adelantado todo el corpus LMFDB.
«Hacer una gran base de datos de hechos teóricos numéricos no formalizados disponibles dentro de Mathlib proporcionará una técnica poderosa para el descubrimiento matemático, porque el conjunto de hechos que un agente podría desear considerar mientras busca un teorema o prueba es exponencialmente más grande que el conjunto de hechos que eventualmente deben formularse en realmente provocar la teórica», dice el ROE.
Los investigadores señalan que probar nuevos teoremas en la frontera del conocimiento matemático a menudo implica pasos que dependen de un cálculo no trivial. Por ejemplo, la prueba de Andrew Wiles del último teorema de Fermat usa lo que se conoce como el «truco 3-5» en un punto crucial de la prueba.
«Este truco depende del hecho de que la curva modular X_0 (15) tiene solo muchos puntos racionales, y ninguno de esos puntos racionales corresponde a una curva elíptica semi-estable», 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 modernos de álgebra por computadora, pero no es algo que uno pueda probar de manera realista usando lápiz y papel, ni es necesariamente fácil de formalizar».
Si bien los retrocesos formales del teorema se están conectando a los sistemas de álgebra por computadora para una verificación más eficiente, aprovechar las salidas computacionales en bases de datos matemáticas existentes ofrece varios otros beneficios.
El uso de resultados almacenados aprovecha los miles de años de CPU de tiempo de cálculo que ya ha pasado en la creación del LMFDB, ahorrando dinero que se necesitaría para rehacer estos cálculos. Tener información precomputada disponible también hace que sea factible buscar ejemplos o contraejemplos sin saber con anticipación cuán amplia puede ser la búsqueda. Además, las bases de datos matemáticas son repositorios seleccionados, no simplemente una colección aleatoria de hechos.
«El hecho de que los teóricos de los números enfatizaran el papel del conductor en las bases de datos de las curvas elípticas ya ha demostrado ser crucial para un descubrimiento matemático notable realizado con herramientas de aprendizaje automático: murmuraciones», dice Sutherland.
«Nuestros próximos pasos son construir un equipo, comprometerse con las comunidades LMFDB y Mathlib, comenzar a formalizar las definiciones que sustentan la curva elíptica, el campo numérico y las secciones de forma modular del LMFDB, y hacen que sea posible ejecutar búsquedas LMFDB desde Mathlib”, dice Roe. «Si eres un estudiante del MIT interesado en involucrarse, ¡no dudes en comunicarse!»
