FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
Dieser Beitrag stellt FormalRewardBench vor, den ersten Benchmark zur Bewertung von Reward-Modellen im Bereich des formalen Theorembeweisens, der auf 250 von Experten kuratierten Präferenzpaaren basiert und zeigt, dass fortschrittliche LLMs spezialisierte Theorembeweiser bei der Bewertung der Beweisqualität übertreffen, gleichzeitig aber die Grenzen aktueller Modelle beim Unterscheiden korrekter Beweise von verschiedenen eingefügten Fehlern aufzeigt.
Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen
Stellen Sie sich vor, Sie lehren einen Roboter, mathematische Probleme zu lösen. Um den Roboter zum Lernen zu bringen, müssen Sie ihm mitteilen, wann er recht hat und wann er unrecht hat.
Lange Zeit war der Standardweg, diese Roboter (sogenannte „neuronale Theorembeweiser") zu unterrichten, ein einfaches Ampelsystem:
- Grüne Ampel: Der Beweis ist perfekt.
- Rote Ampel: Der Beweis ist falsch.
Dies funktioniert gut, weil die „Ampel" tatsächlich ein Computerprogramm ist, das die Mathematik mit 100-prozentiger Genauigkeit überprüft. Doch es gibt ein großes Problem: Es ist zu spärlich. Wenn der Roboter 99 % eines schwierigen Problems löst, aber am ganz Ende einen winzigen Fehler macht, erhält er eine Rote Ampel. Er bekommt keine Anerkennung für die 99 %, die er richtig hatte. Es ist wie bei einem Schüler, der eine „Fünf" auf einem Test bekommt, weil er eine Frage verpasst hat, ohne Rückmeldung zum Rest der Arbeit. Der Roboter gerät in Verwirrung und weiß nicht, wie er sich verbessern soll.
Um dies zu beheben, wollen Forscher dem Roboter ein Belohnungsmodell beibringen. Stellen Sie sich dies als einen menschlichen Lehrer vor, der einen Beweis ansehen und sagen kann: „Hier hast du großartig gearbeitet, aber dort hast du einen Fehler gemacht", und eine Punktzahl von 0 bis 100 vergibt, anstatt nur Bestanden/Nicht bestanden.
Das Problem: Wie wissen Sie, ob Ihr „menschlicher Lehrer" (das Belohnungsmodell) tatsächlich gut im Benoten ist?
Normalerweise müssen Sie, um einen Lehrer zu testen, ihn in ein Klassenzimmer setzen und wochenlang beobachten, wie er unterrichtet, um zu sehen, ob sich die Schüler verbessern. Dies ist teuer und langsam.
Die Lösung: FormalRewardBench
Die Autoren dieses Papiers haben eine standardisierte Benotungsprüfung speziell für diese „Lehrer"-Roboter entwickelt. Sie nennen sie FormalRewardBench.
So haben sie die Prüfung aufgebaut:
- Das Ausgangsmaterial: Sie nahmen 250 echte, schwierige mathematische Probleme (aus Wettbewerben wie der Internationalen Mathematik-Olympiade), die in eine strenge Computersprache namens Lean 4 übersetzt wurden.
- Die Falle: Für jeden korrekten Beweis verwendeten sie eine superintelligente KI, um fünf verschiedene Arten von gefälschten, falschen Beweisen zu generieren. Dies waren nicht nur offensichtliche Tippfehler; es waren clevere Fallen, die einen Roboter täuschen sollten.
- Der „Chirurgische Schlag": Das Ändern nur eines winzigen Buchstabens oder einer Zahl, der die Logik zerstört.
- Der „Glatter Redner": Das Hinzufügen langer, selbstbewusst klingender Erklärungen, die richtig klingen, aber tatsächlich falsch sind.
- Der „Betrüger": Das Schreiben der Lösung in Python-Code (der für Computer funktioniert) anstatt in der erforderlichen Mathematiksprache (Lean).
- Der „Verwirrte Schüler": Die Verwendung der richtigen Werkzeuge, aber deren Anwendung auf falsche Annahmen.
- Der „Wortreiche Unsinn": Das Schreiben eines Beweises, der unglaublich lang und kompliziert ist, aber fundamental fehlerhaft.
Der Test:
Sie nahmen verschiedene KI-Modelle und baten sie, ein Paar von Beweisen (einen echten, einen gefälschten) zu betrachten und den korrekten auszuwählen. Sie testeten vier Arten von „Richtern":
- Die Super-Genies (Frontier-LLMs): Massive, allgemein verwendete KI-Modelle (wie Claude Opus oder GPT-5).
- Die professionellen Benotenden (Judge LLMs): Modelle, die speziell darauf trainiert wurden, die bessere Antwort auszuwählen.
- Die Mathe-Genies (allgemeine LLMs): Modelle, die stark auf Mathematik und Code trainiert wurden.
- Die Beweisspezialisten (Theorembeweiser): Modelle, die speziell entwickelt wurden, um mathematische Beweise zu generieren.
Die schockierenden Ergebnisse:
Das Papier fand eine überraschende Wendung in der Geschichte:
- Die Spezialisten scheiterten: Die Modelle, die am besten darin sind, Beweise zu schreiben (die Beweisspezialisten), waren tatsächlich die schlechtesten darin, sie zu bewerten. Sie erzielten etwa 24 % (kaum besser als Raten). Es stellt sich heraus, dass man nicht weiß, wie man ein Haus auf Risse untersucht, nur weil man weiß, wie man eines baut.
- Die Generalisten gewannen: Die „Super-Genies" (allgemeine KI-Modelle) waren am besten darin, die gefälschten Beweise zu erkennen, mit fast 60 %.
- Die „Glatter Redner"-Falle: Viele Modelle ließen sich leicht von den „wortreichen Unsinn"- oder „glatten Redner"-Beweisen täuschen. Sie mochten die langen Erklärungen, selbst wenn die Mathematik falsch war.
Das Fazit:
Das Papier kommt zu dem Schluss, dass die Fähigkeit, einen Beweis zu erstellen, einen nicht automatisch gut darin macht, einen zu bewerten. Um bessere KI zu entwickeln, die Mathematikern helfen kann, müssen wir Modelle speziell darauf trainieren, „Kritiker" oder „Richter" zu sein, nicht nur „Schöpfer".
Die Autoren haben diese Prüfung (FormalRewardBench) der Öffentlichkeit zugänglich gemacht, damit andere Forscher ihre eigenen „Lehrer"-Roboter testen und sehen können, ob sie tatsächlich besser darin werden, Fehler zu erkennen.
Ertrinken Sie in Arbeiten in Ihrem Fachgebiet?
Erhalten Sie tägliche Digests der neuesten Arbeiten passend zu Ihren Forschungsbegriffen — mit technischen Zusammenfassungen, in Ihrer Sprache.