Ayer, OpenAI publicó 722 manuscritos de matemáticas de IA de una sola vez, y justo ahora retiró 3 de ellos.
La razón es simple: se escribió incorrectamente un signo de más-menos.
Justo ahora, OpenAI publicó su primer registro de actualización en el repositorio openai/math. El registro muestra que OpenAI retiró 3 manuscritos, revisó 14 y actualizó las citas de otros 13. El número total de manuscritos en el repositorio cayó de 722 a 719.
Un signo de más-menos derriba tres artículos
Los tres artículos retirados están todos relacionados con la conjetura de Hodge, uno de los Problemas del Milenio:
Algebraicidad de las clases de Weil en variedades abelianas de dimensión ocho escindidas
Algebraicidad de las correspondencias de Kuga–Satake para superficies K3
La conjetura de Hodge racional para productos de superficies K3
El problema radica en el primer artículo. En la nota de retirada, OpenAI escribió que en un argumento clave, el artículo registró el signo de cierta operación geométrica como +1, mientras que, según la propia convención del artículo, debería ser -1.
https://github.com/openai/math/blob/main/history.md
Un más frente a un menos marca una gran diferencia. Un recuento que debería haberse cancelado y finalmente haber sido cero se convirtió en un número distinto de cero. Un teorema clásico en el que se basa el artículo tiene como condición previa precisamente que este recuento debe ser cero. Al fallar la condición previa, toda la construcción posterior pierde su sustento.
Los otros dos artículos tomaron prestada esta construcción, por lo que también fueron retirados.
Sin embargo, en las tres notas de retirada, OpenAI enfatizó la misma frase: lo que se retira es la prueba, lo que no significa que estas proposiciones matemáticas en sí mismas sean erróneas. Los manuscritos originales tampoco fueron eliminados y aún pueden consultarse a través de enlaces archivados.
Estos tres artículos pertenecen todos a la familia de resultados n.º 032 del repositorio, es decir, los resultados relacionados con la conjetura de Hodge que antes habían despertado más interés.
Tras la retirada, el nombre de esta familia también cambió: de "Resultados de Hodge y Kuga–Satake para todas las superficies K3 proyectivas" a "la conjetura de Hodge racional para variedades abelianas CM".
En otras palabras, la parte de las conclusiones relativa a las superficies K3 ha sido eliminada de la lista. La conclusión central de esta familia, a saber, demostrar la conjetura de Hodge racional para todas las variedades abelianas CM complejas, todavía se mantiene, y la nueva versión de ese artículo solo actualizó las citas.
Cabe mencionar que el artículo con el error está fechado el 18 de septiembre, lo que lo convierte en uno de los primeros manuscritos del repositorio. Desde su fecha hasta su publicación pública pasaron casi tres semanas, y fue retirado dentro de uno o dos días después de su publicación. En cuanto a quién descubrió el error, OpenAI no lo dijo.
Otros 14 artículos fueron revisados
Además de las retiradas, OpenAI también revisó 14 manuscritos, incluyendo la corrección de pruebas, la rectificación de declaraciones de conclusiones y la aclaración de precondiciones y dependencias.
Estos 14 involucran alturas de Lipschitz y el modelo de Ashkin–Teller en física estadística (4 artículos), el programa de modelos minimales de Kähler y abundancia en geometría compleja (6 artículos), geometría simpléctica (2 artículos), computación general para fluidos de Navier-Stokes (1 artículo), y un artículo sobre la fórmula BSD del cual se eliminaron citas obsoletas.
Una revisión es bastante representativa. La familia de resultados n.º 342 afirmaba probar la conjetura de "compatibilidad de pushforward manso" propuesta por Simon Donaldson. La conclusión principal no cambió, y hay una formalización en Lean. Pero se descubrió que una conclusión incidental más fuerte en el artículo estaba exagerada: la versión revisada la reduce a un caso específico y también añade un ejemplo que muestra que no se cumple en general.
Tasa de formalización: 42%
La actualización también añadió 6 formalizaciones en Lean y 5 resultados auxiliares suplementarios. Según la contabilidad de OpenAI, los resultados principales de 300 manuscritos han sido ahora formalizados, lo que representa aproximadamente el 42% de todos los 719.
Entre las formalizaciones recién añadidas, varias tienen un peso considerable, como la familia de logros n.º 103 en informática teórica que afirma probar que la computación en espacio logarítmico puede ser completamente derandomizada (L = RL = BPL).
Cabe señalar que el "aproximadamente sesenta por ciento" que reportamos anteriormente se contaba por familia de logros, es decir, siempre que un artículo de una familia venga con una formalización, se cuenta; el 42% anunciado por OpenAI se cuenta por resultados principales individuales, lo que refleja mejor la proporción real que ha sido verificada línea por línea por una computadora.
Donde ocurren errores, no hay supervisión de Lean
Al comparar con el directorio del repositorio se revela un patrón: el contenido que fue retirado y sustancialmente revisado esta vez casi todo cae en las partes sin formalización en Lean.
Esto también confirma la advertencia anterior de la comunidad matemática: los resultados que no han pasado por formalización y revisión por pares actualmente solo pueden considerarse como "afirmaciones".
Afortunadamente, esta fe de erratas se manejó de manera bastante adecuada: los errores se declararon claramente, se explicó la cadena de dependencias y se mantuvo disponible la versión antigua para referencia, en línea con el principio de "modificación con rastro" recomendado por el Grupo Asesor de Matemáticas e Inteligencia Artificial del Instituto de Estudios Avanzados.
Sin embargo, solo dos días después de que más de 700 manuscritos se hicieran públicos, llegó la primera fe de erratas. Lo más probable es que no sea la última.
Este artículo proviene de la cuenta pública de WeChat "Machine Heart" (ID: almosthuman2014), editor: Panda
