💻 computer science

Benchmarking Testing in Automated Theorem Proving

Dieser Beitrag stellt „T" vor, ein neuartiges Framework, das die semantische Korrektheit von KI-generierten formalen Theoremen überprüft, indem es verifiziert, ob abhängige Folgetheoreme erfolgreich kompilieren, und dabei eine erhebliche Lücke in den Theoremgenerierungsfähigkeiten aktueller großer Sprachmodelle im Vergleich zu traditionellen lexikalischen oder manuellen Evaluierungsmethoden aufzeigt.

Ursprüngliche Autoren: Jongyoon Kim, Hojae Han, Seung-won Hwang

Veröffentlicht 2026-04-28

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Jongyoon Kim, Hojae Han, Seung-won Hwang

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 stellen ein Team von Architekten ein, um eine neue Brücke zu entwerfen.

Der alte Weg des Testens (Kompilierung)
In der Vergangenheit haben wir bei der Bewertung dieser Architekten (die in diesem Papier als KI-Modelle bezeichnet werden) nur geprüft, ob ihre Baupläne „grammatikalisch korrekt" waren. Wir fragten: Folgt der Bauplan den Regeln der Grammatik? Verbinden sich die Linien? Sagt der Computer „Syntax OK"?

Wenn der Bauplan auf dem Papier perfekt aussah, gingen wir davon aus, dass die Brücke standhalten würde. Doch hier liegt das Problem: Ein Architekt könnte einen Bauplan entwerfen, der besagt: „Diese Brücke besteht aus massivem Gold", und der Computer würde sagen: „Syntax OK!", weil der Satz grammatikalisch korrekt ist. Wenn der Bauplan jedoch eigentlich für eine „Stahlhängebrücke" gedacht war, hat der Architekt die eigentliche Aufgabe verfehlt, auch wenn die Grammatik perfekt war.

In der Welt der Mathematik und des Computercodes nennt man dies Kompilierung. Die KI schreibt ein Theorem (eine mathematische Aussage), und der Computer prüft, ob es kompiliert (ohne Fehler ausgeführt wird). Das Papier argumentiert, dass dies eine schreckliche Methode ist, um zu beurteilen, ob die KI die Mathematik tatsächlich verstanden hat.

Der neue Weg des Testens (T2-Rahmenwerk)
Die Autoren dieses Papiers schlagen eine neue Methode vor, die T2 (Theorem Testing) genannt wird. Anstatt nur die Grammatik des Bauplans zu prüfen, fragen sie: Funktioniert dieser Bauplan tatsächlich, wenn wir versuchen, den Rest der Stadt darum herum zu bauen?

Sie verwenden ein Konzept namens Integrationstest. Stellen Sie sich vor, die Brücke ist nur ein Teil einer riesigen Stadt.

