OpenAI publicó esta semana cientos de supuestas soluciones a problemas matemáticos difíciles, en un intento de demostrar la capacidad de sus modelos para abordar problemas avanzados. Sin embargo, la publicación no cumplió plenamente las directrices establecidas por un grupo asesor de investigadores en matemáticas, lo que reabrió la pregunta fundamental: ¿basta con que los modelos produzcan una solución susceptible de formalización informática, o debe ser comprensible y auditable por matemáticos?
El grupo Advisory Group on Mathematics and Artificial Intelligence (AGMAI) está integrado por nueve destacados investigadores y tiene su sede en el Institute for Advanced Study de la Universidad de Princeton. A finales de septiembre, el grupo publicó directrices para los laboratorios que desarrollan modelos avanzados para resolver problemas matemáticos.
Adhesión parcial a las directrices de los investigadores
AGMAI señaló que, en última instancia, corresponde a la comunidad matemática evaluar el grado de cumplimiento de sus recomendaciones. Una de sus principales recomendaciones es dejar de probar problemas matemáticos avanzados en modelos de propiedad comercial, mientras que OpenAI explicó explícitamente que utiliza problemas de investigación abiertos para evaluar sus propios modelos.
OpenAI siguió algunos principios, como publicar rápidamente los resultados y proporcionar información sobre cómo llegaron los modelos a sus conclusiones. Sin embargo, solo 10 de los 719 manuscritos incluían las cadenas de razonamiento del modelo. Además, el 42 % de las demostraciones publicadas no fueron formalizadas.
El grupo considera que las demostraciones difíciles de entender para los seres humanos deberían convertirse a un formato formal. Pero también hizo hincapié en la responsabilidad del laboratorio de garantizar que la publicación de los resultados vaya acompañada de una comprensión humana de estos, y propuso financiar a matemáticos que ayuden a hacer que esos resultados tengan un significado científico real.
Una brecha entre el lenguaje natural y el código de Lean
Los modelos suelen comenzar creando una explicación en lenguaje natural y luego intentan convertirla a Lean, un lenguaje de programación cuyo compilador puede confirmar la coherencia de la demostración en un formato ejecutable. Sin embargo, la conversión automática puede cambiar el contenido de la demostración o separar lo que dice la explicación de lo que demuestra el código.
Un artículo publicado por matemáticos de la Universidad de Cambridge y King’s College London documentó al menos dos diferencias entre una demostración en lenguaje natural y el código de Lean asociado a una solución presentada por OpenAI para un problema derivado de las ecuaciones de Navier-Stokes sobre el comportamiento de fluidos complejos. Estas diferencias no demuestran necesariamente que ninguna de las dos soluciones sea errónea, pero suscitan dudas sobre permitir que los modelos se encarguen de formalizar sus soluciones sin intervención humana.
AGMAI también pidió incluir metadatos legibles por máquinas que vinculen la demostración textual con la versión formal, algo que OpenAI no proporcionó en estas publicaciones. Los autores del artículo, conocido como “lost in translation”, concluyeron que las demostraciones textuales y las demostraciones de Lean convertidas automáticamente no deberían aceptarse inicialmente sin una revisión por pares y una auditoría similares a las que se aplican a otras demostraciones.
¿Por qué importa esta noticia?
El problema no consiste únicamente en demostrar que el código se compila correctamente, sino en demostrar que el código representa realmente la idea matemática que explica el texto. En la investigación tradicional, los científicos asumen la responsabilidad de sus resultados y los debaten mediante artículos, conferencias y seminarios, un proceso que ayuda a detectar errores y comprender métodos reutilizables.
En cambio, cuando los modelos producen una solución a un problema difícil, es posible que esa comprensión humana no exista en el momento de la publicación. Por ello, los resultados actuales de OpenAI parecen más el comienzo del proceso de verificación científica que el final del problema; la revisión humana y la conexión entre las salidas textuales y formales siguen siendo dos condiciones pendientes antes de aceptar estas demostraciones dentro de la comunidad matemática.