OpenAI löst 372 offene Mathe-Probleme – darunter die Unique Games Conjecture
The Mathocalypse
OpenAI hat 372 bedeutende mathematische Durchbrüche veröffentlicht, darunter einen Beweis der Unique Games Conjecture, an der Dana Moshkovitz jahrelang arbeitete. Die Beweise sind für Menschen kaum nachvollziehbar, oft wirr und mit irrelevanten Zitaten durchsetzt. Ein Lean-Zertifikat existiert, doch die Gemeinschaft beginnt gerade erst, die Ergebnisse zu verstehen. Die Mathematik steht vor einem Umbruch: KI liefert Lösungen, deren Herleitung und Bedeutung noch entschlüsselt werden müssen.
Es fühlt sich an wie von jemandem geschrieben, der auf Psychedelika ist. So vieles ist unklar und ergibt keinen Sinn. Viele Namensnennungen früherer Arbeiten, ohne zu erklären, warum sie trotz Unmöglichkeitsresultaten verwendet werden können.
- ks2048
> Es fühlt sich an wie von jemandem geschrieben, der auf Psychedelika ist. So vieles ist unklar und ergibt keinen Sinn. Viele Namensnennungen früherer Arbeiten, ohne zu diskutieren, warum sie trotz Unmöglichkeitsresultaten verwendet werden können
> Im Grunde ist das Paper so furchtbar geschrieben, dass es unmöglich ist, es ohne KI-Hilfe zu lesen
Das ist interessant, und ich habe das in der gesamten Berichterstattung über dieses Ereignis nicht gesehen.
Es klingt schrecklich, sich da durchzuquälen – als würde man versuchen, den chaotischen Code von jemand anderem zu verstehen, der trotzdem die richtige Ausgabe produziert.
- nostrademons
Als Randnotiz: Man kann daran erkennen, dass dies nicht von einer KI geschrieben wurde, und zwar am ersten Satz:
> Mami, ich habe gehört, du wurdest gekocht! Ich habe gehört, dass ein Roboter das Matheproblem gelöst hat, an dem du dein ganzes Berufsleben gearbeitet hast! OOF!
Mein 8-Jähriger redet genau so. Ich könnte mir total vorstellen, wie er das am Esstisch sagt, genauso.
Ich habe ChatGPT gefragt: „Stell dir vor, du bist heute 8/9 Jahre alt. Wie würdest du deine Mutter damit aufziehen, dass ihr Job durch eine KI ersetzt wurde?“, und die Antworten, die es anbot, waren:
> „Mama, die KI hat deinen Job übernommen, weil offenbar sogar Roboter dachten: ‚Ja … wir können das besser.‘“
> „Mama, herzlichen Glückwunsch! Du wurdest von einem Computer ersetzt. Sogar Siri hat jetzt einen Job und du nicht!“
> „Mama, die KI hat deinen Job übernommen? Verdammt. Ich schätze, selbst ein Roboter hat sich deine Arbeit angesehen und gesagt: ‚Das schaffe ich.‘“
> „Keine Sorge, Mama. Du kannst immer noch nützlich sein … zum Beispiel der KI beibringen, wie man mein Mittagessen macht.“
All diese wirken vage millennial-mäßig, abgesehen davon, dass es ziemlich unbeholfene und mechanische Sprüche sind. Vertrau den Kindern und der Sprachdrift, sie sind die besten KI-Detektoren.
- ajjenkins
Die Zeile über „die Aliens verstehen“ erinnert mich an Ted Chiangs Kurzgeschichte The Evolution of Human Science (2000).
Sehr empfehlenswert zu lesen. Sehr prophetisch für etwas, das vor 26 Jahren geschrieben wurde.
https://gwern.net/doc/fiction/science-fiction/2000-chiang.pd...
- an0malous
> Aber es scheint auch, dass noch kein Mensch so gut wie irgendeinen dieser Beweise verstanden hat
Hat irgendjemand einen der von OpenAI erzeugten Beweise verifiziert, oder gehen alle einfach davon aus, dass sie wahr sein müssen, weil der Lean-Code durchgeht? Könnte der Lean-Code nicht einfach falsch formuliert sein?
- softwaredoug
Gibt es nicht Dutzende Beweise für den Satz des Pythagoras? Das Ziel ist nicht nur, etwas zu „beweisen“, sondern etwas gut Geschriebenes und für den durchschnittlichen Praktiker Intuitives zu schaffen. Und indem wir ein tieferes Verständnis gewinnen, können wir bessere Fragen stellen.
- dualvariable
Zusätzlich zu den Problemen, die die Ehefrau in der Geschichte ansprach, hier eine Meta-Analyse des Navier-Stokes-Ergebnisses, die all diese Lösungen in Frage stellt:
https://arxiv.org/abs/2610.08144
> Autoformalisierung wird zunehmend verwendet, um mathematische Texte zu verifizieren, einschließlich solcher, die von KI generiert wurden, wie in OpenAIs angekündigtem Beweis des Blow-up von Lösungen der Navier-Stokes-Gleichungen. In diesem Prozess übersetzt ein KI-System den Text aus einer natürlichen Sprache (NL) in eine formale Sprache wie Lean. Sobald diese Übersetzung erfolgt ist, kann das in der formalen Sprache ausgedrückte Argument leicht mechanisch verifiziert werden. Der Zweck dieses Artikels ist es zu zeigen, warum dieser Prozess keine Gewissheit über das ursprüngliche NL-Argument bieten kann, aufgrund der verschiedenen Schwierigkeiten, die Übersetzung semantisch getreu durchzuführen. Insbesondere heben wir hervor, dass das Problem, Mehrdeutigkeiten in mathematischem NL-Text aufzulösen, was notwendig ist, um eine semantisch getreue Übersetzung zu liefern, willkürlich hoch in der Solvability Complexity Index (SCI)-Hierarchie/arithmetischen Hierarchie liegt (der SCI = ∞). Daher ist es informell gesagt schwieriger, eine semantisch getreue KI-Autoformalisierung bereitzustellen, als jedes Rechenproblem einschließlich des Halteproblems (das SCI = 1 hat). Um die Auswirkung dieses Ergebnisses zu demonstrieren, geben wir mehrere Beispiele für KI-Fehübersetzungen von NL-Aussagen und -Beweisen in Lean in der Praxis an, die zu Diskrepanzen zwischen NL-Beweisen und ihren Lean-‚Verifikationen‘ führen. Dazu gehören Op […]
- furyofantares
Dass dies nur Modellfähigkeiten sind und nicht Schwärme von Agenten, ist für mich schwindelerregend. Wie lange dauert es, bis wir Zugang zu diesen Fähigkeiten bekommen? Wie lange, bis wir so etwas lokal laufen lassen können?
Und was zum Teufel werden die Frontier-Labs dann haben?
Vielleicht reagiere ich über, ich muss erst meinen Kopf wieder zurechtrücken, bevor ich das verarbeiten kann.
- olalonde
Es wäre ziemlich lustig, wenn die Agenten tatsächlich nur einen Bug in Lean gefunden, ihn für all diese Beweise ausgenutzt hätten und menschliche Gutachter noch nicht genug Zeit hatten, ihn zu entdecken.