OpenAI: Astra-Modell löst zehn langjährige mathematische Probleme für 2.000 Dollar

OpenAI enthüllte am Samstag, dass sein internes Modell Astra neue Ergebnisse für zehn Probleme in der Mathematik und theoretischen Informatik geliefert hat, die seit mindestens einem Jahrzehnt ungelöst waren. Das Unternehmen veröffentlichte zu jeder Behauptung maschinell überprüfbare Beweise und meldete Token-Kosten von etwa 2.000 Dollar zu aktuellen API-Preisen für alle zehn Lösungen.forbes+1

Verifizierte Beweise in verschiedenen Fachgebieten

Die Ergebnisse erstrecken sich über die Bereiche hochdimensionale Kugelpackung, Codierungstheorie, Kryptographie, extremale Kombinatorik und Quantenspieltheorie. Das Hauptergebnis ist die explizite Konstruktion einer nicht-sofischen Gruppe, eine seit 1999 offene Frage, die die Vermutung widerlegt, dass alle abzählbaren Gruppen sofisch sind. Astra widerlegte zudem Connes Starrheitsvermutung aus dem Jahr 1980 und löste drei Probleme aus dem Katalog von Paul Erdős, darunter Problem 183 über mehrfarbige Ramsey-Zahlen.newscientist+1

OpenAI veröffentlichte ein 249-seitiges Manuskript zusammen mit Lean 4-Beweiszertifikaten auf GitHub unter einer Apache 2.0-Lizenz und meldete eine "Sorry"-Anzahl von null, was bedeutet, dass kein Schritt in einem formalisierten Beweis unbewiesen blieb. Der Lean-Kernel liefert ein binäres Urteil: Entweder der Beweis kompiliert oder nicht, was die Notwendigkeit beseitigt, dem Output des Modells blind zu vertrauen.siliconangle+1

Thomas Bloom, der den Erdős-Problemkatalog pflegt, nannte die Ergebnisse "große Neuigkeiten" und stufte sie höher ein als das Gegenbeispiel für Einheitsabstände, das ein früheres OpenAI-Modell im Mai produziert hatte. Abhishek Saha von der Queen Mary University of London sagte, jede der zehn Lösungen "wäre eine bedeutende und beeindruckende Leistung".newscientist+1

Skeptiker mahnen zur Vorsicht

Die Ankündigung stieß auf deutliche Kritik. Gary Marcus, ein prominenter KI-Skeptiker, beschrieb die Veröffentlichung als "erstaunlich, aber massiv überverkauft" und argumentierte, dass der Erfolg in formal verifizierbarer Mathematik nicht auf Bereiche übertragbar sei, in denen die Verifizierung schwieriger ist. Er merkte an, dass die Zahl von 2.000 Dollar nur erfolgreiche Versuche abdecke und die Gehälter der Mathematiker und Informatiker ausschließe, die bei der Vorbereitung der Arbeiten geholfen haben.garymarcus.substack

Francesco Fournier-Facio von der University of Cambridge stellte die Transparenz der Arbeit in Frage und argumentierte, dass die Lösung zur Sofizität stark auf früheren Arbeiten von Andreas Thom und Gábor Kun aus den Jahren 2016 und 2019 beruhe. Die ursprüngliche Behauptung von OpenAI, dass bei allen zehn Problemen "seit mindestens einem Jahrzehnt keine Fortschritte beim Hauptergebnis erzielt wurden", wurde korrigiert, nachdem Fournier-Facio sie als inkorrekt bezeichnet hatte.newscientist

Breitere Auswirkungen

Astra selbst bleibt unveröffentlicht. OpenAI beschreibt es als eine Modellfamilie, die darauf ausgelegt ist, mehrere Agenten bei komplexen Aufgaben zu koordinieren. CEO Sam Altman hat das Modell politischen Entscheidungsträgern in Washington demonstriert, aber das Unternehmen hat kein Veröffentlichungsdatum bekannt gegeben oder ob es als GPT-6 oder eine andere Variante erscheinen wird.siliconangle

Der Zeitpunkt fällt in eine Phase, in der die mathematische Gemeinschaft gegen KI-Unternehmen mobil macht. Im Juni unterstützte die International Mathematical Union die Leiden-Erklärung, die davor warnt, dass KI-Firmen "veröffentlichte Forschung ohne Zustimmung nutzen, das Peer-Review-Verfahren umgehen und die Integrität von Beweisen und Zuschreibungen bedrohen".siliconangle