PSI: KI von Anthropic beweist Quanten-Vermutung

Physical Superintelligence (PSI), ein auf Physik spezialisiertes KI-Startup, teilte am Freitag, den 6. November, mit, dass ein von ihnen entwickeltes Forschungssystem die Aaronson-Ambainis-Vermutung, ein seit 2008 offenes Problem der Quantenkomplexität, mithilfe von Instanzen eines nicht-öffentlichen Anthropic-Modells bewiesen hat. Das Unternehmen gab an, dass das System am dritten Tag eines Durchlaufs auf der eigenen Infrastruktur einen vollständigen Beweis erbrachte und der Lean-Beweisassistent diesen akzeptierte. Das Ergebnis hat noch keine wissenschaftliche Begutachtung durchlaufen. Derzeit handelt es sich um eine Behauptung des Unternehmens, aber das Papier und der maschinell geprüfte Beweis sind öffentlich zugänglich, sodass externe Experten sie testen können.psi.inc

Was der Beweis behauptet

Die Vermutung stellt die Frage, ob Quantencomputer bei zufälligen Eingaben exponentiell schneller sein können als herkömmliche Computer, da diese fast nie die verborgenen Muster enthalten, die Algorithmen wie Shors Faktorisierungsmethode ausnutzen. Aaronson und Ambainis zeigten, dass Quantenbeschleunigungen bei zufälligen Eingaben höchstens polynomiell wären, wenn ihre Aussage über beschränkte Polynome niedrigen Grades zuträfe. Die Ankündigung von PSI fasste das Ergebnis so zusammen: "Ein Quantencomputer kann nicht exponentiell viele Abfragen einsparen, es sei denn, die Zeichenfolge weist ein seltenes Muster auf". Das Theorem begrenzt, wie oft ein Algorithmus seine Eingabe liest, nicht die gesamte Rechenzeit, was Raum für praktische Quantenvorteile lässt.thequantuminsider.com+1

Der erste Beweis lieferte eine schwächere Schranke. Nachdem PSI das System auf verwandte offene Probleme angesetzt hatte, verbesserte es das Ergebnis zweimal, und Lean akzeptierte die endgültige Version. Die Argumentation folgt einem Plan von Shachar Lovett und Jiapeng Zhang. Sie ersetzt eine Ungleichung, die sie als Vermutung offen gelassen hatten, durch eine neue, die durch die Paarung von Eingabeeinstellungen mittels einer Determinante bewiesen wurde.psi.inc

Menschliche Rollen und Überprüfungen

PSI-Mitarbeiter David Turturean baute und betrieb das System, wies das Modell an, das Papier zu entwerfen, und ist für dessen Korrektheit verantwortlich. Die Berater Jim Halverson und Phiala Shanahan prüften den Beweis und kommentierten die Formalisierung. Das GitHub-Repository des Projekts gibt an, dass der Beweis, das Papier und die Formalisierung von KI-Modellen erstellt wurden. Es heißt dort auch, dass die Lean-Theoreme keine Platzhalter oder zusätzlichen Axiome enthalten und von zwei unabhängigen Kernel-Implementierungen erneut geprüft wurden. Leser müssen dennoch bestätigen, dass die formale Aussage mit der ursprünglichen Vermutung übereinstimmt.github.com+1

Die Stanford-Forscher Guy Blanc, Jordan Docter, Carmen Strassle und Li-Yang Tan lösten im August einen Spezialfall. Sie haben den vollständigen Beweis gelesen und nannten ihn in einer von PSI veröffentlichten Stellungnahme "ein riesiges Ergebnis", bei dem "alles auf eine fast magische Weise zusammengeführt wird".psi.inc

Offene Fragen

PSI hat nicht mitgeteilt, welches Anthropic-Modell verwendet wurde, und Anthropic reagierte nicht auf eine Anfrage um Stellungnahme. Die Ankündigung folgt auf die Behauptung von OpenAI im September, ein Problem im Zusammenhang mit den Navier-Stokes-Gleichungen gelöst zu haben, und befeuert die Debatte darüber, was KI für die Karrieren von Mathematikern bedeutet.businessinsider.com