Wie weit ist das große Sprachmodell noch von einem "Mathematikbeweis-Experten" entfernt? Teams von Stanford, Berkeley und MIT haben den Bewertungsstandard IneqMath vorgeschlagen.

Viele große Sprachmodelle (LLM) geben häufig scheinbar korrekte Ergebnisse, aber sobald man sich den Lösungsweg ansieht, möchte man den Kopf schütteln. Verstehen diese Modelle wirklich den logischen Schlussfolgerungsprozess? Oder raten sie einfach, weil es so aussieht, als wäre es richtig?

Ungleichungsaufgaben sind ideale Gegenstände, um zu prüfen, ob ein Modell tatsächlich beweisen kann - sie haben eine einfache Struktur, einen klaren logischen Aufbau und lassen schnell Lücken im Schlussfolgerungsprozess erkennen. Man kann sagen, dass sie wie ein "Geisterspiegel" für die mathematische Schlussfolgerungsfähigkeit von KI sind.

Die zentrale Herausforderung bei der Untersuchung dieses Problems ist eigentlich das, woran die formale Mathematik arbeitet: die Überprüfung der Strenge des Schlussfolgerungsprozesses. Formale Systeme wie Lean und Coq können die Richtigkeit eines Beweises fehlerfrei überprüfen. Aber sie setzen hohe logische Anforderungen, jede Schritt muss korrekt geschrieben werden, damit der Computer ihn überprüfen kann. Diese Systeme haben eine hohe Einstiegshürde und eine geringe Automatisierung. Es ist mühsam, damit zu arbeiten, und bei olympiadeähnlichen Ungleichungsaufgaben ist es schwierig, eine Massenverarbeitung zu realisieren.

Beispielbild für die Verwendung der Lean - Sprache zur mathematischen Beweisführung

Andererseits werden große Sprachmodelle mit einer großen Menge natürlicher Sprache trainiert. Obwohl ihre Fähigkeit, direkt maschinenverifizierbare formale Beweise zu generieren, nicht besonders stark ist, zeigen sie in der "informellen Schlussfolgerung" gute Ergebnisse. Natürliche Sprache entspricht dem menschlichen Denkmodell, hat eine niedrige Einstiegshürde und ist einfach zu verarbeiten. Daher ist die Erforschung der Fähigkeit von großen Sprachmodellen, Ungleichungen in einer natürlichen Sprachumgebung zu beweisen, ein interessantes und wertvolles Forschungsgebiet.

Deshalb haben die Forschungsgruppen von Stanford, Berkeley und MIT einen neuen Ansatz vorgeschlagen: Die Ungleichungsbeweise werden in zwei kleine, in informeller natürlicher Sprache geschriebene, aber verifizierbare Aufgaben aufgeteilt - "Bound Estimation" (Schrankenschätzung) und "Relation Prediction" (Beziehungsvorhersage). Innerhalb dieses Rahmens haben sie auch einen neuen Benchmark - Datensatz namens IneqMath erstellt. Er ist wie eine "Zwischenbrücke" zwischen natürlicher Sprache und formaler Logik, mit der man Schritt für Schritt den Schlussfolgerungsprozess des Modells in einer natürlichen Sprachumgebung überprüfen kann und entscheiden kann, ob es wirklich "logisch argumentiert" oder nur rät.

Projekt - Homepage: https://ineqmath.github.io

Paper: https://arxiv.org/abs/2506.07927

Code - Repository: https://github.com/lupantech/ineqmath

Datensatz: https://huggingface.co/datasets/AI4Math/IneqMath

Rangliste: https://huggingface.co/spaces/AI4Math/IneqMath - Leaderboard

Wie bewertet diese "informelle" Methode einen Beweis?

Einfach ausgedrückt, teilen sie eine Ungleichungsaufgabe in zwei kleine Aufgaben auf: Bound Estimation (Schrankenschätzung) und Relation Prediction (Beziehungsvorhersage). Beispielsweise für ein Beweisproblem:

Für beliebige reelle Zahlen a und b, beweisen Sie, dass a² + b² ≥ 2ab gilt. Dies kann in die folgenden beiden Aufgaben umgewandelt werden:

