IA, las matemáticas y Navier-Stokes

En los últimos días, después del anuncio de OpenAI de la resolución de varios de los casos del problema de Navier-Stokes (NS), hemos visto discusiones sobre la capacidad de la IA en las matemáticas y el futuro de las matemáticas.

Es necesario recalcar, como hemos ido defendiendo en este sitio , las capacidades de los modelos de deep learning (LLMs y los agentes basados en ellos) para generar nuevos datos, en este caso largas pruebas matemáticas. Unidas al desarrollo de programas de verificación como Lean 4, han permitido realizar búsquedas en el espacio de soluciones y verificar su corrección sintáctica.

Sobre la resolución del problema de NS y las implicaciones en matemáticas. De más general a más específico:

• De manera general, cuando un LLM o unos agentes resuelven un problema (de matemáticas o cualquier área), para valorar su capacidad hay que tener claro sobre qué datos se han entrenado y post-entrenado. Si usas un agente que ya ha sido entrenado con una estrategia previa y la utiliza y explota, hay que tenerlo en cuenta y saber de dónde ha partido el agente. El término inteligencia debería estar más relacionado con producir más conocimiento del que partes, no relacionar conocimiento existente. Es la discusión extrapolación vs interpolación y deducción vs inducción (abducción).

• Cuando un LLM instanciado por agentes resuelve un problema matemático, va creando soluciones o términos adicionales de la solución y verificando su consistencia lógica en Lean 4. Puede haber encontrado una solución verificada formalmente pero haber creado objetos (espacios, transformaciones…) innecesarios, incluso sin sentido matemático o físico o haber explotado algún agujero en Lean 4. Entonces, tenemos dos aspectos: La prueba puede no ser nada eficiente en términos de recursos empleados (objetos, teoremas…) ni aportar nuevo conocimiento matemático y puede ser incorrecta porque al trasladarla a Lean 4 se hayan debilitado las condiciones iniciales.

• Navier-Stokes. Como todo el mundo comenta, se han resuelto las opciones (C) y (D) del problema, que permiten introducir una fuerza, no el más interesante que es ver como evoluciona el fluido de manera natural. Ya se ha demostrado que la solución no aplicaría al caso de F=0, obviamente.

• La propia definición del problema, que busca una solución con una singularidad en la velocidad pero manteniendo finita la energía, obliga a ir a escalas próximas a 0 y saltarse la hipótesis del medio continuo y el sentido físico del problema.

• Se ha explotado la indefinición del enunciado del problema de NS, ya que normalmente cuando se permite introducir una fuerza, esta debería ser un término independiente que se introduce y se observa cómo evolucionan los campos de velocidad y presión. Aquí, primero se ha definido el campo para que tenga una singularidad en t=1, se ha introducido el término perturbativo en el campo para cancelar las divergencias del término residual (término necesario para que los campos cumplan con las ecuaciones de NS) y la fuerza es el término que ajusta lo que queda. Vamos, la fuerza es un término dependiente del campo en lugar de independiente.

• Lo más importante ahora es revisar que lo que está verificando Lean 4 es lo mismo que hay en el artículo y que no se han relajado ni cambiado ninguna de las condiciones. Lean 4 verifica corrección sintáctica no semántica. Especialmente, hay que tener cuidado, entre otras cosas, que:
  • En Lean 4 se haya definido bien el requisito de diferenciabilidad y que este requisito no se haya debilitado o localizado.
  • En Lean 4 se haya trasladado bien la singularidad como que el campo tiende a infinito y no se haya definido usando algún agujero topológico como que la solución deje de existir en ese dominio espacial para ese tiempo concreto. 
  • También, debido a que Lean 4 solo juzga la estricta tipificación lógica impuesta originalmente para el campo velocidad en el espacio de Sobolev original (“¿Sigue existiendo en H^3), al destruirse esa suavidad específica, Lean 4 puede levantar la bandera de correcto. Da por válida la prueba de que ocurrió un “finite-time blowup”, cuando en realidad lo único que ocurrió fue un cambio en la rugosidad matemática de la curva del fluido y el fluido sigue fluyendo normal en un espacio de Sobolev inferior como H^2.

El trabajo de la investigación en matemáticas ya no es hacer búsquedas exhaustivas, buscar contraejemplos o aplicar algoritmos conocidos a datos y va a centrarse más en:

• Definir las preguntas y los problemas a resolver.
• Formular nuevas teorías o relaciones entre áreas de las matemáticas.
• Verificar la corrección de las soluciones de la IA.
• Interpretar y simplificar las soluciones de la IA y desarrollar nuevos enfoques y marcos teóricos a partir de ellas.
• Entender matemáticamente como funcionan los modelos de IA, especialmente la diferencia de generación de soluciones de la IA frente a los humanos.