OpenAI afirmó que su próximo modelo de IA resolvió 10 problemas de clase mundial, incluida la refutación de la conjetura de rigidez de Connes.
Al día siguiente, apareció un artículo humano que respondía: El contraejemplo propuesto por la IA no es válido.
El autor es J. L. Nielsen del Centro de Física Topológica de la Universidad de Kansas. Revisó de principio a fin las 37.000 líneas de código en Lean 4 publicadas por OpenAI, comparando cada objeto con su prototipo matemático, y finalmente presentó dos trayectorias de fallo independientes.
El proceso de demostración específico es difícil de entender para la gente común, dejemos que la IA y los matemáticos libren su batalla celestial.
Pero este incidente demuestra que la revisión humana de los resultados de investigación científica de la IA sigue siendo crucial.
¿Qué es la conjetura de rigidez de Connes?
La conjetura de rigidez de Connes trata sobre lo siguiente.
Matemáticamente, a un grupo se le puede asignar una estructura algebraica. A veces, dos grupos que parecen diferentes pueden generar estructuras completamente idénticas.
Connes propuso alrededor de 1980 la siguiente conjetura: Siempre que este grupo cumpla dos condiciones adicionales, esta situación no ocurrirá; si las estructuras son iguales, los grupos deben ser iguales.
Estas dos condiciones adicionales se denominan ICC y propiedad (T) de Kazhdan.
En otras palabras, para refutar esta conjetura, es necesario presentar grupos que cumplan ambas condiciones pero tengan estructuras diferentes.
El enfoque del nuevo modelo de OpenAI fue construir dos grupos no isomórficos que generen el mismo álgebra, y proporcionar pruebas de que ambos grupos cumplen con ICC y la propiedad (T).
Toda la argumentación se escribió en 37.000 líneas de código Lean 4, verificadas línea por línea por el núcleo de Lean, junto con una documentación explicativa sobre cómo se construyeron estos dos grupos.
Nielsen señaló: Uno de los grupos construidos por la IA en realidad no cumple las condiciones adicionales; no es ICC y tampoco tiene la propiedad (T).
Existen tres posibilidades para esto:
O la propiedad (T) en el código no corresponde fielmente a la definición original de Kazhdan; o la prueba solo es válida para una parte, pero se aplicó a todo el grupo; o el grupo en el código simplemente no es el descrito en la documentación.
37.000 líneas, comparadas una por una
Para verificar esta conclusión, Nielsen hizo algo aún más laborioso.
El código publicado públicamente era una versión consolidada en un solo archivo, donde todos los nombres de los módulos fuente originales habían desaparecido.
Por lo tanto, creó una tabla de correspondencias, marcando el nombre y el número de línea de cada objeto matemático en el nuevo código:
El grupo de cocadenas cero positivas está en la línea 13700, el grupo torcido en la línea 14069, la prueba del isomorfismo de las dos álgebras en la línea 36712, y el teorema principal en la línea 36954.
También rastreó la cadena de razonamiento completa en el código que probaba ICC. Esta cadena comenzaba en la línea 31430, pasaba capa por capa y finalmente sintetizaba la conclusión en la línea 31610.
El problema señalado por Nielsen es que estos lemas tratan objetos después de una transformación dual, no el grupo original con elementos centrales, por lo que no cubren directamente la parte crucial de elementos.
En cuanto a si se cumplen para cada elemento del grupo específico que finalmente entra en el teorema, depende de cómo se conectan las interfaces entre las dos construcciones.
Esto indica que el problema está en "qué se intenta probar", no en "si la prueba es correcta". Lean solo se encarga de verificar lo último.
Con respecto al otro grupo torcido, la postura de Nielsen es conservadora. Dijo que no verificó de forma independiente a partir del código si realmente cumple con ICC, y admitió que los lemas en el código podrían realmente probar que lo cumple, pero eso no cambia la conclusión, ya que una de las condiciones no se satisface.
También escribió sus dos refutaciones en código Lean, compilables en Lean 4.32.2.
La máquina verifica la forma, no el significado
La última sección del artículo sitúa este incidente en un contexto más amplio.
Lo que el núcleo de Lean puede garantizar es solo que una prueba sea formalmente rigurosa, pero no se responsabiliza de si realmente demuestra la conclusión original.
Aquí podemos citar directamente a Terence Tao: lo que se verifica es la afirmación formal en sí misma, no si esta afirmación coincide con la intención, por lo que la revisión humana no puede ser reemplazada directamente.
Ya existen registros de incidentes similares en el pasado.
Una auditoría de cinco puntos de referencia comunes en Lean reveló 4.833 hallazgos, incluidos contraejemplos, teoremas vacíos y axiomas no confiables, todos pasados por la verificación de la máquina. Finalmente, fueron los humanos quienes construyeron contraejemplos para descubrir que la afirmación probada en sí era incorrecta.
En trabajos de formalización de la teoría del aprendizaje estadístico, la situación más peligrosa se describe como "no una prueba fallida, sino una prueba exitosa de una afirmación incorrecta".
Investigaciones en redes tensoriales también han registrado fenómenos similares: el sistema proporcionaba una prueba formalmente completamente correcta, solo que el teorema probado era más débil de lo esperado.
Nielsen escribió que esa formalización de OpenAI podría haber establecido correctamente cada conclusión que afirmaba. Pero lo que no estableció, y lo que el núcleo de Lean tampoco puede verificar, es si esas conclusiones tienen alguna relación con el enunciado original de la conjetura.
Un humano que lea la conjetura verá las premisas; un asistente de pruebas que reciba una conclusión que no satisface las premisas, verificará cualquier afirmación sobre ella de todos modos.
La conjetura de rigidez de Connes sigue abierta.
Dirección del artículo:
https://philarchive.org/archive/NIEWTCv17
Enlaces de referencia:
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
Este artículo proviene del WeChat público "Qubit", autor: Meng Chen
