La verificación en Lean no garantiza que una prueba matemática generada por IA sea correcta
Navier–Stokes Lost in Translation
La autoformalización con IA traduce textos matemáticos a Lean para verificarlos mecánicamente, pero un nuevo artículo demuestra que una traducción semánticamente fiel es imposible en general: resolver ambigüedades del lenguaje natural es más difícil que el problema de la parada (SCI = ∞). El trabajo expone varios casos reales de mistraducción, incluida la anunciada prueba de blow-up de las ecuaciones de Navier-Stokes de OpenAI, y muestra que la prueba formal en Lean no corresponde a la demostración original en lenguaje natural.
El problema de resolver ambigüedades en textos matemáticos en lenguaje natural, necesario para una traducción semánticamente fiel, es arbitrariamente alto en la jerarquía del Solvability Complexity Index (SCI = ∞).
- ComplexSystems
Aparte de las discusiones habituales sobre la IA, parece que la afirmación bomba es esta:
"En particular, mostramos que la prueba formalizada en Lean no se corresponde con la prueba en lenguaje natural de la explosión de soluciones de las ecuaciones de Navier-Stokes."
Así que estos autores parecen afirmar que OpenAI no ha demostrado realmente Navier-Stokes en absoluto. Si entiendo bien su idea, sostienen que el LLM no ha formalizado correctamente la idea original en "lenguaje natural" de Navier-Stokes. Si es cierto, significaría que su supuesta prueba en Lean no es en realidad una prueba de Navier-Stokes en absoluto, sino algo que es una traducción incorrecta de la idea original en lenguaje natural. Si es correcto, es una afirmación realmente audaz y me gustaría ver si otros investigadores están de acuerdo.
- buzzy_hacker
Si entiendo bien, ¿esto cuestiona la equivalencia entre la prueba en lenguaje natural y la prueba en Lean, pero no la corrección de la prueba en Lean?
- stared
Para refrescar en pocas palabras qué es Navier-Stokes: https://p.migdal.pl/equations-explained-colorfully/#navier-s...
- vanyle
Este artículo es una gran cantidad de nada. Primero, el lenguaje natural no es tan preciso como Lean, así que tienes múltiples formas de traducir un argumento en lenguaje natural a Lean. Como se muestra en la Fig. 1, el LLM hizo un trabajo decente al traducir el argumento sobre raíces de forma sucinta.
Además, el artículo afirma que los argumentos en lenguaje natural de Navier-Stokes son más fuertes que los de Lean. Mi entendimiento es que el LLM traductor se volvió perezoso y escribió la cantidad mínima de código que satisfacía el teorema sin las afirmaciones adicionales más fuertes.
Es común en los artículos de matemáticas decir "Y por cierto, esto en realidad demuestra [afirmación más fuerte]", pero esto es algo que una IA con el objetivo preciso de realizar una traducción nunca haría, ya que su objetivo es traducir la prueba, no hacer matemáticas de calidad.
- infogulch
El artículo muestra que la prueba en Lean y la prueba en prosa (pdf) no coinciden exactamente. Pero si el teorema de Lean que Lean aceptó es equivalente al enunciado original del problema publicado por el Clay Institute, esta discrepancia no tiene consecuencias para la validez de la prueba en sí. Ese no es un "si" trivial: enunciar el problema con precisión es a menudo tan difícil como la prueba. Los esfuerzos de validación deberían concentrarse en si el teorema de Lean es equivalente al publicado por el Clay Institute.
Dicho esto, una brecha entre la prueba en Lean y el pdf es molesta para la interpretabilidad, y la interpretación es un objetivo válido, pero eso no influye en la validez de la prueba.
- sigbottle
¿Alguna vez nos encontraremos con una crisis de la teoría del significado?
_Suponiendo_ dos modos de fallo:
- El kernel de Lean siempre podría tener un bug.
- El enunciado formalizado podría no corresponder a lo que los _matemáticos_ "realmente querían".
Parece natural hacer el argumento de: "Bueno, incluso si planteas que la prueba puede tener errores, seguramente es más fácil verificar el enunciado del problema de algo que la solución".
(Una "propiedad agradable" es que el agente ni siquiera necesita "acertar los subargumentos" según el _segundo_ criterio; quizás en la prueba natural inventa un objeto sutilmente diferente del formal, pero todo cuadra. Si garantizas que el enunciado _original_ corresponde, entonces la única posibilidad es el kernel de Lean. Así que no recursa infinitamente, en este caso).
Pero las "definiciones" siempre son algo realmente extraño para lo que no creo que tengamos buenas teorías. ¿Cómo cuantificas cuánto poder descriptivo necesitas para expresar una pregunta? A menudo en matemáticas, la parte difícil es acertar con la definición, pero ¿y si la definición misma se vuelve tan compleja e inverificable que nadie puede corresponderla con nada? Bueno, parece que muchos problemas matemáticos interesantes y de larga data tienen enunciados "relativamente" simples, de tal manera que podrías formalizarlos en Lean fácilmente, pero no estoy seguro de si realmente hay una bala de plata con Lean o si va a ser tortugas hasta el fondo.
Probablemente no importe siempre que la IA siga disparándose […]
- dooglius
Dada la descripción de alto nivel de los ejemplos, creo que es menos una "mala traducción" y más que el LLM ajustó la prueba mientras la formalizaba. Pasar de m+4 a m+5 es algo bastante diferente del tipo de ambigüedades que generalmente surgen al analizar enunciados matemáticos en lenguaje natural.
- Sniffnoy
Mmm, mirando esto, no veo dónde indican qué es lo que OpenAI realmente demostró en lugar de la explosión de Navier-Stokes con forzamiento. Veo dónde lo hacen para otros enunciados particulares usados en el camino, pero no para el resultado principal.