Gestern hat OpenAI 722 KI-Mathematik-Manuskripte auf einmal veröffentlicht, und gerade eben hat es 3 davon zurückgezogen.
Der Grund ist einfach: Ein Plus-Minus-Zeichen wurde falsch geschrieben.
Gerade eben hat OpenAI sein erstes Update-Log im Repository openai/math veröffentlicht. Das Log zeigt, dass OpenAI 3 Manuskripte zurückgezogen, 14 überarbeitet und die Zitate für weitere 13 aktualisiert hat. Die Gesamtzahl der Manuskripte im Repository sank von 722 auf 719.
Ein Plus-Minus-Zeichen bringt drei Arbeiten zu Fall
Die drei zurückgezogenen Arbeiten beziehen sich alle auf die Hodge-Vermutung, eines der Millennium-Probleme:
Algebraizität von Weil-Klassen auf gespaltenen abelschen Achtfachen
Algebraizität von Kuga-Satake-Korrespondenzen für K3-Flächen
Die rationale Hodge-Vermutung für Produkte von K3-Flächen
Das Problem liegt in der ersten Arbeit. In der Rückzugsnotiz schrieb OpenAI, dass die Arbeit in einem entscheidenden Argument das Vorzeichen einer bestimmten geometrischen Operation als +1 festhielt, während es gemäß der eigenen Konvention der Arbeit -1 sein sollte.
https://github.com/openai/math/blob/main/history.md
Ein Plus gegenüber einem Minus macht einen gewaltigen Unterschied. Eine Zählung, die sich hätte aufheben und letztlich null ergeben sollen, wurde zu einer von null verschiedenen Zahl. Ein klassisches Theorem, auf das sich die Arbeit stützt, hat als Voraussetzung genau, dass diese Zählung null sein muss. Da die Voraussetzung fehlschlägt, verliert die gesamte nachfolgende Konstruktion ihre Grundlage.
Die anderen beiden Arbeiten haben diese Konstruktion beide übernommen, daher wurden sie ebenfalls zurückgezogen.
In allen drei Rückzugsnotizen betonte OpenAI jedoch denselben Satz: Zurückgezogen wird der Beweis, was nicht bedeutet, dass diese mathematischen Aussagen selbst falsch sind. Die ursprünglichen Manuskripte wurden auch nicht gelöscht und können weiterhin über archivierte Links eingesehen werden.
Diese drei Arbeiten gehören alle zur Ergebnisgruppe Nr. 032 des Repositories, also zu den zuvor am meisten beachteten Ergebnissen im Zusammenhang mit der Hodge-Vermutung.
Nach dem Rückzug änderte sich auch der Name dieser Gruppe: von "Hodge- und Kuga-Satake-Ergebnisse für alle projektiven K3-Flächen" zu "die rationale Hodge-Vermutung für CM-abelsche Varietäten".
Mit anderen Worten, der Teil der Schlussfolgerungen, der K3-Flächen betrifft, wurde aus der Liste entfernt. Die Kernschlussfolgerung dieser Gruppe, nämlich der Beweis der rationalen Hodge-Vermutung für alle komplexen CM-abelschen Varietäten, bleibt weiterhin erhalten, und die neue Version dieser Arbeit hat nur die Zitate aktualisiert.
Erwähnenswert ist, dass die fehlerhafte Arbeit auf den 18. September datiert ist, was sie zu einem der frühesten Manuskripte im Repository macht. Von ihrem Datum bis zur öffentlichen Veröffentlichung vergingen fast drei Wochen, und sie wurde innerhalb von ein oder zwei Tagen nach der Veröffentlichung zurückgezogen. Wer den Fehler entdeckt hat, sagte OpenAI nicht.
Weitere 14 Arbeiten wurden überarbeitet
Zusätzlich zu den Rücknahmen überarbeitete OpenAI auch 14 Manuskripte, einschließlich der Korrektur von Beweisen, der Berichtigung von Schlussfolgerungen und der Klärung von Voraussetzungen und Abhängigkeiten.
Diese 14 betreffen Lipschitz-Höhen und das Ashkin-Teller-Modell in der statistischen Physik (4 Arbeiten), das Kähler-Minimalmodellprogramm und Abundanz in der komplexen Geometrie (6 Arbeiten), symplektische Geometrie (2 Arbeiten), allgemeine Berechnung für Navier-Stokes-Fluide (1 Arbeit) und eine BSD-Formel-Arbeit, aus der veraltete Zitate entfernt wurden.
Eine Überarbeitung ist recht repräsentativ. Ergebnis-Familie Nr. 342 behauptete, die von Simon Donaldson vorgeschlagene Vermutung der "tame pushforward compatibility" zu beweisen. Die Hauptschlussfolgerung änderte sich nicht, und es gibt eine Lean-Formalisierung. Aber eine stärkere beiläufige Schlussfolgerung in der Arbeit erwies sich als überzogen: Die überarbeitete Version schränkt sie auf einen spezifischen Fall ein und fügt außerdem ein Beispiel hinzu, das zeigt, dass sie im Allgemeinen nicht gilt.
Formalisierungsrate: 42 %
Das Update fügte außerdem 6 Lean-Formalisierungen und 5 ergänzende Hilfsergebnisse hinzu. Nach OpenAIs Abrechnung wurden die Hauptergebnisse von 300 Manuskripten inzwischen formalisiert, was etwa 42 % aller 719 ausmacht.
Unter den neu hinzugefügten Formalisierungen haben mehrere beträchtliches Gewicht, wie die 103. Ergebnis-Familie in der theoretischen Informatik, die behauptet zu beweisen, dass logarithmische Speicherberechnung vollständig derandomisiert werden kann (L = RL = BPL).
Es sollte beachtet werden, dass die "etwa sechzig Prozent", über die wir zuvor berichtet haben, nach Ergebnis-Familien gezählt wurden, was bedeutet, dass, solange eine Arbeit in einer Familie mit einer Formalisierung versehen ist, sie gezählt wird; die von OpenAI bekannt gegebenen 42 % werden nach einzelnen Hauptergebnissen gezählt, was den tatsächlichen Anteil, der Zeile für Zeile von einem Computer überprüft wurde, besser widerspiegelt.
Wo Fehler auftreten, gibt es keine Lean-Aufsicht
Ein Vergleich mit dem Repository-Verzeichnis offenbart ein Muster: Der Inhalt, der diesmal zurückgezogen und wesentlich überarbeitet wurde, fällt fast ausschließlich in die Teile ohne Lean-Formalisierung.
Dies bestätigt auch die frühere Warnung aus der Mathematikgemeinschaft: Ergebnisse, die nicht formalisiert und nicht von Fachleuten begutachtet wurden, können derzeit nur als "Behauptungen" betrachtet werden.
Glücklicherweise wurde dieses Erratum recht ordentlich behandelt: Die Fehler wurden klar dargelegt, die Abhängigkeitskette erklärt und die alte Version zur Referenz verfügbar gehalten, im Einklang mit dem Prinzip der "Änderung mit Spur", das von der Mathematics and Artificial Intelligence Advisory Group des Institute for Advanced Study empfohlen wird.
Doch nur zwei Tage, nachdem mehr als 700 Manuskripte veröffentlicht worden waren, kam das erste Erratum. Es wird höchstwahrscheinlich nicht das letzte sein.
Dieser Artikel stammt vom WeChat-öffentlichen Konto "Machine Heart" (ID: almosthuman2014), Redakteur: Panda
