Learning to Disprove: Formal Counterexample Generation with Large Language Models

Diese Arbeit schließt die Lücke in der KI-gestützten mathematischen Beweissuche, indem sie große Sprachmodelle durch eine symbolische Mutationsstrategie und ein Multi-Belohnungs-Expert-Iteration-Framework darauf trainiert, formal verifizierte Gegenbeispiele in Lean 4 zu generieren.

Das Wesentliche

Stellen Sie sich vor, Sie sind ein genialer Mathematik-Lehrer, der versucht, einen sehr klugen, aber noch etwas unerfahrenen Schüler (eine Künstliche Intelligenz) zu unterrichten.

Bisher haben sich die KI-Forscher fast ausschließlich darauf konzentriert, diesem Schüler beizubringen, wie man Beweise führt – also wie man sagt: "Ja, diese Aussage ist wahr, und hier ist der Weg, warum." Das ist wie das Bauen eines perfekten Hauses.

Aber in der Mathematik gibt es eine ebenso wichtige Fähigkeit: Das Zerstören von falschen Aussagen. Wenn jemand behauptet: "Alle Schwäne sind weiß", reicht es nicht, 100 weiße Schwäne zu zählen. Man muss einen schwarzen Schwan finden, um die Aussage zu widerlegen. Das Finden dieses einen schwarzen Schwans nennt man ein Gegenbeispiel.

Bisher war die KI darin ziemlich schlecht. Sie konnte viele Häuser bauen, aber kaum einen schwarzen Schwan finden.

Diese neue Arbeit ("Learning to Disprove") ändert das. Hier ist die Erklärung, wie sie das gemacht haben, mit ein paar einfachen Analogien:

1. Das Problem: Der leere Kühlschrank und der spärliche Lohn

Es gab zwei große Hindernisse, warum die KI das nicht gut konnte:

• Keine Übungsaufgaben: Es gab kaum Beispiele dafür, wie man Gegenbeispiele findet. Es war, als würde man einem Schüler einen leeren Kühlschrank geben und erwarten, dass er kocht.
• Kein Feedback: Wenn die KI versuchte, ein Gegenbeispiel zu finden und scheiterte, bekam sie kein Feedback. Es war wie ein Spiel, bei dem man nur gewinnt, wenn man sofort den Jackpot trifft. Wenn man daneben liegt, passiert gar nichts. Das macht es schwer, daraus zu lernen.

2. Die Lösung: Der "Mutations-Generator" (Der kreative Koch)

Um das Problem mit den fehlenden Übungen zu lösen, haben die Forscher einen cleveren Trick angewendet. Sie haben nicht einfach gewartet, bis jemand ein Gegenbeispiel fand. Stattdessen haben sie einen automatischen Generator gebaut.

Stellen Sie sich vor, Sie haben eine perfekte, bewiesene mathematische Regel (z. B. "Wenn es regnet, wird der Boden nass").
Der Generator nimmt diese Regel und nimmt einen wichtigen Teil davon weg (z. B. "Wenn es regnet...").
Jetzt ist die Regel falsch! Der Boden könnte trocken bleiben, wenn es nicht regnet.
Der Generator sagt dann zur KI: "Hey, hier ist eine falsche Regel. Finde mir ein konkretes Beispiel, das zeigt, warum sie falsch ist!"

Durch diesen Prozess haben sie aus wenigen bestehenden Regeln 575.000 neue Übungen geschaffen. Plötzlich hatte der Schüler einen riesigen Übungsheft voller Aufgaben, wie man falsche Aussagen entlarvt.

3. Der "Doppel-Lösegeld"-Trick (Das Belohnungssystem)

Aber wie lernt die KI, wenn sie oft scheitert? Hier kommt der zweite Teil des Tricks ins Spiel: Die Multi-Belohnung.

Stellen Sie sich vor, die KI versucht, einen schwarzen Schwan zu finden.

• Früher: Wenn sie keinen schwarzen Schwan fand, bekam sie 0 Punkte. Punkt. Ende.
• Jetzt: Die Forscher haben das Spiel cleverer gemacht.
  1. Die KI muss nicht nur den schwarzen Schwan finden (das ist schwer).
  2. Sie muss auch beweisen, dass der ursprüngliche Teil der Regel (den wir entfernt haben) in diesem Fall nicht gilt.

Das ist wie bei einem Detektiv: Wenn er den Täter nicht sofort findet, bekommt er trotzdem einen kleinen Punkt dafür, wenn er beweisen kann, dass der Verdächtige nicht am Tatort war.
Dieser "kleine Punkt" (die Belohnung) hilft der KI, auch dann weiterzulernen, wenn sie das große Ziel noch nicht erreicht hat. Sie lernt Schritt für Schritt, statt frustriert aufzugeben.

4. Der Zwei-Phasen-Prozess: Erst raten, dann beweisen

