-
Einführung zu o3 und FrontierMath
- o3 ist OpenAIs neues Sprachmodell und erreichte 25 % auf dem geheimen FrontierMath-Datensatz.
- FrontierMath ist ein nicht öffentlich zugänglicher Datensatz mit schwierigen Mathematikaufgaben, wie sie von Epoch AI veröffentlicht wurden.
- Der Datensatz besteht aus Aufgaben wie „Finde diese Zahl!“ und fordert eindeutige, automatisch verifizierbare Antworten.
-
Schwierigkeit des FrontierMath-Datensatzes
- Die Aufgaben von FrontierMath sind für Forschungsmathematiker untypisch, und einige von ihnen erfordern Kenntnisse auf Doktoranden-Niveau.
- Die Datensatzfragen konzentrieren sich mehr auf das Auffinden von Zahlen als auf mathematische Beweise.
- Da sich Mathematiker vor allem darauf konzentrieren, Beweise oder Ideen zu finden, ist FrontierMath ein wichtiger Datensatz für die KI-Mathematikforschung.
-
Mathematische Fähigkeiten von KI
- KI kann derzeit Aufgaben auf High-School-Niveau gut lösen und soll voraussichtlich bald auch Universitätsprüfungen bestehen.
- Die Generierung innovativer Ideen über das Niveau eines fortgeschrittenen Grundstudiums bleibt jedoch weiterhin eine Herausforderung.
- Dass o3 25 % erreichte, ist bemerkenswert, aber der Einwand besteht, dass einige der Probleme auf College-Niveau sind.
-
Rolle der KI in der Mathematikforschung
- In der Mathematikforschung ist es entscheidend, Probleme der Art „Beweise diesen Satz!“ zu lösen.
- DeepMinds AlphaProof hat 4 Probleme der internationalen Mathematik-Olympiade 2024 gelöst, wobei einige vollständig mit Lean-bewiesenen Beweisen verifiziert wurden.
- Damit KI in der Mathematikforschung eine größere Rolle spielt, muss sie Beweise auf eine Weise erklären können, die für Menschen verständlich ist.
-
Zukunftsausblick
- Damit KI in der Mathematikforschung eine größere Rolle spielt, muss sie Beweise auf eine Weise erklären können, die für Menschen verständlich ist.
- Die Entwicklung von KI schreitet rasch voran, doch der Weg bleibt lang.
- Es ist noch unklar, wann KI die Hürde eines Bachelor-Niveaus überschreiten wird.
1 Kommentare
Hacker News Kommentar
In einem Reddit-Thread sind bei den drei Schwierigkeitsstufen 25 % T1 (am leichtesten) und 50 % T2. Von den fünf offenen Aufgaben, die der Autor gesehen hat, waren zwei T1 und zwei T2. Glazer beschrieb T1 als „IMO-/Bachelor-Niveau“, aber der Verfasser des Artikels sieht darin keine reinen Bachelor-Aufgaben. Die LLMs tun bereits Dinge, die den Autor hätte überraschen können.
Der Versuch, lineare Algebra mithilfe von ChatGPT zu verstehen, führte im echten mathematischen Arbeiten häufig zu absichtlos offensichtlichen Fehlern. Beispielsweise indexiert es jenseits der Dimension eines Vektors, versucht eine Matrixfaktorisierung für einen Skalar oder multipliziert Matrizen mit inkompatiblen Dimensionen.
O1 erkennt Fehler besser als 4o, macht aber immer noch viele unsinnige Fehler. Ohne Unterstützung durch jemanden mit etwas Hintergrundwissen ist es schwer, konsistente Ergebnisse zu erzeugen.
In einem Vortrag von Akshay Venkatesh wurde die Zukunft von „Mathematik-Berufen“ diskutiert, falls automatisierte Theorembeweise allgemeiner werden. Er sprach darüber, wie Fortschritte in der automatischen Schlussfolgerung die Art und Weise verändern könnten, wie Forschungsmathematik konzipiert und durchgeführt wird.
Als Elternteil eines 18-jährigen Sohnes, der Mathematik studieren möchte, macht man sich Sorgen, dass durch Automatisierung ein Beruf verschwinden könnte. Dennoch ist fraglich, ob LLMs ihn völlig ersetzen können. Da ein LLM nicht über unendliche Zeit und Ressourcen verfügt, um alles zu lösen, wird es aus meiner Sicht immer einen menschlichen Beitrag geben.
Ob man eine Sammlung von Aufgaben erstellen kann, in der ein LLM fast alles löst, weiß ich nicht, aber ich glaube nicht, dass daraus ein allgemeiner Problemlöser wird, der menschliches Schlussfolgern ersetzt. Erst wenn KI eine soziale Rationalität im Sinne menschlicher Unabhängigkeit entwickelt, ist echte Schlussfolgerung möglich.
Er zeigte Beispiele für grundlegende Fehler von ChatGPT. So wurde bei der Herleitung der Effizienzformel von Stop-and-Wait ARQ ein falscher Schritt angegeben. Als weiteres Beispiel lieferte ChatGPT auf die Bitte, trainierbare Syllogismen zu üben, inkonsistente Syllogismen.
Es wird die Möglichkeit diskutiert, dass der FrontierMath-Datensatz beschädigt ist. Wenn OpenAI die Fragen kennt, erwartet er, dass der nächste FrontierMath-Test über 80 % erreichen könnte.
Ein ähnliches Problem besteht in der Quantenforschung: Fortschritt muss durch Berechnungen belegt werden, die auf klassischen Computern nicht möglich sind. Als ChatGPT 25 % erreichte, stellte sich die Frage, wie nahe diese 25 % an den Fragen des Trainingssatzes lagen.
Er äußert Bedenken, dass ein Sprachmodell einen „Beweis“ der Riemannschen Vermutung liefern könnte. Mathematiker könnten versuchen, solche Beweise zu verifizieren, was jedoch sehr zeitaufwändig werden kann.
Es wird erwartet, dass bei der IMO 2025 keine Maschinen teilnehmen. Bei der IMO gibt es kein Konzept eines „Bewertungsrichters“; die Punkte werden zwischen den Teamleitern der Länder und den Prüfern ausgehandelt. Niemand wird hunderte Personen dazu bewegen, KI-Lösungen länger zu bewerten.