OpenAI bepreiste zehn Beweise mit fremden Tarifen

Ein 249-seitiges Papier kam mit einem Namen

Sébastien Bubeck, Forscher bei OpenAI, verbrachte den Samstag damit, dem Internet mitzuteilen, dass nichtsofische Gruppen existieren. Er beschrieb die Aussage als eines von vielen Ergebnissen, die Astra bewiesen habe, das er als nächstes großes Modell des Hauses bezeichnete, und erklärte, OpenAI veröffentliche zehn solcher Beweise samt Lean-Zertifikaten und Erläuterungen der Gedankengänge. Beigefügt waren ein 249-seitiges Manuskript, ein zweites Dokument mit diesen Erläuterungen und ein öffentliches Repositorium maschinell prüfbarer Zertifikate. Die anschließende Berichterstattung einigte sich rasch auf zwei Zahlen: zehn Probleme und rund 2.000 Dollar Rechenaufwand.

Das Manuskript selbst verwendet das Wort Astra kein einziges Mal. Es beginnt mit der Vorstellung einer Sammlung von Ergebnissen, die ein internes Modell von OpenAI erzielt habe, und widmet sich dann auf 249 Seiten Kugelpackungen, von-Neumann-Algebren und Schaltkreiskomplexität, ohne dasjenige zu benennen, das sie hervorbrachte. Der Name lebt in der Ankündigung. Die Mathematik lebt im Papier. Diese beiden Ebenen auseinanderzuhalten ist die eigentliche Arbeit für jeden, der das als Käufer und nicht als Zuschauer liest.

Was tatsächlich geliefert wurde, ist echt prüfbar

Die zehn Ergebnisse sind kein Beiwerk. Das erste bestimmt die exakte asymptotische Stärke des Cohn-Elkies-Programms und hebt den allgemeinen hochdimensionalen Kugelpackungsexponenten vom klassischen Kabatianskii-Levenshtein-Wert 0,59905576 auf etwa 0,6044, was laut Papier die erste Verbesserung dieser allgemeinen Schranke seit 1978 darstellt. Das dritte konstruiert eine explizite nichtsofische Gruppe und klärt, ob jede abzählbare Gruppe endliche Permutationsnäherungen zulässt. Das vierte widerlegt Connes' Rigiditätsvermutung, indem es unendlich viele paarweise nichtisomorphe Gruppen mit Eigenschaft (T) konstruiert, die eine gemeinsame Gruppen-von-Neumann-Algebra teilen. Die übrigen behandeln binäre und sphärische Codes, untere Schranken für die Berechnung der Permanente, Quanten-Parallelwiederholung, das Problem des nächsten Vektors, Ehrharts Volumenvermutung, eine superexponentielle untere Schranke für mehrfarbige Ramsey-Zahlen sowie Gegenbeispiele zu zwei Vermutungen der extremalen Graphentheorie, drei davon aus dem Katalog von Paul Erdos.

Jedes Ergebnis trägt eine Lean-4-Formalisierung in einem öffentlichen Repositorium, gebaut gegen mathlib auf Lean 4.32.0 und unter Apache-2.0-Lizenz freigegeben. Das ist der Teil dieser Veröffentlichung, der uneingeschränktes Lob verdient. Ein maschinell prüfbares Zertifikat bedeutet, dass ein Fremder mit einem Laptop das Argument bestätigen kann, ohne OpenAI zu vertrauen, ohne dem Modell zu vertrauen und ohne auf ein Peer-Review zu warten. Die meisten Fähigkeitsbehauptungen, die Unternehmern dieses Jahr vorgelegt wurden, kamen als Benchmark-Wert von derselben Partei, die das Modell verkauft. Diese hier kamen als Objekte, die keiner von beiden verpflichtet sind.

Die Danksagung nennt ein längst käufliches Modell