Bound Estimation (Schrankenschätzung)

Für beliebige reelle Zahlen a und b, entscheiden Sie über die Beziehung zwischen den beiden Ausdrücken: a² + b²? 2ab

Relation Prediction (Beziehungsvorhersage)

Für beliebige reelle Zahlen a und b, finden Sie die größte Konstante C, sodass a² + b² ≥ Cab immer gilt.

Diese beiden Arten von Aufgaben können direkt in natürlicher Sprache + LaTeX ausgedrückt werden. Große Modelle können die Aufgaben schrittweise lösen, was sowohl die Beweisbarkeit der mathematischen Aufgaben bewahrt als auch nicht zu kompliziert ist. Gleichzeitig ist die Lösung eindeutig und die Überprüfung einfach.

IneqMath: Der erste "in natürlicher Sprache, aber verifizierbarer" Ungleichungsdatensatz

Die Forschungsgruppe hat auf der Grundlage der oben genannten Aufgabenstruktur den Datensatz IneqMath erstellt. Der Datensatz enthält 1.252 Ungleichungsaufgaben als Trainingsmenge, wobei jede Aufgabe mit einem detaillierten Lösungsweg und Anmerkungen zu den relevanten Sätzen versehen ist. Gleichzeitig enthält der Datensatz 200 Testaufgaben, die von internationalen Mathematikolympiade - Goldmedaillisten markiert wurden, sowie 100 Validierungsaufgaben.

Hier sind Beispiele für Trainings - und Testaufgaben aus IneqMath:

Wie kann man beurteilen, ob die Schlussfolgerung eines Modells zuverlässig ist?

Die Forschungsgruppe hat speziell ein "KI - mathematisches Richtersystem" entwickelt. Obwohl der Name nicht besonders aufregend ist, ist es sehr praktisch - es kann nicht nur feststellen, ob die endgültige Lösung richtig ist, sondern auch aus vier verschiedenen Perspektiven automatisch beurteilen, ob jeder Schritt der Schlussfolgerung des Modells logisch ist, um zu vermeiden, dass man nur aufgrund der endgültigen Lösung getäuscht wird. Hier sind die vier Prüfer, die die Strenge des Prozesses aus verschiedenen Perspektiven beurteilen:

• Toy Case Judge: Prüft, ob aus speziellen Werten auf allgemeine Ergebnisse geschlossen wird, ohne den Verallgemeinerungsprozess zu berücksichtigen.
• Logical Gap Judge: Prüft, ob es logische Lücken wie fehlende Schritte oder unerkärte äquivalente Umformungen gibt.
• Numerical Approximation Judge: Prüft, ob es unangemessene Näherungen gibt.
• Numerical Computation Judge: Prüft, ob die Berechnungen richtig sind, einschließlich numerischer Fehler bei elementaren algebraischen Operationen oder beim Einsetzen von Werten.

Mit einer Genauigkeit von F1 = 0,93 können die Menschen schon aussteigen?

Dieses System ist nicht nur "kritikfreudig", sondern auch sehr genau. Die Forschungsgruppe hat einen Vergleich mit manuell markierten Ergebnissen durchgeführt und festgestellt, dass die Übereinstimmung zwischen diesen automatischen Prüfern und menschlichen Experten bei der Beurteilung der Strenge sehr hoch ist, mit einem F1 - Wert von 0,93! Einfach ausgedrückt, kann es jetzt sehr zuverlässig die Arbeit vieler manueller Korrekturen ersetzen.

Einige wichtige Erkenntnisse

"Richtige Lösung" ≠ "Richtiger Schlussfolgerungsprozess"

