OpenAI a annoncé que sa prochaine génération de modèle d'IA avait résolu 10 problèmes mondiaux, y compris la conjecture de rigidité de Connes.
Le lendemain, un article humain a répondu : Le contre-exemple proposé par l'IA n'est pas valable.
L'auteur est J. L. Nielsen du Centre de Topologie Physique de l'Université du Kansas. Il a suivi ligne par ligne les 37 000 lignes de code Lean 4 publiées par OpenAI, a retracé chaque objet vers son prototype mathématique, et a finalement identifié deux chemins d'échec indépendants.
Le processus de preuve spécifique n'est pas facile à comprendre pour le commun des mortels, laissons l'IA et les mathématiciens se battre.
Mais cet événement montre que la vérification humaine des résultats de recherche de l'IA reste cruciale.
Qu'est-ce que la conjecture de rigidité de Connes
La conjecture de rigidité de Connes dit ceci.
Mathématiquement, on peut associer une structure algébrique à un groupe. Parfois, deux groupes qui semblent différents donnent des structures complètement identiques.
Connes a émis la conjecture vers 1980 : À condition que ce groupe satisfasse deux conditions supplémentaires, cette situation ne se produira pas. Structure identique signifie groupe identique.
Ces deux conditions supplémentaires sont l'une appelée ICC, l'autre la propriété (T) de Kazhdan.
En d'autres termes, pour réfuter cette conjecture, il faut trouver des groupes satisfaisant les deux conditions mais construits différemment.
La nouvelle méthode du modèle d'OpenAI consiste à construire deux groupes non isomorphes, leur faire générer la même algèbre, et fournir une preuve que les deux groupes satisfont ICC et la propriété (T).
L'argumentation complète est écrite en 37 000 lignes de code Lean 4, vérifiées ligne par ligne par le noyau Lean, accompagnée d'une documentation expliquant comment ces deux groupes sont construits.
Nielsen souligne : L'un des groupes construits par l'IA ne satisfait en fait pas les conditions supplémentaires. Il n'est ni ICC, ni ne possède la propriété (T).
Il y a trois possibilités :
Dans le code, la propriété (T) ne correspond pas fidèlement à la définition originale de Kazhdan ; ou la preuve n'est valable que pour une partie, mais est considérée comme valable pour le groupe entier ; ou bien le groupe dans le code n'est pas du tout celui décrit dans la documentation.
37 000 lignes, vérifiées ligne par ligne
Pour vérifier cette conclusion, Nielsen a fait un travail encore plus fastidieux.
Le code publié est une version intégrée en un seul fichier, les noms des premiers modules sources ont tous disparu.
Il a donc créé une table de correspondance, listant le nom et le numéro de ligne de chaque objet mathématique dans le nouveau code :
Le groupe de cocycles nuls en haut à la ligne 13700, le groupe tordu à la ligne 14069, la preuve de l'isomorphisme des deux algèbres à la ligne 36712, le théorème principal à la ligne 36954.
Il a aussi retracé toute la chaîne de raisonnement dans le code prouvant ICC. Cette chaîne commence à la ligne 31430, passe de couche en couche, et aboutit à une conclusion synthétisée à la ligne 31610.
Le problème soulevé par Nielsen est que ces lemmes traitent des objets après une transformation duale, pas du groupe original avec élément central, et ne couvrent donc pas directement la partie cruciale des éléments.
Quant à savoir s'ils sont valables pour chaque élément du groupe spécifique qui entre finalement dans le théorème, cela dépend de la manière dont l'interface entre les deux blocs de construction est connectée.
Cela montre que le problème est "que faut-il prouver", et non "si la preuve est correcte". Lean ne vérifie que le second.
Pour l'autre groupe tordu, Nielsen adopte une position prudente. Il déclare ne pas avoir vérifié indépendamment à partir du code s'il satisfait vraiment ICC, et admet que les lemmes dans le code pourraient effectivement prouver qu'il la satisfait, mais cela ne change pas la conclusion, une condition n'étant déjà pas satisfaite.
Il a également écrit ses deux réfutations sous forme de code Lean, compilé sous Lean 4.32.2.
La machine vérifie la forme, pas le sens
La dernière section de l'article place cet événement dans un contexte plus large.
Ce que le noyau Lean peut garantir, c'est uniquement qu'une preuve est formellement rigoureuse, mais il ne se charge pas de savoir si elle prouve réellement la conclusion originale.
On peut citer directement Terence Tao : la vérification de la preuve concerne l'énoncé formel lui-même, et non la correspondance de cet énoncé avec l'intention, donc la vérification humaine ne peut être directement remplacée.
De tels incidents ont déjà été documentés.
Un audit de cinq bases de référence Lean couramment utilisées a relevé 4833 découvertes, y compris des contre-exemples, des théorèmes vides et des axiomes non fiables, tous ayant passé la vérification machine. C'est finalement une construction humaine de contre-exemples qui a révélé que la phrase prouvée était elle-même fausse.
Dans les travaux de formalisation de la théorie de l'apprentissage statistique, le scénario le plus dangereux est décrit comme "pas une preuve ratée, mais une preuve réussie d'un énoncé erroné".
La recherche sur les réseaux de tenseurs a également documenté un phénomène similaire : le système produisait une preuve formellement parfaitement correcte, sauf que la proposition prouvée était plus faible que prévu.
Nielsen écrit que cette formalisation d'OpenAI a peut-être correctement établi chacune des conclusions qu'elle prétend prouver. Mais ce qu'elle n'établit pas, et que le noyau Lean ne vérifie pas, c'est si ces conclusions ont un rapport avec la formulation originale de la conjecture.
Un humain lisant la conjecture voit les prémisses, un assistant de preuve recevant une conclusion qui ne satisfait pas les prémisses vérifiera néanmoins toute affirmation la concernant.
La conjecture de rigidité de Connes reste ouverte.
Adresse de l'article :
https://philarchive.org/archive/NIEWTCv17
Liens de référence :
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
Cet article provient du compte WeChat "Quantum Bits", auteur : Meng Chen