Am Ende des vierten Kapitels, nach dem Dank an Sorin Popa und andere für Kommentare und Durchsichten, steht ein Satz, den keine Berichterstattung aufgriff. Während der Vorbereitung dieses Manuskripts, schreibt OpenAI, habe man von unabhängiger und zeitgleicher Arbeit von Shuoxing Zhou erfahren, die ebenfalls ein Gegenbeispiel zu Connes' Rigiditätsvermutung erbrachte, entwickelt zum Teil mit Unterstützung von GPT-5.6 Sol. Sol ist nicht das unveröffentlichte Modell. Sol ist das Modell, das OpenAI heute verkauft, mit einer veröffentlichten Preisliste.

Nüchtern gelesen wurde eines der zehn Vorzeigeergebnisse zeitgleich von jemandem außerhalb des Labors erreicht, der mit allgemein verfügbarer Software arbeitete. Das schmälert die anderen neun nicht, und OpenAI legte es im eigenen Dokument offen, statt es entdecken zu lassen, was dem Unternehmen anzurechnen ist. Doch es ist der für Lizenzentscheidungen mit Abstand wichtigste Satz der gesamten Veröffentlichung, und er steht in einer Danksagung jenseits von 200 Seiten Operatoralgebra statt in der Ankündigung. Für deutsche Käufer, die KI-Leistungen ausschreiben, liegt genau dort die Differenz zwischen einer Demonstration und einer Leistungszusage.

Ein Preisschild, geliehen von einem anderen Produkt

Die Zahl von 2.000 Dollar hat im letzten Tag mehr Arbeit geleistet als jede andere Zahl der Veröffentlichung, und sie ist kein Preis. Sie ist eine Tokenmenge, bewertet zu den veröffentlichten API-Tarifen von GPT-5.6 Sol, umgerechnet rund 1.800 Euro. Astra hat keine veröffentlichten Tarife, weil Astra nicht verkäuflich ist. Die Zahl beantwortet also eine hypothetische Frage, nämlich was diese Token gekostet hätten, wären sie als Sol-Token abgerechnet worden, und sie wird als Antwort auf eine andere Frage gelesen, nämlich was mathematische Spitzenforschung nunmehr koste.

Was die Zahl nicht enthält, wiegt so schwer wie das, was sie enthält. Sie verrät nicht, wie viele Versuche den zehn geglückten vorausgingen, wie viel menschliche Steuerung sie formte, wie lange das alles in realer Zeit dauerte oder was Astra kosten wird, wenn es denn erscheint. OpenAI hat keinen Termin genannt und beschreibt es nur als nächste große Modellfamilie. Wer 2.000 Dollar als geltenden Satz für eine gelöste Vermutung ablegt, hat eine Zahl notiert, die nie eine Rechnung war, für ein Produkt, das sich noch nicht kaufen lässt.

Fragen Sie, was das ausgelieferte Modell leistet

Der Abstand zwischen dem Modell in der Vorführung und dem Modell auf der Preisliste ist die am zuverlässigsten manipulierte Größe in der KI-Beschaffung, und er bleibt meist unsichtbar, weil Anbieter ihn nicht dokumentieren müssen. Diese Veröffentlichung ist gerade deshalb ungewöhnlich, weil der Beleg über das ausgelieferte Modell im Manuskript des Anbieters selbst steckt. Die richtige Reaktion ist nicht Skepsis gegenüber der Mathematik, die formalisiert und prüfbar ist, sondern Disziplin beim Schluss daraus. Ein verifizierter Beweis ist eine Aussage über den Beweis. Er sagt nichts darüber, welches Modell ihn erzeugte, im wievielten Anlauf, mit wie viel Hilfe und zu welchem Preis.

Drei Fragen machen daraus Beschaffungspraxis. Welche Modellversion hat das gezeigte Ergebnis erzeugt, und ist diese Version heute allgemein verfügbar. Falls nicht, was leistet die allgemein verfügbare Version bei derselben Aufgabe. Und wie lauten die veröffentlichten Tarife für die Version, die ich tatsächlich betreiben würde. Ein Anbieter, der alle drei beantwortet, verkauft ein Produkt. Ein Anbieter, der nur die erste beantwortet, zeigt eine Forschungsvorschau, wie beeindruckend das beigefügte Artefakt auch sein mag.

Weiterlesen: Microsoft schulte seine Verkäufer darauf, Claude als langsamer zu bezeichnen  |  Google verwarf ein fast fertiges KI-Modell