Ein Mathematiker hat die von OpenAI gelöste Vermutung innerhalb von 24 Stunden zurückgewiesen! „Die KI hat jede einzelne Aussage korrekt bewiesen, aber das hat keinerlei Bezug mehr zur ursprünglichen Vermutung“

OpenAI behauptet, dass sein nächstes KI-Modell 10 weltweite schwierige Probleme gelöst hat, darunter die Widerlegung der Connes-Rigiditätsvermutung.

Am nächsten Tag erschien eine menschliche Arbeit als Antwort: Das von der KI vorgeschlagene Gegenbeispiel ist ungültig.

Der Autor ist J. L. Nielsen vom Zentrum für Topologische Physik der Universität Kansas. Er verfolgte die 37.000 Zeilen des von OpenAI veröffentlichten Lean-4-Codes von Anfang bis Ende, ordnete jedes Objekt seinem mathematischen Urbild zu und ergab schließlich zwei voneinander unabhängige Fehlpfade.

Der konkrete Beweisprozess ist für normale Menschen kaum verständlich – lassen wir die KI und die Mathematiker ihr „Götterkampf“ austragen.

Aber dieses Ereignis zeigt, dass die menschliche Überprüfung der wissenschaftlichen Forschungsergebnisse von KI nach wie vor entscheidend ist.

Was ist die Connes-Rigiditätsvermutung

Die Connes-Rigiditätsvermutung beschreibt folgendes Sachverhalt.

Mathematisch kann man einer Gruppe eine algebraische Struktur zuordnen. Manchmal ergeben zwei Gruppen, die auf den ersten Blick unterschiedlich aussehen, genau dieselbe Struktur.

Connes stellte um 1980 die Vermutung auf: Solange die Gruppe zwei zusätzliche Bedingungen erfüllt, kann dieser Fall nicht eintreten: Bei gleicher Struktur müssen die Gruppen identisch sein.

Diese zwei zusätzlichen Bedingungen heißen ICC und die Kazhdan-Eigenschaft (T).

Mit anderen Worten, um diese Vermutung zu widerlegen, muss man Gruppen angeben, die beide Bedingungen erfüllen, aber unterschiedliche Konstruktionen aufweisen.

Das Vorgehen des neuen Modells von OpenAI besteht darin, zwei nicht isomorphe Gruppen zu konstruieren, die dieselbe Algebra erzeugen, und zu beweisen, dass beide Gruppen die Bedingungen ICC und Eigenschaft (T) erfüllen.

Die gesamte Argumentation wurde in 37.000 Zeilen Lean-4-Code verfasst, der Zeile für Zeile vom Lean-Kern verifiziert wurde. Zusätzlich liegt ein Erklärungsdokument vor, das erläutert, wie diese beiden Gruppen aufgebaut sind.

Nielsen wies darauf hin: Eine der von der KI konstruierten Gruppen erfüllt die zusätzlichen Bedingungen tatsächlich nicht: Sie ist weder ICC noch weist sie die Eigenschaft (T) auf.

Dafür gibt es drei mögliche Gründe:

Entweder entspricht die Eigenschaft (T) im Code nicht treu der ursprünglichen Definition von Kazhdan; oder der Beweis gilt nur für einen Teil der Gruppe, wird aber auf die gesamte Gruppe ausgeweitet; oder die Gruppe im Code entspricht überhaupt nicht der Beschreibung im Erklärungsdokument.

37.000 Zeilen, Zeile für Zeile abgeglichen

Um diese Schlussfolgerung zu überprüfen, unternahm Nielsen noch eine aufwändigere Aufgabe.

Der öffentlich veröffentlichte Code ist zu einer einzigen Datei zusammengefasst, alle Namen aus dem ursprünglichen modularen Quellcode sind verschwunden.

Er erstellte daher eine Vergleichstabelle, in der er den Namen und die Zeilennummer jedes mathematischen Objekts im neuen Code einzeln aufführte:

Die Gruppe der Null-Kozykel oberhalb befindet sich in Zeile 13700, die verdrehte Gruppe in Zeile 14069, der Beweis der Isomorphie der beiden Algebren in Zeile 36712 und der Hauptsatz in Zeile 36954.

