OpenAI hat Mathematik in Code für seinen Navier-Stokes-Beweis falsch übersetzt
OpenAI mistranslated mathematics into code for its Navier-Stokes proof
Ein Team von Mathematikern behauptet, OpenAI habe bei der Veröffentlichung seiner Navier-Stokes-Beweise einen subtilen Fehler gemacht: Die Version für Menschen und die für Computer stimmen nicht überein. Der Fehler bedeutet nicht, dass die Beweise falsch sind oder das Problem nicht gelöst wurde, wirft aber die Frage auf, ob KI-generierte mathematische Ergebnisse immer zuverlässig sind. Anders Hansen von der University of Cambridge betont, dass solche Beweise von Menschen gelesen werden müssen, was eine enorme zusätzliche Belastung darstellt.
Was mit all diesen von großen Sprachmodellen generierten Beweisen geschehen muss, ist, dass sie von Menschen gelesen werden müssen, und das schafft eine enorme zusätzliche Belastung für Mathematiker.
- krackers
Duplikat von https://news.ycombinator.com/item?id=49994145
- jey
Diese Schlagzeile ist völlig falsch. Die passende Coding-Analogie ist eher die: Das Paper in natürlicher Sprache war das "Design-Dokument", bevor man es codiert hat; als man es dann als Lean4-Beweise codierte, stellte sich heraus, dass bestimmte Details leicht danebenlagen[1], und sie wurden korrigiert, während man die Implementierung in Code als maschinell prüfbare Beweise schrieb. Was, da bin ich sicher, eine extrem nachvollziehbare Situation für die meisten von uns hier ist. Aber das Paper bzw. das "Design-Dokument" wurde danach nicht korrigiert.
Ich denke außerdem, dass dieser "erst Paper, dann Code"-Ansatz inzwischen überholt ist. Der moderne Weg in KI-gestützten Workflows ist, zuerst iterativ an "Ableitungsskizze <-> maschinell prüfbarer Beweis" zu arbeiten und das Ergebnis schrittweise auszubauen. Man kann unterwegs natürlich `sorry`-Platzhalter stehen lassen und sie später füllen, man ist also nicht darauf beschränkt, komplett von unten nach oben vorzugehen. Sobald man schließlich einen `sorry`-freien Beweis seiner wichtigsten Top-Level-Aussagen (Theoreme) hat, kann man daran gehen, die Darstellung in LaTeX auf Basis des Lean-Codes zu schreiben.
1. Siehe https://arxiv.org/abs/2610.08144 für Details, aber ein Beispiel, das sie nennen, ist, dass eine entscheidende Schranke 5 zusätzliche Ableitungsordnungen erforderte (und in Lean auch so formuliert wurde), während das Paper behauptete, die Schranke gelte bereits mit nur vier weiteren Ableitungen.