Oft können große Sprachmodelle die richtige Lösung geben, aber der Schlussfolgerungsprozess hält der Prüfung nicht stand. Nehmen wir Grok 3 mini als Beispiel. In den Tests war die Lösung in 71,5 % der Fälle richtig. Klingt beeindruckend? Aber hier ist das Problem: Als die Forschungsgruppe ihr automatisches Prüfungssystem anwandte, waren nur noch 6 % der Lösungen "logisch und streng begründet". Und dieses Problem ist nicht nur bei Grok zu finden, fast alle Modelle haben ähnliche Probleme, und die "Genauigkeit" sinkt um bis zu 65,5 %. Dies zeigt, dass viele Modelle zwar die Lösung "raten" können, aber der Schlussfolgerungsprozess entweder Schritte überspringt, auf spezielle Werte setzt oder einfach nur vage Erklärungen gibt.

Ist ein größeres Modell besser in der Schlussfolgerung? Nicht unbedingt!

Man denkt immer, dass ein größeres Modell "intelligenter" ist. In gewissem Sinne stimmt das - Studien haben gezeigt, dass größere Modelle besser darin sind, die Lösung zu "raten". Bei verschiedenen mathematischen Aufgaben steigt die Genauigkeit der Lösung in der Regel mit der Anzahl der Parameter. Aber wenn wir nicht nur die Lösung betrachten, sondern auch die Strenge des Schlussfolgerungsprozesses evaluieren, hört dieser "Steigerungstrend" auf.

Deshalb ist der Weg, die Parameter zu erhöhen und die Hardware zu verbessern, um die Strenge der Schlussfolgerung zu verbessern, nicht erfolgreich. Logik und Strenge wachsen nicht automatisch mit der Größe des Modells.

Mehr Denken bedeutet nicht zwangsläufig bessere Ergebnisse

Was ist, wenn wir eine andere Strategie wählen: Lassen wir das Modell "länger nachdenken", wird das Ergebnis besser? D.h., lassen wir es mehr Token verwenden und einen längeren Schlussfolgerungsprozess schreiben, um langsam und gründlich zu analysieren. Ist das zuverlässiger?

Das Ergebnis zeigt... nicht wirklich.

Die Forschungsgruppe hat versucht, die Beschränkungen zu lockern und das Modell dazu zu bringen, mehr Inhalte zu generieren. Obwohl die Strenge der Schlussfolgerung etwas verbessert wurde, trat schnell ein "Flaschenhals" auf - egal wie viele Token man dem Modell gibt, die Verbesserung ist begrenzt. Die Länge der Schlussfolgerung nimmt zu, aber die Qualität steigt nicht synchron.

Genau wie bei einem Schüler in der Prüfung: Wenn er die Aufgabe nicht kann, bringt es ihm nichts, nur Unsinn zu schreiben. Der Schlüssel liegt darin, auf den Punkt zu kommen. Das Gleiche gilt für große Modelle: "Mehr denken" bedeutet nicht "klarer denken".

Zwei effektive Methoden

Obwohl große Modelle noch nicht so gut in der Beweisführung sind, hat die Forschungsgruppe zwei effektive Methoden gefunden:

Self - Critique (Selbstkritik)

Lassen Sie das Modell zunächst seine eigene Lösung prüfen und dann korrigieren. Genau wie ein Schüler, der seine Hausaufgaben kontrolliert, hat diese Methode die Genauigkeit von Gemini 2.5 Pro um etwa 5 % verbessert.

Theorem as Hints (Sätze als Tipps)

Gegeben Sie dem Modell relevante Sätze im Voraus, ähnlich wie man einem Schüler vor der Prüfung die Schwerpunkte nennt. Das Ergebnis ist, dass die Genauigkeit um bis zu 10 % verbessert wird, was besonders bei komplexen Aufgaben hilfreich ist.

Dies zeigt, dass es nicht nur um Rechenleistung geht. Es ist wichtig, das Modell dazu zu bringen, "selbstkritisch" zu sein und "Werkzeuge" zu nutzen, um wirklich "klüger" zu werden.

Schlusswort

Aktuelle große Modelle können raten, aber noch nicht so gut streng schlussfolgern. IneqMath soll nicht beweisen, dass die Modelle nicht funktionieren, sondern ihnen helfen, Schritt für Schritt zu lernen, wie man schlussfolgert und wie man ein mathematisches KI - System wird, das wirklich "beweisen" kann.

Vielleicht können sie heute noch nur gut raten, aber in Zukunft könnten sie