KI-Modelle und Plattformen
PSI meldet maschinell geprüften Beweis der Aaronson-Ambainis-Vermutung
Unite.AI zu deinen bevorzugten Quellen auf Google hinzufügen
Physical Superintelligence gab am 6. November 2026 bekannt, dass ein internes Forschungssystem, auf dem Instanzen eines nicht öffentlichen Anthropic-Modells liefen, einen Beweis für die seit 2008 ungelöste Vermutung von Aaronson und Ambainis gefunden hatte – ein Problem aus der Quanteninformatik.
Das System erbrachte während des dritten Tages eines Durchlaufs auf PSIs eigener Infrastruktur einen vollständigen Beweis, den der Beweisassistent Lean akzeptierte. Anschließend stellte PSI dem System verwandte offene Probleme, woraufhin es das Ergebnis zweimal verbesserte, bevor Lean die endgültige Fassung akzeptierte. Das Manuskript und die Formalisierung in Lean 4 sind öffentlich zugänglich.
Was die Vermutung über quantenmechanische Beschleunigungen aussagt
Die Frage ist, wann Quantencomputer exponentiell schneller sein können als klassische Rechner. Shors Faktorisierungsalgorithmus aus dem Jahr 1994 beruht auf einer Struktur: Seine Eingabe enthält ein sich wiederholendes Muster, das der Algorithmus nutzen kann. Das Ergebnis von PSI betrifft den gegensätzlichen Fall zufälliger oder unstrukturierter Eingaben, bei denen ein solches Muster in der Regel fehlt.
Im Abfragemodell liest ein klassischer Algorithmus pro Abfrage ein Bit, während eine Quantenabfrage in einer Superposition über viele Positionen der Eingabe verteilt sein kann. PSI stellt in seiner Erklärung einen Zusammenhang zwischen diesem Modell und Polynomen her: Nach T Quantenabfragen ist die Wahrscheinlichkeit, dass der Algorithmus mit Ja antwortet, ein beschränktes Polynom der Eingabebits mit einem Grad von höchstens 2T. Einen Quantenalgorithmus zu simulieren, läuft daher auf die Frage hinaus, wie sich dieses Polynom abschätzen lässt, ohne exponentiell viele Eingabebits zu lesen.
In ihrer ursprünglichen Arbeit vermuteten Scott Aaronson und Andris Ambainis, dass jedes beschränkte Polynom niedrigen Grades eine Variable mit großem Einfluss besitzt. Sie bewiesen, dass sich unter der Annahme dieser Vermutung jeder Quantenalgorithmus mit T Abfragen für die meisten Eingaben durch einen klassischen Algorithmus mit polynomiell vielen Abfragen in T simulieren lässt. Daraus folgt ein polynomielles statt exponentielles Wachstum der Zahl klassischer Abfragen bei jedem festgelegten Approximationsfehler und jedem festgelegten Anteil ausgeschlossener Eingaben; ausgeschlossen sind dadurch jedoch nicht exponentielle Vorteile von Quantencomputern bei Problemen mit geeigneter Struktur.
Formal betrachtet das Repository ein reelles Polynom p mit einem Grad von höchstens d, dessen Werte auf dem diskreten Würfel zwischen 0 und 1 liegen. Ist seine Varianz über eine gleichverteilte Zufallseingabe mindestens ε, so hat eine Koordinate einen Einfluss von mindestens (8√15 / (125π⁴)) · ε^(5/2) / d⁶ und folglich mindestens (ε/d)⁷. Der Einfluss ist die erwartete quadrierte Änderung von p, wenn das Bit dieser Koordinate umgekehrt wird.
Wie der Beweis entwickelt und geprüft wurde
Der Beweis folgt einem von Shachar Lovett und Jiapeng Zhang entwickelten Plan, der auf fraktionalen Zertifikaten und Niveaumengen beruht. Er ersetzt jedoch eine Ungleichung, die in diesem Plan als Vermutung offengeblieben war, durch eine neue Ungleichung für alle Paare. Eine Determinante erzeugt eine bijektive Paarung von Eingabebelegungen. PSI zufolge geht diese Paarung über die schwächere Paarung aus David Reimers Butterfly-Lemma hinaus, weil sie zusätzlich begrenzt, wie oft die gepaarten Belegungen in jeder Koordinate übereinstimmen – eine für die neue Ungleichung erforderliche Schranke.
Das Repository gliedert den elementaren Beweis in vier Teile: Herleitung der Ungleichung für alle Paare aus der Determinante und der Bijektion, Integration über Niveaumengen, Mittelung über Koordinaten sowie Herleitung einer Zeilenschranke mithilfe einer punktweisen Sensitivitätsschranke. Zusammengenommen ergeben diese Schritte die explizite Schranke für den Einfluss.
Laut dem im Repository dokumentierten Audit enthält die formale Entwicklung weder Beweisplatzhalter noch hinzugefügte Axiome. Ihre Deklarationen wurden durch den Lean-Kernel und lean4lean, eine unabhängige Implementierung von Leans Typprüfer, erneut ausgeführt. Bei einem isolierten Durchlauf akzeptierte ein Vergleichsprogramm, das die nanoda- und Lean-Kernel verwendete, die vier abschließenden Theoreme; auf einem zweiten Rechner akzeptierte es eine korrekte kleine Lösung und verwarf vier absichtlich falsche.
Diese Prüfungen haben ausdrücklich benannte Grenzen. Leserinnen und Leser müssen weiterhin bestätigen, dass die formale Aussage mit der gedruckten Vermutung übereinstimmt. Die für Menschen lesbare Arbeit selbst ist nicht maschinell geprüft, und Leans Kernel und Compiler, die Definitionen in Mathlib sowie die für die Prüfung verwendeten Rechner bleiben Teil der Vertrauensbasis.
Rollen der Beteiligten und fachliche Begutachtung
David Turturean, Mitglied des technischen Teams von PSI, entwickelte und betrieb das Forschungssystem, steckte das Problem ab, veranlasste das Modell, einen ersten Entwurf zusammenzustellen, prüfte diesen Entwurf und trägt die Verantwortung für die Korrektheit der Arbeit. Im Repository wird offengelegt, dass KI-Modelle die mathematischen Aussagen, den ersten Entwurf und die Lean-Formalisierung erstellt haben. Jim Halverson prüfte den Beweis, und Phiala Shanahan kommentierte die Formalisierung.
Der Ankündigung ging eine am 19. August 2026 eingereichte Arbeit von Guy Blanc, Jordan Docter, Carmen Strassle und Li-Yang Tan voraus. Diese Autorinnen und Autoren hatten die Konsequenz für klassische Simulationen paralleler Quantenalgorithmen bewiesen: Ein Algorithmus mit t Abfragen und d Runden lässt sich für die meisten Eingaben mit t^(O(d²)) klassischen Abfragen simulieren. PSI zufolge haben alle vier den vollständigen Beweis gelesen, Kommentare beigesteuert und bereiten eine kürzere Darstellung für Fachleute vor.
In ihrer von PSI veröffentlichten Einschätzung schrieben die Forschenden: „Das ist ein gewaltiges Ergebnis. Es löst eine jahrzehntealte Vermutung, die wichtige Implikationen dafür hat, welche Probleme Quantenvorteile ermöglichen. Der Beweis greift auf mehrere Forschungsstränge zur Analyse boolescher Funktionen und zur probabilistischen Kombinatorik zurück und führt sie weiter. Alles wird auf eine geradezu magische Weise zusammengeführt.“
Die unmittelbare Überprüfung ist ungewöhnlich konkret: Unabhängige Kernel können das kodierte Argument erneut nachvollziehen, während Fachleute noch bestätigen müssen, dass die kodierte Aussage mit der Vermutung von Aaronson und Ambainis übereinstimmt, und die Teile der Arbeit beurteilen müssen, die nicht in Lean formalisiert sind. Diese Aufteilung bestimmt, was die maschinelle Prüfung belegt und was weiterhin einer mathematischen Begutachtung durch Menschen bedarf.
