El artículo, titulado 'Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs,' examina el uso de la IA para traducir argumentos matemáticos de lenguaje natural a lenguajes de prueba formales como Lean. Señala que una vez traducido, la prueba formal puede verificarse mecánicamente, pero cuestiona si esa verificación brinda confianza en el argumento original de lenguaje natural. Los autores se centran en la prueba anunciada de OpenAI del estallido de soluciones a las ecuaciones de Navier-Stokes como un ejemplo destacado de autoformalización mediante IA, donde muestran que la prueba formalizada en Lean no corresponde a la prueba de lenguaje natural del estallido.
Los autores argumentan que la dificultad principal reside en resolver las ambigüedades inherentes a los textos matemáticos de lenguaje natural. Demuestran que este problema es arbitrariamente alto en la jerarquía del Índice de Complejidad de Solvabilidad (SCI), lo que significa que es más difícil que cualquier problema computacional, incluido el problema de la Parada (que tiene un SCI de 1). Por lo tanto, crear una traducción semánticamente fiel del lenguaje natural a un lenguaje formal como Lean es, en principio, más difícil que resolver cualquier problema algorítmico, lo que implica que ningún método general puede garantizar una traducción fiel para todos los textos matemáticos.
Para demostrar esto, el artículo proporciona varios ejemplos de mistranslations de la IA de enunciados y pruebas de lenguaje natural a Lean, lo que resulta en discrepancias entre las pruebas de lenguaje natural y sus verificaciones en Lean. En el caso de la prueba de Navier-Stokes de OpenAI, la prueba formalizada en Lean no corresponde a la prueba de lenguaje natural del estallido. Esto significa que, aunque la prueba de Lean pueda ser correcta por sí misma, no representa con precisión el argumento original de lenguaje natural que la IA debería haber formalizado, lo que socava la confianza que la verificación en Lean ofrece en la corrección de la prueba original de NL.