Er verfolgte auch die gesamte Beweiskette der ICC-Eigenschaft im Code. Diese Kette beginnt in Zeile 31430, wird schichtweise nach oben übertragen und ergibt schließlich in Zeile 31610 die Schlussfolgerung.

Das von Nielsen aufgezeigte Problem besteht darin, dass diese Lemmata Objekte behandeln, die nach einer dualen Transformation umgewandelt wurden, nicht die ursprüngliche Gruppe mit Zentralelementen, sodass sie den entscheidenden Teil der Elemente nicht direkt abdecken.

Ob diese Aussagen für jedes Element der konkreten Gruppe gelten, die letztendlich in den Satz eingeht, hängt davon ab, wie die Schnittstelle zwischen den beiden Konstruktionsteilen verbunden ist.

Das bedeutet, dass bereits das „Was bewiesen werden soll“ fehlerhaft ist, nicht das „Ob der Beweis korrekt ist“ – Letzteres wird nur von Lean überprüft.

Bei der anderen verdrehten Gruppe verhält sich Nielsen konservativ. Er gibt an, dass er nicht unabhängig aus dem Code überprüft hat, ob sie die ICC-Eigenschaft erfüllt, und räumt ein, dass die Lemmata im Code diese Eigenschaft möglicherweise tatsächlich beweisen – aber das ändert nichts an der Schlussfolgerung, da bereits eine Bedingung nicht erfüllt ist.

Er schrieb seine beiden Widerlegungen ebenfalls in Lean-Code, der unter Lean 4.32.2 kompiliert wurde.

Maschinen prüfen die Form, nicht die Bedeutung

Der letzte Abschnitt der Arbeit stellt dieses Ereignis in einen größeren Kontext.

Was der Lean-Kern garantieren kann, ist nur, dass ein Beweis formal lückenlos ist – er übernimmt keine Verantwortung dafür, ob er die ursprüngliche Schlussfolgerung tatsächlich beweisen kann.

Hier kann man direkt Tao Ter-Tses Aussage zitieren: Überprüft wird die formale Aussage des Beweises selbst, nicht ob diese Aussage mit der beabsichtigten Bedeutung übereinstimmt. Daher kann menschliche Überprüfung nicht direkt ersetzt werden.

In der Vergangenheit gab es bereits Aufzeichnungen über solche Vorfälle.

Eine Prüfung von fünf gängigen Lean-Benchmarks ergab 4833 Feststellungen, darunter Gegenbeispiele, inhaltsleere Sätze und unzuverlässige Axiome, die alle die Maschinenprüfung bestanden. Erst als Menschen Gegenbeispiele konstruierten, stellte sich heraus, dass die bewiesene Aussage selbst falsch war.

Bei der Formalisierung der statistischen Lerntheorie wird der gefährlichste Fall als „kein fehlgeschlagener Beweis, sondern ein erfolgreicher Beweis einer falschen Aussage“ beschrieben.

Auch bei Forschungen zu Tensornetzwerken wurden ähnliche Phänomene dokumentiert: Der vom System gelieferte Beweis ist formal völlig korrekt, nur der Satz, den er beweist, ist schwächer als erwartet.

Nielsen schreibt, dass die Formalisierung von OpenAI möglicherweise jede der von ihr behaupteten Schlussfolgerungen korrekt aufgebaut hat. Was sie aber nicht aufgebaut hat und auch vom Lean-Kern nicht überprüft werden kann, ist, ob diese Schlussfolgerungen mit der ursprünglichen Formulierung der Vermutung übereinstimmen.

Wenn Menschen die Vermutung lesen, erkennen sie ihre Voraussetzungen. Ein Beweisassistent erhält eine Schlussfolgerung, die die Voraussetzungen nicht erfüllt, und wird trotzdem jede Aussage darüber verifizieren.

Die Connes-Rigiditätsvermutung bleibt weiterhin offen.

Adresse der Arbeit:

https://philarchive.org/archive/NIEWTCv17

Referenzlinks:

[1]https://openai.com/index/ten-advances-in-mathematics/

[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean

Dieser Artikel stammt aus dem WeChat-Offiziellen Konto „QbitAI“, Autor: Meng Chen, veröffentlicht mit Genehmigung von 36kr.