OpenAI tradujo mal las matemáticas a código en su prueba de Navier-Stokes
OpenAI mistranslated mathematics into code for its Navier-Stokes proof
Un equipo de matemáticos afirma que OpenAI cometió un error sutil al publicar sus pruebas del problema de Navier-Stokes: produjo una versión para humanos y otra para computadoras, pero no coinciden. El fallo no invalida la solución, aunque pone en duda la fiabilidad de los resultados generados por modelos de lenguaje, que exigen una revisión humana exhaustiva.
Lo que hay que hacer con todas estas pruebas generadas por modelos de lenguaje es que tendrán que ser leídas por humanos, y esto crea una enorme carga adicional para los matemáticos.
- krackers
Duplicado de https://news.ycombinator.com/item?id=49994145
- jey
Este titular está completamente equivocado. La analogía correcta con la programación es más bien que el artículo en lenguaje natural era el "documento de diseño" antes de programarlo, y luego, al programarlo como demostraciones en Lean4, se descubrió que ciertos detalles específicos estaban ligeramente mal[1] y se corrigieron mientras se escribía la implementación en código como demostraciones verificables por máquina. Lo cual estoy seguro de que es una situación extremadamente identificable para la mayoría de nosotros aquí. Pero el artículo o "documento de diseño" no se corrigió después.
También creo que este enfoque de "primero el artículo, luego el código" ya está obsoleto. La forma moderna, en flujos de trabajo asistidos por IA, es iterar primero sobre "esbozo de derivación <-> demostración verificable por máquina" construyendo incrementalmente tu resultado. Por supuesto, puedes dejar marcadores de posición `sorry` en el camino e irlos rellenando, así que no es que estés restringido a ir totalmente de abajo hacia arriba. Finalmente, una vez que tienes una demostración sin `sorry` de tus enunciados de nivel superior (teoremas) de interés, puedes entonces trabajar en redactar la exposición en LaTeX basándote en el código Lean.
1. Véase https://arxiv.org/abs/2610.08144 para más detalles, pero un ejemplo que señalan es que una cota clave requería 5 órdenes adicionales de derivadas (y así se enunciaba en Lean), pero el artículo afirmaba que la cota se cumplía con solo cuatro derivadas más.