Sieben Forscher von Google Research reichten am 30. September ein Paper auf arXiv ein, das ein Multi-Agenten-System namens Cogentic vorstellt, das speziell für das Auffinden von Beweisen auf Forschungsniveau entwickelt wurde. Dem Paper zufolge nutzt das System Gemini als Basismodell und hat fünf offene Probleme in den drei Bereichen Online-Lernen, Auktionstheorie und Mechanismusdesign vorangebracht; sämtliche Beweise wurden im Nachhinein unabhängig von Fachleuten geprüft und zu vollständigen Papers mit Experten als Mitautoren ausgearbeitet.
Zu den Autoren zählen Yang Cai, der zugleich an der Yale University tätig ist, und Vineet Gupta, der zugleich bei Google DeepMind gelistet ist, außerdem Aranyak Mehta, Christopher Liaw, Di Wang und weitere. Das Paper ist den Kategorien cs.AI und cs.GT (Spieltheorie) zugeordnet.
Ein einzelner Durchlauf reicht nicht, also wird daraus eine Pipeline
Der Ausgangspunkt des Papers ist simpel: Sprachmodelle können bereits brauchbare mathematische Ideen liefern, aber bei Problemen, die mehrere Vermutungen gleichzeitig testen und über Tage hinweg vorangetrieben werden müssen, reicht eine einzelne Generierung nicht mehr aus.
Cogentic verteilt die Beweissuche auf verschiedene Rollen:
- Der Orchestrator behält den Gesamtzustand im Blick und entscheidet, wie viele Prover auf welche Richtung angesetzt werden;
- Prover schreiben parallel Kandidatenbeweise;
- Verifier suchen aus komplementären Blickwinkeln nach Fehlern, mit einer adversarialen Ausrichtung;
- Literatur-Rechercheure liefern Hintergrundmaterial;
- Das Ledger speichert nur geprüfte Zwischenergebnisse, die über mehrere Runden erhalten bleiben, sodass spätere Beweise direkt darauf verweisen können;
- Eine zusätzliche „Advisor"-Rolle beobachtet die Muster des gesamten Prozesses und passt laufend Parameter an.
Beweisen, Prüfen, erneut Beweisen – so geht es immer weiter. Das Ledger-Design löst ein altbekanntes Problem von Langzeitaufgaben: Ein Lemma, das das Modell in einer Runde hervorbringt, wird in der nächsten Runde oft vergessen oder anders formuliert; jetzt wird es nach bestandener Prüfung fest abgelegt.
Wie weit die fünf Probleme vorangebracht wurden
Laut den Ergebnissen des Papers:
- Online inverse lineare Optimierung: erstmals eine effiziente O(d)-Regret-Schranke, unabhängig vom Zeithorizont T, bei einem Rechenaufwand von O(d²) pro Runde;
- Wettbewerbskomplexität zweiseitiger Märkte: Beweis, dass genau 2 zusätzliche Verkäufer auf der kleineren Seite ausreichen, damit der Handelserlös die optimale Allokation erreicht;
- Anytime-Regret bei n Experten: ein Anytime-Algorithmus, dessen Konstante mit der Version fester Laufzeit übereinstimmt;
- Einfache Mechanismen und optimaler Umsatz: Das Näherungsverhältnis für einen einzelnen additiven Käufer wurde von 5,2 auf 3,52 verbessert;
- Price of Anarchy bei automatisiertem Bieten: bei 2 Bietern wird das Optimum 1,5 erreicht, bei n Bietern 2−1/(4n+1).
Bei den Kosten schreibt das Paper, dass die meisten Probleme Gemini in der Größenordnung von Hunderten Aufrufen benötigten, das schwierigste im Bereich von Tausenden; welche Gemini-Version konkret verwendet wurde, bleibt offen.
Im Vergleich zu den Beweis-Vorstößen von OpenAI
In der zweiten Jahreshälfte häufen sich Meldungen über KI, die Mathematik betreibt; nebeneinandergestellt liegt der Unterschied im Verifikationsansatz.
OpenAI legte im August mit Astra zehn Ergebnisse aus Mathematik und theoretischer Informatik vor, begleitet von einem 249-seitigen Paper und formalen Lean-Zertifikaten; der im September vorgestellte Navier-Stokes-Beweis setzte rund zehntausend Agenten ein, die 88 Stunden liefen, ebenfalls mit beigefügten Lean-Dateien. Maschinell prüfbare formale Zertifikate sind das Verkaufsargument, das OpenAIs Linie immer wieder betont.
Das Cogentic-Paper setzt den Schwerpunkt woanders: Innerhalb des Systems filtern adversariale Verifier einmal durch, nach dem Verlassen des Systems liest jeweils ein Fachmann jeden Beweis und schreibt ihn zusammen mit Experten zu einem formalen Paper aus. Auch der Umfang der Probleme ist enger gefasst: Alle fünf stammen aus dem eigenen Forschungsgebiet der Autoren – Probleme, die innerhalb des Fachgebiets beobachtet werden und von Fachkollegen beurteilt werden können, sobald sie gelöst sind.
Diese Auswahl macht die Ergebnisse leichter anerkennbar, der Preis dafür ist die Übertragbarkeit. Das Paper räumt selbst ein, dass die Probleme „aus dem Bereich ausgewählt wurden, mit dem die Autoren vertraut sind"; wie es in Bereichen aussieht, die den Autoren weniger vertraut sind, beantwortet das Paper nicht.
Die Leser kommen mit dem Schreibtempo nicht mit
Im Paper steht ein Satz, der fast dasselbe anspricht, worüber sich Terence Tao in seinem Vortrag im August Sorgen machte:
"A system like this can produce candidate results faster than they can be read."
„Ein solches System kann Kandidatenergebnisse schneller produzieren, als sie gelesen werden können."
Bei allen fünf Cogentic-Problemen haben Fachleute gegengeprüft, deshalb lässt sich von „verifiziert" sprechen. Sobald diese Orchestrierung für mehr Menschen geöffnet und auf mehr Probleme ausgeweitet wird, verlagert sich der Engpass auf die Gutachter. Das Paper nennt nicht, wie viel Zeit Fachleute für die Prüfung jedes einzelnen Beweises benötigten – genau diese Zahl entscheidet darüber, wie weit sich das System skalieren lässt.
Quellen: arXiv-Paper 2609.40324, CocoLoop, Google Research; Schranken, Näherungsverhältnisse und Größenordnungen der Aufrufzahlen für alle fünf Ergebnisse folgen dem Wortlaut des Papers.