La inteligencia artificial (IA) está transformando diversas disciplinas, y las matemáticas no son la excepción. Recientemente, investigadores del Departamento de Matemáticas del MIT, David Roe y Andrew Sutherland, han sido galardonados con las becas ‘AI for Math’ de Renaissance Philanthropy y XTX Markets. Este reconocimiento impulsa una nueva era en el descubrimiento matemático, prometiendo acelerar el avance en este campo crucial.
¿Qué son las becas ‘AI for Math’?
Estas becas están diseñadas para apoyar a matemáticos e investigadores en universidades y organizaciones que trabajan en el desarrollo de sistemas de inteligencia artificial. El objetivo principal es crear herramientas que ayuden a avanzar en el descubrimiento y la investigación matemática en diversas áreas clave.
En esta primera edición, se han seleccionado 29 proyectos ganadores, incluyendo el de Roe y Sutherland, junto con otros cuatro ex alumnos del MIT: Anshula Gandhi, Viktor Kunčak, Gireeja Ranade y Damiano Testa, quienes también fueron reconocidos por sus proyectos individuales.
Conectando el Universo del Conocimiento Matemático
Roe y Sutherland, en colaboración con Chris Birkbeck de la Universidad de East Anglia, utilizarán su beca para fortalecer la demostración automatizada de teoremas. Su enfoque principal es construir conexiones entre la Base de Datos de Funciones L y Formas Modulares (LMFDB) y la biblioteca matemática Lean4 (mathlib).
Sutherland explica: “Los demostradores automáticos de teoremas son técnicamente complejos, pero su desarrollo carece de recursos.” La integración de tecnologías de IA, como los grandes modelos de lenguaje (LLM), está disminuyendo las barreras de entrada, haciendo que los marcos de verificación formal sean accesibles para los matemáticos.
Mathlib y LMFDB: Dos Pilares Clave
Mathlib es una extensa biblioteca matemática impulsada por la comunidad para el demostrador de teoremas Lean, un sistema formal que verifica la exactitud de cada paso en una prueba. Actualmente, Mathlib contiene alrededor de 105 resultados matemáticos, incluyendo lemas, proposiciones y teoremas.
Por otro lado, la LMFDB es un recurso en línea colaborativo que funciona como una enciclopedia de la teoría de números moderna, conteniendo más de 109 declaraciones concretas. Tanto Sutherland como Roe son editores de la LMFDB.
El Proyecto: Un Puente entre Sistemas
El proyecto financiado por la beca busca mejorar ambos sistemas, integrando los resultados de la LMFDB en mathlib como afirmaciones que aún no han sido formalmente probadas. Además, proporcionará definiciones formales precisas de los datos numéricos almacenados en la LMFDB. Este puente beneficiará tanto a los matemáticos como a los agentes de IA, estableciendo un marco para conectar otras bases de datos matemáticas con sistemas formales de demostración de teoremas.
Superando los Obstáculos
La automatización del descubrimiento y la demostración matemática enfrenta varios desafíos:
- Conocimiento matemático formalizado limitado.
- Alto costo de formalizar resultados complejos.
- Brecha entre lo que es computacionalmente accesible y lo que es factible de formalizar.
Para abordar estos problemas, los investigadores crearán herramientas para acceder a la LMFDB desde mathlib, permitiendo que un sistema de prueba formal acceda a una vasta base de datos de conocimiento matemático no formalizado. Esto permitirá a los asistentes de prueba identificar objetivos específicos para la formalización sin necesidad de formalizar todo el corpus de la LMFDB por adelantado.
Roe destaca: “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 desear considerar al buscar un teorema o prueba es exponencialmente más grande que el conjunto de hechos que eventualmente necesitan ser formalizados para probar el teorema.”
Computación y Demostración: Un Enfoque Práctico
Los investigadores señalan que la demostración de nuevos teoremas a menudo implica pasos que dependen de cálculos no triviales. Un ejemplo es la prueba del Último Teorema de Fermat por Andrew Wiles, que utiliza el “truco 3-5” en un punto crucial.
Sutherland explica que este truco depende de que la curva modular X_0(15) tenga solo un número finito de puntos racionales, y ninguno de esos puntos corresponde a una curva elíptica semiestable. Este hecho, conocido antes del trabajo de Wiles, es fácil de verificar con herramientas computacionales modernas, pero difícil de probar con lápiz y papel o de formalizar.
Beneficios Adicionales de las Bases de Datos Matemáticas
Además de conectar los demostradores de teoremas con sistemas de álgebra computacional, el uso de bases de datos matemáticas existentes ofrece múltiples ventajas:
- Aprovechamiento de miles de años de CPU ya invertidos en la creación de la LMFDB, ahorrando costos.
- Facilidad para buscar ejemplos o contraejemplos sin conocer de antemano la amplitud de la búsqueda.
- Bases de datos como repositorios curados y organizados.
Sutherland comenta que el énfasis de los teóricos de números en el papel del conductor en las bases de datos de curvas elípticas ya ha sido crucial para un descubrimiento matemático notable realizado con herramientas de aprendizaje automático: las murmuraciones.
Próximos Pasos
Roe concluye: “Nuestros próximos pasos son construir un equipo, interactuar con las comunidades de LMFDB y mathlib, comenzar a formalizar las definiciones que sustentan las secciones de curvas elípticas, campos numéricos y formas modulares de la LMFDB, y hacer posible ejecutar búsquedas en la LMFDB desde dentro de mathlib.”
Este proyecto representa un emocionante paso adelante en la intersección de la inteligencia artificial y las matemáticas, prometiendo nuevas herramientas y enfoques para el descubrimiento matemático.
Fuente: MIT News – AI
Leave a Comment