Die KI wurde in zwei Schritten trainiert:

1. Der Träumer (Informelles Denken): Die KI denkt sich eine Idee aus. "Vielleicht ist dieser Schwan schwarz, weil er in einem dunklen Wald lebt." Sie muss keine perfekte Formel haben, nur eine plausible Idee.
2. Der Richter (Formaler Beweis): Sobald die Idee da ist, muss die KI diese Idee in eine strenge, mathematische Sprache (Lean 4) übersetzen, die ein Computer-Prüfer automatisch überprüfen kann.

Das ist wie beim Schreiben eines Romans: Zuerst schreibt man eine grobe Skizze (die Idee), und dann muss man sie so perfekt formulieren, dass ein strenger Lektor (der Computer) sie akzeptiert.

Das Ergebnis

Das Ergebnis ist ein KI-Modell, das nicht nur gut darin ist, Dinge zu beweisen, sondern auch darin, falsche Dinge zu entlarven.

• Es ist wie ein Schüler, der nicht nur Hausaufgaben macht, sondern auch lernt, Fehler in den Aufgaben des Lehrers zu finden.
• In Tests hat dieses neue Modell deutlich besser abgeschnitten als alle bisherigen Modelle. Es hat die Fähigkeit, logisch zu denken, indem es lernt, sich selbst zu hinterfragen und Fehler zu finden.

Zusammenfassend: Die Forscher haben der KI einen riesigen Vorrat an "falschen Regeln" gegeben, um sie zu üben, und ein Belohnungssystem entwickelt, das sie auch für kleine Erfolge lobt. So wurde aus einem KI-Modell, das nur bauen konnte, eines, das auch gut darin ist, zu zerstören – und damit die Mathematik sicherer zu machen.

Technische Zusammenfassung

1. Problemstellung

Mathematisches Schlussfolgern erfordert zwei komplementäre Fähigkeiten: den Aufbau rigoroser Beweise für wahre Aussagen und das Entdecken von Gegenbeispielen (Counterexamples) für falsche Aussagen. Während aktuelle KI-Forschung im Bereich Mathematik fast ausschließlich auf die Beweisgenerierung (Proof Construction) fokussiert ist, wird die ebenso wichtige Aufgabe des Gegenbeispiels oft vernachlässigt.

Zwei Hauptprobleme behindern den Fortschritt in diesem Bereich:

• Mangel an Trainingsdaten: Es gibt kaum Datensätze, die speziell für das Generieren von Gegenbeispielen kuratiert sind. Der einzige existierende Benchmark (CounterMath) enthält nur ca. 1.200 natürliche Sprachprobleme, was für das Training von LLMs unzureichend ist.
• Spärliche Belohnungssignale (Sparse Rewards): In Reinforcement-Learning-Szenarien verschwindet das Belohnungssignal oft, wenn das Modell für komplexe Probleme kein korrektes Gegenbeispiel findet. Dies führt zu einem Leistungsplateau, da das Modell keine Rückmeldung erhält, um sich zu verbessern.

Das Ziel der Arbeit ist es, Large Language Models (LLMs) so zu trainieren, dass sie formale Gegenbeispiele generieren können. Dies bedeutet, dass das Modell nicht nur ein Beispiel vorschlägt, sondern auch einen formalen Beweis in Lean 4 liefert, der automatisch verifiziert werden kann.

2. Methodik

Die Autoren schlagen einen integrierten Rahmen vor, der aus zwei Hauptphasen besteht: der Synthese von Gegenbeispielen und einem Multi-Reward-Training.

A. Symbolische Mutationsstrategie (Data Synthesis)

Um das Datenproblem zu lösen, entwickeln die Autoren eine Methode zur automatischen Generierung von Trainingsdaten:

1. Ausgangspunkt: Sie nehmen beweisbare, universell quantifizierte Theoreme (z. B. $\forall x, H_1(x) \land H_2(x) \to C(x)$) aus bestehenden Lean-Bibliotheken (Mathlib, LeanWorkbook) oder aus von LLMs generierten Beweisen.
2. Mutation: Ein notwendiges Hypothesen-Element (z. B. $H_1$) wird systematisch entfernt. Das resultierende Theorem ($H_2(x) \to C(x)$) ist nun falsch (da die Hypothese notwendig war).
3. Formulierung des Problems: Das neue Problem wird als existenzielle Aussage formuliert: $\exists x, H_2(x) \to C(x)$. Ein Gegenbeispiel existiert genau dann, wenn $H_1(x)$ falsch ist.
4. Validierung: Ein Lean-4-Prover wird verwendet, um sicherzustellen, dass die entfernte Hypothese tatsächlich notwendig war und das mutierte Theorem widerlegbar ist.
5. Ergebnis: Diese Strategie generierte 575.000 neue Gegenbeispiel-Probleme aus über 320.000 Saat-Theoremen.

