El avance matemático de OpenAI ha empezado a generar dudas. Los científicos compararon la demostración publicada sobre las ecuaciones de Navier-Stokes con su versión algorítmica en Lean y encontraron discrepancias: en varios puntos clave, la variante automática, verificable por ordenador, contiene afirmaciones más débiles. No es todavía una refutación, pero el terreno para las dudas ya es bastante fértil.
Fuente de la imagen: Thomas T /unsplash.com
Según los matemáticos, la discrepancia no significa en absoluto que las demostraciones sean falsas ni que OpenAI haya resuelto mal el problema, pero pone en duda que siempre se pueda confiar en los resultados matemáticos generados por modelos de inteligencia artificial.
«Lo que hay que hacer con todas estas grandes demostraciones creadas a partir de un modelo de lenguaje es que las lea gente, y eso supone una enorme carga adicional para los matemáticos», ha señalado el jefe del equipo, Anders Hansen.
El proceso de búsqueda de discrepancias llevó al equipo unas dos semanas. Los matemáticos se apoyaron en las indicaciones de ChatGPT. Cabe recordar que a OpenAI le llevó 88 horas resolver el problema.
Los matemáticos señalaron una discrepancia en una parte de la demostración denominada lema 8.6. En la demostración en lenguaje natural, la ecuación de esa parte exige que un determinado valor sea menor que m + 4, donde m es un número entero, mientras que en la versión en Lean es menor que m + 5, lo que matemáticamente es más débil, ya que admite más soluciones posibles y no equivale a lo primero.
Imaginemos que nos piden resolver la ecuación x + 3 = 6, cuya respuesta es x = 3. Se puede escribir una demostración de que x debe ser menor que 4, y también de que x debe ser menor que 5. Ambas afirmaciones matemáticas son absolutamente ciertas, pero la segunda admite más respuestas posibles para x, lo que la hace matemáticamente más débil.
Según Hansen, el error de traducción pudo deberse a que la IA tiende a que el código informático sea plenamente coherente y no arroje errores. Si durante la formalización automática la IA detecta una parte de la demostración que no compila, intenta buscar un camino alternativo, aunque eso suponga apartarse de la demostración escrita en lenguaje natural.
Kevin Buzzard, del Imperial College de Londres, ha señalado que se puede formalizar de forma fiable en Lean el enunciado mismo del teorema y comprobar después si la demostración compila. Pero eso no garantiza que la demostración en texto del PDF transmita correctamente la lógica. Es decir, el código en Lean puede ser coherente en sí mismo, pero no corresponderse con lo que dice el artículo. «Estoy convencido de que el problema de Navier-Stokes se resolvió correctamente», dice Buzzard. «Estoy mucho menos convencido de que la demostración descrita en el texto sea correcta».
OpenAI ha declarado al medio New Scientist que conoce la discrepancia entre la demostración en lenguaje natural y la escrita en código, y que eso no significa que ninguna de las dos sea inválida.