OpenAI resuelve un problema de Navier-Stokes y lo verifica en Lean en 17 horas

Estimaron 40 millones de dólares en costos de agentes (era una gran flota de ellos). Usando el número del artículo, se acerca más a ~880,000 horas × $150/hora = $132 millones para el caso humano. Aun así es una hazaña increíble, no exactamente "cuatro órdenes de magnitud". La comparación es obviamente inútil porque coordinar 1 millón de horas de trabajo intelectual no es fácil, por decir lo menos.

¡Tiempos muy emocionantes e inciertos!

La gente parece estar hablando de cualquier cosa menos de los resultados reales con este anuncio en particular.

Sigue siendo asombroso que cualquier tipo de programa informático generalizado pueda resolver un problema de esta magnitud, y hemos sido testigos de que sucede en tiempo real. Me daría curiosidad ver si el nuevo modelo también puede hacer pruebas más directas/pruebas inductivas.

En mi opinión, la regla de "cuarenta horas por página" no está actualizada, y es más una consecuencia de la falta de automatización de pruebas en 2005. Por lo que entiendo sobre Lean, esto ha sido una de las cosas en las que han puesto mucho esfuerzo para mejorar, haciendo la mecanización de pruebas más aceptable para los inclinados a las matemáticas, en lugar de solo para los lógicos.

¿Cómo sabes que está formalizando lo que crees que está formalizando? Si tu Lean 4 tiene un error, ¿no estarás demostrando algo distinto de lo que pensabas?

No necesariamente aplicado a la solución de OpenAI para Navier-Stokes, pero ¿qué sucede si y cuando una IA parece genuinamente resolver un problema extremadamente difícil pero los humanos no pueden verificar la solución de forma independiente porque comprender la prueba/argumento requiere una inteligencia que los verificadores biológicamente no tienen o los recursos para costear el uso de herramientas automatizadas?

Ya hemos visto evidencia en la práctica de agentes intentando evitar hacer el trabajo real en la evaluación comparativa (es decir, simplemente robar la hoja de respuestas) debido a la economía percibida de hacer trampa para obtener resultados. ¿Qué sucede si o cuando ya no tenemos la capacidad de detectar realmente si la IA hace trampa o simplemente da una respuesta incorrecta? ¿Qué pasa si hay un ataque de ingeniería social a largo plazo (como el intento de toma de control de XZ) de algo anterior a una herramienta central (o sus dependencias) para la verificación formal y no tenemos una base de computación confiable?

¿Qué sería más barato y un camino más directo, especialmente a largo plazo? Quienes intentan construir un castillo sólido como una roca necesitan defender miles de posibles brechas; el atacante solo necesita encontrar una.

sin restarle mérito al aprecio del autor por las pruebas formales recién accesibles, ¡la gente ha estado hablando de los ahorros en el esfuerzo de formalización desde antes de que se hablara de que la IA hiciera las pruebas reales!

Formalizar pruebas en Lean se ha vuelto dramáticamente más fácil desde las formalizaciones disponibles en 2005. Y la mathlib de Lean ha hecho la mayor parte del trabajo subyacente para que tengas sus axiomas y lemas necesarios incorporados. Puedes pensar en términos de abstracciones estándar que se parecen mucho a la notación exacta del libro de texto de pregrado.

Dicho esto, de ninguna manera intento menospreciar lo increíble que es lograr formalizar un algoritmo ganador de un premio del milenio en Lean. Quiero decir, solo mira el código que publicó OpenAI. Es como una enciclopedia de diferentes conceptos de dinámica de fluidos.