Das Ziel: Die KI wird aufgefordert, ein spezifisches Theorem zu beweisen (z. B. „Die Addition ist kommutativ", was bedeutet $a + b = b + a$ ).
Die Nachfolger: In der echten Mathematik verwenden andere Mathematiker, sobald ein kleines Faktum bewiesen ist, dieses Faktum, um größere, komplexere Dinge zu beweisen. Das Papier untersucht alle anderen Theoreme, die von der Antwort der KI abhängen.
Der Test: Die Antwort der KI wird in diese „nachgelagerten" Beweise eingefügt.
- Wenn die KI eine „gefälschte" Antwort gab (wie eine Tautologie, die immer wahr ist, aber nichts Nützliches aussagt), werden die nachgelagerten Beweise abstürzen. Sie werden nicht kompilieren können, weil sie sich auf eine spezifische Bedeutung verlassen haben, die die KI nicht geliefert hat.
- Wenn die KI die korrekte Antwort gab, laufen die nachgelagerten Beweise reibungslos.

Die große Entdeckung
Die Autoren haben eine massive Testsuite mit 2.206 realen mathematischen Problemen aus der Programmiersprache „Lean" erstellt. Sie testeten 18 der intelligentesten verfügbaren KI-Modelle (darunter Modelle von Google, OpenAI und Anthropic).

Hier ist das, was sie fanden, unter Verwendung unserer Brücken-Analogie:

Die „Grammatik"-Falle: Die meisten KIs waren hervorragend darin, den alten Test zu bestehen. Sie schrieben Baupläne, die perfekt aussahen und ohne Fehler kompilierten. Beim alten Test erzielten sie etwa 80 % Erfolg.
Der Realitätscheck: Als die Autoren den neuen „Stadt-Integrations"-Test anwendeten, sanken die Ergebnisse drastisch. Das beste KI-Modell erreichte nur etwa 39 % richtige Antworten.
Die Kluft: Das bedeutet, dass von jedem 100 Brücken, die die KI zu bauen behauptete, etwa 60 sofort einstürzen würden, sobald jemand versucht, eine Straße darauf zu bauen. Die KI war gut darin, das Aussehen der Mathematik zu imitieren, aber schlecht im Sinn.

Warum das wichtig ist
Das Papier zeigt, dass die aktuellen Methoden zur Messung mathematischer Fähigkeiten von KI uns belügen.

Lexikalische Ähnlichkeit (BLEU): Zu prüfen, ob die Wörter der KI menschlichen Wörtern ähneln, ist nutzlos. Die KI kann Unsinn schreiben, der wie Mathematik aussieht, und trotzdem bestehen.
Spezialisierte Modelle: Selbst Modelle, die speziell dafür trainiert wurden, „Mathematik-Experten" zu sein, schnitten nicht viel besser ab als allgemeine Chatbots. Sie wurden nur besser darin, die Syntax zu imitieren.
Die Lösung: Der einzige Weg, um zu wissen, ob eine KI Mathematik wirklich versteht, besteht darin, zu sehen, ob ihre Arbeit standhält, wenn andere Beweise versuchen, darauf aufzubauen.

Kurz gesagt
Das Papier führt einen neuen „Stresstest" für KI-Mathematik ein. Es hört auf zu fragen: „Sieht dieser Satz wie Mathematik aus?" und beginnt zu fragen: „Funktioniert diese Mathematik tatsächlich, wenn wir versuchen, sie zur Lösung größerer Probleme einzusetzen?" Das Ergebnis ist ein harter Realitätscheck: Die besten KI-Modelle von heute haben immer noch Schwierigkeiten, echte, sinnvolle Mathematik zu leisten, auch wenn sie so aussehen, als würden sie es perfekt tun.

1. Problemstellung

Der rasche Fortschritt bei Large Language Models (LLMs) hat ihre Fähigkeit verbessert, formale Beweise in Systemen wie Lean zu generieren. Allerdings leiden die aktuellen Evaluierungsmethoden an einem kritischen Mangel: sie verwechseln syntaktische Gültigkeit mit semantischer Korrektheit.

Die Einschränkung der Kompilierung: Bestehende Benchmarks (z. B. MiniF2F, ProofNet) bewerten Modelle primär, indem sie prüfen, ob ein generierter Theorem kompiliert. Während die Kompilierung bestätigt, dass der Code syntaktisch gültig und isoliert logisch konsistent ist, garantiert sie nicht, dass der Theorem die beabsichtigte mathematische Bedeutung erfasst.
Das „Tautologie"-Problem: Ein Modell kann eine triviale Tautologie generieren (z. B. $a + b = a + b$ ), die erfolgreich kompiliert, aber versagt, die beabsichtigte nicht-triviale Aussage zu beweisen (z. B. Kommutativität $a + b = b + a$ ).
Unzulänglichkeit von Proxies: Bestehende Versuche, semantische Korrektheit zu messen, verlassen sich auf unzuverlässige Proxies wie lexikalische Überlappung (BLEU-Scores) gegenüber menschlich annotierten Referenzen oder manuelle Inspektion. Diese Methoden sind entweder verrauscht, erfordern teuren menschlichen Aufwand oder scheitern daran, zwischen korrekten und inkorrekten semantischen Bedeutungen zu unterscheiden.

2. Methodik

Die Autoren schlagen einen Paradigmenwechsel vor, der von Integrationstests in der Softwareentwicklung inspiriert ist. Anstatt einen Theorem isoliert zu bewerten, bewerten sie ihn basierend darauf, wie er mit dem Rest der Codebasis interagiert.

Kernkonzept: Theorem-Testing (T2)

In Anlehnung an die Curry-Howard-Korrespondenz (wo Beweise Programmen entsprechen) behandeln die Autoren einen generierten Theorem als Funktion und die Theoreme, die von ihm abhängen, als „Testfälle".

Abhängigkeitsgraph: Sie konstruieren einen Abhängigkeitsgraphen, bei dem ein Ziel-Theorem ( $t_{GT}$ ) Vorgänger (Definitionen/Lemmas, die es verwendet) und Nachfolger (Theoreme, die es aufrufen oder darauf aufbauen) hat.
Logik der Integrationstests: Wenn ein generierter Theorem ( $t_{fl}$ ) semantisch inkorrekt ist (z. B. definiert er eine Tautologie anstelle der beabsichtigten Eigenschaft), wird jeder Nachfolger-Theorem, der darauf angewiesen ist, beim Kompilieren fehlschlagen.
Analogen zur Schnittstellenelimination: Der Prozess ist formal im logischen Prinzip der Schnittstellenelimination (Cut Elimination) begründet. Wenn eine Beweiskette ( $X \to Y \to Z \to W$ ) fehlschlägt, wenn das Zwischenlemma ( $Y$ ) durch einen generierten Kandidaten ersetzt wird, ist der Kandidat semantisch inkorrekt.

Der T2-Benchmark

Die Autoren haben einen groß angelegten Benchmark, T2, konstruiert, um diese Evaluierung zu ermöglichen:

Quelle: Extrahiert aus 5 realen Lean 4-Repositorys (abdeckend Algebra, Topologie, Zahlentheorie usw.).
Skala: 2.206 Probleme, jedes gepaart mit durchschnittlich 41 Nachfolger-Theoremen.
Schwerer Teilmenge: Eine Teilmenge von 389 „Hard"-Problemen, bei denen das Modell sowohl die Proposition (Aussage) als auch den Beweis generieren muss, anstatt nur einen Beweis für eine gegebene Aussage einzufügen.
Automatisierung: Die Extraktionspipeline ist vollständig automatisiert und erfordert keine menschliche Annotation für die Abhängigkeitsstruktur. Natürlichsprachliche (NL) Beschreibungen wurden von einem starken LLM (Claude Sonnet 4.5) generiert und für eine Stichprobe manuell verifiziert.

Die Metrik: Testgenauigkeit (Testing Accuracy, TA)

Das Paper führt Testgenauigkeit (TA) als primäre Evaluierungsmetrik ein:
$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$
Ein generierter Theorem besteht nur, wenn alle seine abhängigen Nachfolger-Theoreme erfolgreich kompilieren, wenn der ursprüngliche Theorem durch den generierten ersetzt wird.

3. Hauptbeiträge

T2-Benchmark: Der erste groß angelegte, abhängigkeitsreiche Benchmark für formale Theorembeweise, der über isolierte Probleme hinausgeht und reale Repository-Kontexte einbezieht.
Testgenauigkeit (TA): Eine neuartige, automatische, referenzfreie Metrik, die semantische Korrektheit direkt durch Kompilierung abhängiger Module verifiziert.
Empirische Lückenanalyse: Umfassende Evaluierung von 18 State-of-the-Art-Modellen (sowohl Open-Source als auch Closed-Source), die eine massive Diskrepanz zwischen Kompilierungserfolg und semantischer Korrektheit aufzeigt.
Kontextuelle Erkenntnisse: Es wurde gezeigt, dass die Bereitstellung von Nachfolger-Theoremen als Kontext die semantische Korrektheit signifikant verbessert, während die Bereitstellung von nur natürlichen Sprachbeweisen dies nicht tut.

4. Experimentelle Ergebnisse

Die Autoren evaluierten 18 Modelle (einschließlich GPT-5, Claude-Sonnet-4.5, Llama-3.1 und spezialisierter Mathematik-Modelle wie DeepSeek-Prover) auf dem T2-Benchmark.

Die semantische Lücke:
- Kompilierungsgenauigkeit: Modelle erreichten hohe Kompilierungsraten (z. B. Claude-Sonnet-4.5: 80,3 % auf dem gesamten Set).
- Testgenauigkeit (TA): Dieselben Modelle erzielten drastisch niedrigere TA-Werte (z. B. Claude-Sonnet-4.5: 38,9 % auf dem gesamten Set; 4,5 % auf dem Hard-Set).
- Falsch-Positive: Bis zu 93,1 % der kompilierbaren Theoreme erwiesen sich als semantisch inkorrekt, wenn sie gegen Nachfolger getestet wurden.
Versagen bestehender Metriken:
- BLEU: Hohe lexikalische Ähnlichkeit (BLEU-Scores) zeigte fast keine Korrelation mit semantischer Korrektheit (Korrelation: 0,123). Modelle konnten textlich ähnliche, aber logisch falsche Beweise generieren.
- Spezialisierte Modelle: Modelle, die speziell für Theorembeweise feinabgestimmt wurden, erreichten oft höhere Kompilierungsraten, schnitten bei TA jedoch schlechter oder ähnlich ab wie allgemeine Modelle, was darauf hindeutet, dass sie sich eher an Syntax als an Semantik anpassen (Overfitting).
Auswirkung des Kontexts:
- Die Bereitstellung von Nachfolger-Theoremen als Eingabekontext verbesserte die TA konsistent (z. B. +4,9 % für Claude-Sonnet-4.5).
- Die Bereitstellung von NL-Beweisen allein ohne Nachfolger verbesserte die Leistung nicht und verschlechterte sie manchmal.
- Few-Shot-Prompting und iterative Verfeinerung (unter Verwendung von Compiler-Rückmeldungen) erzielten auf dem Hard-Set vernachlässigbare Verbesserungen, was darauf hindeutet, dass die Schwierigkeit in der tiefen semantischen Reasoning liegt und nicht nur im Aufgabenformat.

5. Bedeutung und Fazit

Dieses Paper stellt den aktuellen Stand der Evaluierung von Automatisierten Theorembeweisen (ATP) grundlegend in Frage.

Neudefinition von Erfolg: Es beweist, dass „Kompilierung" eine notwendige, aber unzureichende Bedingung für die Theoremgenerierung ist. Ein Modell kann syntaktisch perfekt, aber semantisch nutzlos sein.
Vertrauenswürdigkeit: Der T2-Benchmark und die TA-Metrik bieten eine rigorose, automatische Möglichkeit zu bewerten, ob ein LLM mathematische Konzepte wirklich versteht oder lediglich syntaktisch gültigen Code halluziniert.
Zukunftsrichtung: Die Arbeit legt nahe, dass zukünftige ATP-Systeme hinsichtlich ihrer Fähigkeit bewertet werden müssen, sich in bestehende Codebasen zu integrieren (abhängigkeitsbewusste Generierung), anstatt isolierte Rätsel zu lösen. Sie hebt zudem hervor, dass die Bereitstellung des „Test-Sets" (Nachfolger-Theoreme) an das Modell während der Generierung eine entscheidende Strategie zur Verbesserung der semantischen Ausrichtung ist.

Zusammenfassend argumentiert das Paper, dass Integrationstests das fehlende Glied bei der Evaluierung von LLMs für formale Mathematik sind und offenbaren, dass aktuelle State-of-the-Art-Modelle weit davon entfernt sind, eine zuverlässige semantische Korrektheit im Theorembeweis zu erreichen.