B. Multi-Reward Guided Training (Expert Iteration)

Um das Problem der spärlichen Belohnungen zu lösen, führen die Autoren ein Multi-Reward-System ein, das auf dem Prinzip der Expert-Iteration basiert:

• Zwei Belohnungen: Für ein generiertes Gegenbeispiel $x^*$ werden zwei formale Beweise verlangt:
  1. Beweis für das mutierte Theorem (das Ziel).
  2. Beweis für die „verworfene Hypothese" (dass $H_1(x^*)$ falsch ist).
• Mechanismus: Selbst wenn das LLM das Hauptproblem (mutiertes Theorem) nicht vollständig löst, kann es oft den einfacheren Beweis für die verworfene Hypothese liefern. Dies aktiviert ein Teilergebnis (Reward), das das Training auch bei schwierigen Problemen vorantreibt.
• Gewichtung: Die finalen Gewichte für das Fine-Tuning setzen sich aus beiden Belohnungen zusammen ($\alpha$ für das Hauptziel, $1-\alpha$ für die Hypothese). Dies verhindert, dass das Modell in einer „Low-Difficulty-Falle" stecken bleibt (nur einfache Beweise zu generieren), indem die Gewichtung angepasst wird.

Der Trainingsprozess nutzt zwei Modelle:

1. Ein Modell für informelles Schlussfolgern (Vorschlag des konkreten Gegenbeispiels).
2. Ein Modell für formales Schlussfolgern (Generierung des Lean-4-Beweises).

3. Wichtige Beiträge

• Erster Framework für formale Gegenbeispiele: Die Arbeit adressiert die Lücke zwischen Beweisgenerierung und Widerlegung in formalen Umgebungen (Lean 4).
• Skalierbare Datengenerierung: Die vorgestellte Mutationsstrategie erzeugt eine massive Menge an hochwertigen Trainingsdaten (575k Instanzen), die über die manuelle Kuratierung hinausgeht.
• Multi-Reward-Strategie: Ein innovativer Ansatz zur Überwindung spärlicher Belohnungssignale, der die Effizienz des Trainings signifikant steigert, indem Teilerfolge (Beweis der verworfenen Hypothese) belohnt werden.
• Benchmark-Erweiterung: Einführung neuer Benchmarks (FOR-COUNTER, VERI-FORMALIZE, VERI-REASON) zur Evaluierung von Gegenbeispielsuche und Verifikation.

4. Ergebnisse

Die Experimente wurden auf drei neu erstellten Benchmarks durchgeführt und verglichen mit State-of-the-Art-Modellen (einschließlich proprietärer Modelle wie GPT-4.1, DeepSeek-R1 und Open-Source-Provern wie Goedel-Prover).

• Leistungssteigerung: Das feinabgestimmte Modell erreicht eine relative Verbesserung von 47 % bis 74 % in der Pass@1-Quote im Vergleich zu den stärksten Baselines.
• Konvergenz: Das Multi-Reward-Training konvergiert schneller und erreicht höhere Endleistungen als Single-Reward-Training (ca. 49 % Pass@1 vs. 43 % bei Single-Reward).
• Vergleich: Das Modell übertrifft sowohl proprietäre Reasoning-Modelle als auch bestehende Open-Source-neurale Theorembeweiser in allen getesteten Aufgaben (Gegenbeispielsuche, Verifikation von Autoformalisierungen und Verifikation von Beweisschritten).
• Datenmenge: Die Nutzung der synthetisierten 575k Datenpunkte ermöglichte ein effektives Fine-Tuning, das ohne diese Strategie nicht möglich gewesen wäre.

5. Bedeutung und Ausblick

Diese Arbeit zeigt, dass das Training von LLMs zum „Lernen des Widerlegens" (Learning to Disprove) nicht nur die Fähigkeit zur Generierung von Gegenbeispielen verbessert, sondern auch die allgemeine mathematische Schlussfolgerungsfähigkeit stärkt.

• Selbstkorrektur: Die Fähigkeit, Gegenbeispiele zu finden, ermöglicht es Modellen, ihre eigenen logischen Prozesse zu überprüfen und zu korrigieren.
• Praktische Anwendung: Das Framework dient als praktischer Assistent (Copilot) für Mathematiker, um Vermutungen zu validieren und Fehler in neuen Theoremen frühzeitig zu erkennen.
• Zukunft: Die Autoren sehen Potenzial in der Erweiterung auf komplexere Modelle und der Verbesserung der Datenqualität synthetischer Datensätze, um die Effizienz weiter zu steigern.

Zusammenfassend stellt das Paper einen bedeutenden Schritt vorwärts dar, indem es die einseitige Fokussierung auf Beweise in der KI-Mathematik korrigiert und ein robustes, datenreiches und reward-optimiertes Framework für die formale Widerlegung von Aussagen etabliert.