Automatisiertes System löst Aaronson-Ambainis-Quantenvermutung in drei Tagen
Das Physik-Forschungs-Start-up PSI nutzt Modelle von Anthropic und die Lean-Verifikation zur Bewältigung einer 18 Jahre alten Rechenfrage.
Automatisch aus dem englischen Original übersetzt Original lesen
Ein rechnergestütztes Forschungssystem hat einen formalen mathematischen Beweis für die Aaronson-Ambainis-Vermutung geliefert, ein 18 Jahre altes ungelöstes Problem über die Grenzen des Quantencomputings. Das Physik-Forschungsunternehmen PSI gab bekannt, dass seine automatisierte Plattform die Verifikation innerhalb von drei Tagen erbrachte, indem sie künstliche Intelligenz nutzte, um zu untersuchen, wann herkömmliche Maschinen Quantenalgorithmen approximieren können.
Eine 18 Jahre alte Grenze des Quantenvorteils
Die erstmals im Jahr 2008 formulierte Aaronson-Ambainis-Vermutung untersucht die genauen Grenzen, an denen Quantenprozessoren einen exponentiellen Geschwindigkeitsvorteil gegenüber herkömmlichen digitalen Architekturen behalten. Wie Interesting Engineering berichtet, konzentriert sich die Vermutung auf die Frage, ob Quantenalgorithmen mit einer spezifischen mathematischen Struktur von klassischer Hardware mit lediglich polynomiellem Mehraufwand simuliert werden können. Wenn klassische Maschinen Prozesse bei zufällig gewählten Eingaben innerhalb polynomieller Grenzen simulieren, verringert sich die scheinbare Leistungslücke erheblich. Etablierte Spezialverfahren wie der Shor-Algorithmus zur Faktorisierung ganzer Zahlen bleiben von der Vermutung unberührt, da die mathematische Fragestellung eine ganz bestimmte Teilmenge von Quantenberechnungen betrifft.
Automatisierung formaler Beweise mit Lean
Um die Vermutung anzugehen, leitete der Forscher David Turturean die Initiative bei PSI, entwickelte den automatisierten Forschungs-Workflow, formulierte das Rechenproblem und überwachte die Ausführung. Das System lief auf der internen Infrastruktur von PSI unter Einsatz eines proprietären, nicht öffentlichen Modells für künstliche Intelligenz, das von Anthropic entwickelt wurde. Während des Testlaufs generierte die Plattform formale Aussagen, die direkt in Lean eingespeist wurden – einen interaktiven Beweisassistenten, der dafür entwickelt wurde, zu überprüfen, ob logische Sequenzen festgelegten mathematischen Axiomen strikt folgen. Das System überarbeitete die Argumentation daraufhin zweimal und erzeugte ein Endergebnis, das Lean ohne logische Diskrepanzen akzeptierte.
Unabhängige Verifikation und akademische Überprüfung
Eine formale Codeüberprüfung gewährleistet die interne Konsistenz, doch Mathematiker müssen nach wie vor sicherstellen, dass das übersetzte Theorem mit der ursprünglichen Behauptung von 2008 übereinstimmt. Der Physiker Jim Halverson prüfte die Beweisstruktur, während die theoretische Physikerin Phiala Shanahan vom MIT die in Lean erstellte Formalisierung begutachtete. Parallel dazu begann ein mathematisches Forschungsteam der Stanford University – bestehend aus Guy Blanc, Jordan Docter, Carmen Strassle und Li-Yang Tan – mit der Auswertung des Ergebnisses. Die Stanford-Gruppe, die bereits im August 2026 einen Spezialfall der Aaronson-Ambainis-Vermutung bewiesen hatte, verfasst derzeit eine zusammenfassende Fachpublikation, um die Ergebnisse von PSI der breiteren wissenschaftlichen Gemeinschaft vorzustellen.
Nächste Schritte für automatisierte wissenschaftliche Entdeckungen
Das Projekt stellt eine praktische Demonstration von Innovationen in der maschinengestützten Mathematik durch PSI dar, ein Start-up, das im September 2026 öffentlich an den Start ging, um autonome Entdeckungssysteme zu entwickeln. Während Lean eine programmatische Validierung der Logik liefert, hat der Beweis das standardmäßige Peer-Review-Verfahren in der akademischen Physik-Community noch nicht vollständig durchlaufen. Künftige Veröffentlichungen und Begutachtungen durch externe Theoretiker werden zeigen, ob der Beweis die Aaronson-Ambainis-Vermutung vollständig auflöst.
