OpenAI zieht drei mathematische Ergebnisse zurück

Waren also die 3 zurückgezogenen Beweise diejenigen ohne Lean-Verifikation?

Wenn ja, warum haben sie dann Beweise, die mit Lean verifiziert wurden, mit Beweisen in natürlicher Sprache vermischt?

Das habe ich mich beim Lesen von Aaronsons Blog gefragt:

https://scottaaronson.blog/?p=10169

Oder zumindest sind wir uns ziemlich sicher, dass es ein Beweis ist! Es gibt ein Lean-Zertifikat, wie für einige der anderen 372 bahnbrechenden Ergebnisse (nicht für alle). Aber es scheint auch, dass noch kein Mensch so gut wie irgendeinen dieser Beweise verstanden hat.

Es scheint, das Offensichtliche wäre, in ZWEI Teilen zu veröffentlichen: die verifizierten und die, die vielleicht einige gute Ideen enthalten, aber auch Fehler haben könnten. Vermutlich wäre Letzteres für Menschen viel teurer zu verifizieren.

Ich denke, bei genauerem Hinsehen werden viele dieser vollständig KI-generierten Beweise auseinanderfallen. Selbst in Lean kann man Theorien aufbauen, die kompilieren, aber dennoch etwas anderes aussagen, als man eigentlich beabsichtigt. Es ist nur so, dass die Menge an Beweisen so unvorstellbar groß ist, dass es wahrscheinlich Jahre dauern wird, bis wir die Probleme finden, ähnlich wie bei der abc-Vermutung.

Ich finde das Paper über das Übertreffen von O(n log n) für die Ganzzahlmultiplikation auch ziemlich fischig, nicht sicher, aber es scheint zu gut, um wahr zu sein, ich habe das Gefühl, da muss ein subtiler Fehler drin sein. Vielleicht ist das nur ich, der diese kleinen Zahlen im Paper hasst, aber es scheint falsch, ja unnatürlich! Ich wäre ähnlich skeptisch bei einem Physik-Paper, das behauptet, die Lichtgeschwindigkeit um einen winzigen Bruchteil überschreiten zu können. Es gibt keinen Grund, warum n log n hier die natürliche Grenze sein sollte, aber ich sehe ein paar gute Intuitionen, also scheint etwas anderes, das nicht in eleganter Form dargestellt werden kann, für mich sehr "unmathematisch".

Wenn man so einen Datenauswurf macht, sollte alles davon formalisiert sein, es gibt einfach zu viel Material, um es von Hand zu überprüfen, und außerdem ist es von KI geschrieben, was es im Vergleich zu menschlicher Arbeit schwer lesbar macht.

Was für eine Zeitlinie, das Modell von OpenAI ist so gut, es veröffentlicht Hunderte von Mathematik-Papers.

Das neueste Modell findet sogar Fehler in zuvor veröffentlichten Mathematik-Papers!!!*

* bisher waren nur OpenAIs Mathematik-Papers fehlerhaft und mussten zurückgezogen werden.

So sieht es aus, wenn Software-Engineering-Praktiken auf die Mathematik treffen. "openai/math release 1.3.42: Papers 139 und 140 zurückgezogen, Vorzeichenfehler in Paper 47 behoben, zuvor zurückgezogenes Paper 85 wiederhergestellt, Argumente in Paper 101 refaktoriert".

Ich bin neugierig, ob der Rückzug darauf zurückzuführen ist, dass ein tatsächlicher Mathematiker die Papers angesehen und die Fehler bemerkt hat, oder ob sie ein Modell zum Korrekturlesen darauf angesetzt haben, was vermutlich nicht das erste Mal wäre, da sie das sicherlich vor der Veröffentlichung getan hätten. Beide Optionen haben interessante Implikationen.

3 Fehler (bisher) von ~400 ist immer noch eine ziemlich gute Trefferquote.

Also ist die Mathematik in die Phase "wirf Zeug an die Tafel und schau, ob es kleben bleibt" eingetreten..

Das ist einfach nur OpenAI, die mehr Arbeit stehlen.

Ich habe kein Problem damit, dass sie veröffentlichen. Ich habe kein Problem mit dem Prozess und der Art, wie sie damit interagieren. Ich freue mich, dass sie tatsächlich als Verwalter dieser Werke fungieren.

Abgesehen davon sollten sie die Leute bezahlen, die die Probleme verifizieren. Was mich wirklich stört, ist, dass wir wissen, dass alles, was im Prozess der Verifizierung veröffentlicht wird, in die nächste Trainingssession eingesaugt wird.