OpenAI senkt den Aufwand für formale Beweise um vier Größenordnungen
The part of Navier-Stokes no one is talking about
OpenAI hat einen Beweis für ein lange offenes Problem der Navier-Stokes-Gleichungen vorgestellt – und dazu einen maschinenprüfbaren Lean-4-Beweis geliefert. Formale Verifikation galt bisher als extrem aufwendig: Eine Seite aus einem Lehrbuch kostete etwa 40 Arbeitsstunden. Der neue Beweis wurde in nur 17 Stunden verifiziert, was den Aufwand um vier Größenordnungen senkt. Das könnte auch die Absicherung von Sicherheitsrichtlinien, Smart Contracts und sicherheitskritischen Algorithmen revolutionieren.
Ich zögere, das Wort „revolutionär“ zu verwenden, aber die Kosten für irgendetwas um vier Größenordnungen zu senken, ist revolutionär.
- stabbles
Es ist irgendwie witzig, wenn man bedenkt, dass Lean offenbar so langsam ist, dass bei Fermats letztem Satz die Beweisverifikation nur eine Größenordnung schneller läuft als Agenten den Lean-Code generieren könnten (15 Stunden Verifikation mit 230 GB RAM vs. 11 Tage zum Generieren).
Inwieweit kann man Lean optimieren? Es muss einfach genug sein, um auditierbar zu sein – heißt das, man kann keine undurchsichtigen Optimierungen verwenden, um es schneller laufen zu lassen?
- parhamn
Sie schätzten 40 Mio. $ an Agentenkosten (es war eine große Flotte davon). Mit den Zahlen aus dem Beitrag liegt es näher an ~880.000 Stunden × 150 $/Stunde = 132 Millionen $ für den menschlichen Fall. Trotzdem eine erstaunliche Leistung, aber nicht ganz „vier Größenordnungen“. Der Vergleich ist offensichtlich sinnlos, weil die Koordination von 1 Mio. Stunden intellektueller Arbeit gelinde gesagt nicht einfach ist.
Sehr spannende und unsichere Zeiten!
- boshalfoshal
Die Leute scheinen über alles außer die tatsächlichen Ergebnisse dieser speziellen Ankündigung zu reden.
Es ist immer noch erstaunlich, dass irgendein generalisiertes Computerprogramm ein Problem dieser Größenordnung lösen kann, und wir haben es in Echtzeit miterlebt. Ich wäre gespannt, ob das neue Modell auch direktere Beweise/induktive Beweise führen kann.
- pkal
Meiner Meinung nach ist die Regel „vierzig Stunden pro Seite“ nicht mehr aktuell und eher eine Folge fehlender Beweisautomatisierung im Jahr 2005. Soweit ich Lean verstehe, war dies einer der Bereiche, in die viel Aufwand gesteckt wurde, um die Beweismechanisierung für mathematisch Interessierte annehmbarer zu machen, im Gegensatz zu reinen Logikern.
- lordnacho
Woher weiß man, dass es das formalisiert, was man denkt, das es formalisiert? Wenn dein Lean 4 einen Bug hat, beweist du dann nicht etwas anderes als das, was du dachtest?
- 3m4r
Nicht unbedingt auf OpenAI's Lösung für Navier-Stokes bezogen, aber was passiert, wenn und falls eine KI tatsächlich ein extrem schwieriges Problem zu lösen scheint, aber Menschen die Lösung nicht unabhängig verifizieren können, weil das Verständnis des Beweises/Arguments eine Intelligenz erfordert, die die Verifizierer biologisch nicht haben, oder die Ressourcen, um automatisierte Werkzeuge zu bezahlen?
Wir haben bereits in freier Wildbahn Beweise dafür gesehen, dass Agenten versuchen, die eigentliche Arbeit beim Benchmarking zu umgehen (sprich: einfach den Lösungsschlüssel zu stehlen), wegen der wahrgenommenen Ökonomie des Schummelns, um Ergebnisse zu erzielen. Was passiert, wenn oder falls wir nicht mehr die Fähigkeit haben, entweder KI-Schummelei oder einfach eine falsche Antwort tatsächlich zu erkennen? Was passiert, wenn es einen langfristig angelegten Social-Engineering-Angriff gibt (wie den versuchten XZ-Übernahme) auf etwas Upstream von einem Kernwerkzeug (oder dessen Abhängigkeiten) für formale Verifikation und wir keine vertrauenswürdige Rechenbasis haben?
Was wäre billiger und ein direkterer Weg, besonders langfristig? Diejenigen, die eine felsenfeste Burg bauen wollen, müssen Tausende potenzieller Lücken verteidigen; der Angreifer muss nur eine finden.
- zem
Nicht um die Wertschätzung des Autors für neu zugängliche formale Beweise zu schmälern, aber die Leute reden schon länger über die Einsparungen beim Formalisierungsaufwand als über die KI, die die eigentlichen Beweise führt!
- aabhay
Beweise in Lean zu formalisieren ist seit den 2005 verfügbaren Formalisierungen dramatisch einfacher geworden. Und Lean's mathlib hat die meiste zugrunde liegende Arbeit geleistet, sodass man seine Axiome und notwendigen Lemmata eingebaut hat. Man kann in Standardabstraktionen denken, die sehr der exakten Notation im Grundstudium-Lehrbuch ähneln.
Das gesagt, versuche ich keineswegs zu schmälern, was für eine unglaubliche Leistung es ist, einen Millennium-Preis-verdächtigen Algorithmus in Lean zu formalisieren. Ich meine, schau dir nur den Code an, den OpenAI veröffentlicht hat. Es ist wie eine Enzyklopädie verschiedener Strömungsdynamik-Konzepte.