Am 6. November gab das Start-up PSI (Physical Superintelligence) bekannt, dass sein internes Forschungssystem, das mit einem unveröffentlichten Anthropic-Modell läuft, die seit 18 Jahren offene Aaronson-Ambainis-Vermutung bewiesen hat. Der vollständige Beweis wurde am dritten Tag des Laufs niedergeschrieben und bestand die schrittweise Prüfung durch Lean, einen Beweisassistenten, der jeden Schritt kontrolliert. Es ist ein Meilenstein in der Behauptung, dass KI schwierige Mathematik bewältigen kann – doch vorerst bleibt es die Behauptung eines einzelnen Unternehmens: Das Papier wurde noch nicht begutachtet.
Was fragt die Vermutung eigentlich?
Die Aaronson-Ambainis-Vermutung fragt, wie viel schneller Quantencomputer bei unstrukturierten Daten sein können als klassische Computer. Sie behauptet, dass Quantenalgorithmen bei unstrukturierten Eingaben keine exponentielle Beschleunigung erreichen können. Die Frage ist seit 2008 offen. Im August bewies ein Team aus Stanford einen Spezialfall; PSI sagt, sein System habe das Ergebnis nun auf den allgemeinen Fall ausgeweitet. Hält der Beweis stand, zieht er eine klare Grenze um das, was Quantencomputing leisten kann.
Wie hat die Maschine bewiesen – und wie oft wurde geprüft?
Laut PSI lief das Forschungssystem ununterbrochen auf der eigenen Infrastruktur, schrieb am dritten Tag einen vollständigen Beweis und verbesserte das Ergebnis danach bei verwandten Problemen zweimal, wobei Lean die Endfassung jedes Mal akzeptierte. PSI veröffentlichte das Papier und die Lean-4-Formalisierung gemeinsam auf GitHub: 648 maschinell geprüfte Theoreme, keine leeren Beweisschritte und keine zusätzlich eingeführten Axiome; die Aussagen wurden außerdem durch den Lean-Kernel und die unabhängige Implementierung lean4lean erneut durchgespielt. PSI-Mitarbeiter David Turturean verantwortet die Korrektheit des Papiers, Mathematiker haben den Beweis geprüft.
Noch nicht in die Lehrbücher schreiben
Ein maschinell geprüfter Beweis ist noch keine Anerkennung durch die Mathematik. Lean kann nur garantieren, dass jeder Schritt den Regeln folgt, aber nicht bestätigen, dass die formalisierte Aussage mit der Vermutung übereinstimmt, wie Aaronson und Ambainis sie ursprünglich formuliert haben – das muss noch von Experten per Hand geprüft werden; der menschenlesbare Papiertext selbst wurde nicht maschinell geprüft; der Beweis zählt Abfragen, nicht die gesamte Rechenzeit; und das verwendete Modell wurde nicht offengelegt, Anthropic lehnte eine Stellungnahme ab. Ebenfalls am 6. November meldete Google DeepMind, dass KI-Agenten zwei neue Schwächen in der 1024-Bit-RSA-Verschlüsselung gefunden haben. KI kommt in Mathematik und Kryptografie gleichzeitig voran. Ob der Beweis von PSI der Prüfung durch Fachleute standhält, werden die Expertenprüfungen der kommenden Wochen zeigen.
