Lean-Verifikation von KI-übersetzten Beweisen ist wertlos
Navier–Stokes Lost in Translation
Autoformalisierung übersetzt mathematische Texte in Sprachen wie Lean, um sie maschinell zu prüfen – etwa bei OpenAIs angeblichem Beweis der Blow-up-Lösungen der Navier-Stokes-Gleichungen. Doch die semantisch treue Übersetzung natürlicher Sprache ist nachweislich schwieriger als das Halteproblem (SCI = ∞). Anhand mehrerer Beispiele, darunter OpenAIs Navier-Stokes-Beweis, zeigt der Artikel, dass die Lean-Verifikation nicht dem ursprünglichen natürlichen Beweis entspricht.
Informell ist die Bereitstellung einer semantisch treuen KI-Autoformalisierung schwieriger als jedes Rechenproblem, einschließlich des Halteproblems (das SCI = 1 hat).
- ComplexSystems
Abgesehen vom üblichen Gezänk über KI scheint die Bombe in dieser Behauptung zu liegen:
"Insbesondere zeigen wir, dass der formalisierte Lean-Beweis nicht dem NL-Beweis der Blow-up von Lösungen der Navier-Stokes-Gleichungen entspricht."
Diese Autoren scheinen also zu behaupten, dass OpenAI Navier-Stokes gar nicht wirklich bewiesen hat. Wenn ich ihre Idee richtig verstehe, behaupten sie, dass das LLM die ursprüngliche "natürlichsprachliche" Idee von Navier-Stokes nicht korrekt formalisiert hat. Wenn das stimmt, würde es bedeuten, dass ihr angeblich Lean-Beweis gar kein Beweis von Navier-Stokes ist, sondern etwas, das eine fehlerhafte Übersetzung der ursprünglichen natürlichsprachlichen Idee ist. Wenn das korrekt ist, ist das eine wirklich kühne Behauptung, und ich würde gerne sehen, ob andere Forscher zustimmen.
- buzzy_hacker
Wenn ich das richtig verstehe, wird hier die Äquivalenz zwischen dem natürlichsprachlichen Beweis und dem Lean-Beweis in Frage gestellt, aber nicht die Korrektheit des Lean-Beweises?
- stared
Zur Auffrischung, was Navier-Stokes in wenigen Worten ist: https://p.migdal.pl/equations-explained-colorfully/#navier-s...
- vanyle
Dieses Paper ist eine große Menge Nichts. Erstens ist natürliche Sprache nicht so präzise wie Lean, also gibt es mehrere Möglichkeiten, ein NL-Argument nach Lean zu übersetzen. Wie in Abb. 1 gezeigt, hat das LLM das Argument über Wurzeln recht ordentlich und prägnant übersetzt.
Außerdem behauptet das Paper, dass die NL-Argumente von Navier-Stokes stärker seien als die Lean-Argumente. Meines Verständnisses nach war das Übersetzer-LLM einfach faul und hat den minimalen Code geschrieben, der das Theorem erfüllt, ohne die zusätzlichen stärkeren Behauptungen.
In mathematischen Arbeiten ist es üblich zu sagen: "Und übrigens beweist dies tatsächlich [stärkere Behauptung]", aber das würde eine KI mit dem präzisen Ziel einer Übersetzung niemals tun, da ihr Ziel darin besteht, den Beweis zu übersetzen, und nicht darin, gute Mathematik zu betreiben.
- infogulch
Das Paper zeigt, dass der Lean-Beweis und der Prosa-Beweis (PDF) nicht exakt übereinstimmen. Aber wenn das Lean-Theorem, das Lean akzeptiert hat, äquivalent zur ursprünglichen Problemstellung ist, die vom Clay Institute veröffentlicht wurde, ist diese Diskrepanz für die Gültigkeit des Beweises selbst ohne Belang. Das ist kein triviales Wenn: Die präzise Formulierung des Problems ist oft genauso schwierig wie der Beweis. Validierungsbemühungen sollten sich darauf konzentrieren, ob das Lean-Theorem äquivalent zu dem vom Clay Institute veröffentlichten ist.
Allerdings ist eine Lücke zwischen dem Lean-Beweis und dem PDF ärgerlich für die Interpretierbarkeit, und Interpretation ist ein legitimes Ziel, aber das spielt keine Rolle für die Gültigkeit des Beweises.
- sigbottle
Werden wir jemals in eine Krise der Bedeutungstheorie geraten?
_Angenommen_, es gibt zwei Fehlermodi:
- Der Lean-Kernel könnte immer einen Bug haben.
- Die formalisierte Aussage entspricht möglicherweise nicht dem, was _Mathematiker_ "eigentlich wollten".
Es liegt nahe, das Argument zu bringen: "Nun, selbst wenn man argumentiert, dass der Beweis Fehler enthalten kann, ist es sicherlich einfacher, die Problemstellung von etwas zu überprüfen als die Lösung."
(Eine "schöne Eigenschaft" ist, dass der Agent nicht einmal "Teilargumente korrekt" gemäß dem _zweiten_ Kriterium bekommen muss – vielleicht erfindet er im natürlichen Beweis ein Objekt, das sich subtil vom formalen unterscheidet, aber alles geht durch. Wenn man garantiert, dass die _ursprüngliche_ Aussage übereinstimmt, dann ist die einzige Möglichkeit der Lean-Kernel. Also rekursiert es in diesem Fall nicht unendlich.)
Aber "Definitionen" sind immer eine wirklich seltsame Sache, für die wir meiner Meinung nach keine guten Theorien haben? Wie quantifiziert man, wie viel Beschreibungskraft man braucht, um eine Frage auszudrücken? Oft ist in der Mathematik das Schwierige, die Definition richtig hinzubekommen – aber was, wenn die Definition selbst so komplex und unüberprüfbar wird, dass niemand sie mit irgendetwas in Übereinstimmung bringen kann? Nun, es scheint, dass viele interessante, langjährige mathematische Probleme "relativ" einfache Problemstellungen haben, sodass man sie leicht in Lean formalisieren könnte, aber ich bin nicht sicher, ob es wirklich eine Patentlösung mit Lean gibt oder ob es Schildkröten bis ganz nach unten sind.
Es ist wahrscheinlich egal, solange die KI weiter durch die Decke geht […]
- dooglius
Angesichts der hochgradig abstrakten Beschreibung der Beispiele denke ich, dass es weniger eine "Fehlübersetzung" ist, als vielmehr das LLM, das den Beweis während der Formalisierung anpasst. Zwischen m+4 und m+5 zu wechseln, ist eine ganz andere Sache als die Art von Mehrdeutigkeiten, die beim Parsen natürlichsprachlicher mathematischer Aussagen üblicherweise auftreten.
- Sniffnoy
Hm, wenn ich hier durchschaue, sehe ich nicht, wo sie angeben, was OpenAI tatsächlich anstelle von Navier-Stokes-Blowup mit Forcing bewiesen hat. Ich sehe, wo sie das für einige andere besondere Aussagen tun, die unterwegs verwendet werden, aber nicht für das Hauptergebnis.