💻 computer science

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Diese Studie zeigt, dass RL-trainierte Lean-Theorembeweiser unter einem Inferenzzeit-Modus-Collapse leiden, der durch die Anwendung eines festen Schemas diverser Taktik-Skelette effektiv gemildert werden kann, um erhebliche Leistungssteigerungen zu erzielen, während das Paraphrasieren von Prompts und irrelevante Kommentare sich als unwirksam oder nachteilig erweisen.

Ursprüngliche Autoren: Zachary Burton

Veröffentlicht 2026-05-19

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Zachary Burton

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 einen brillanten Schüler vor, der darin geschult wurde, sehr schwierige Mathe-Rätsel mit einer speziellen Computersprache namens Lean zu lösen. Dieser Schüler, nennen wir ihn „DeepSeek", ist unglaublich intelligent, hat aber eine seltsame Angewohnheit: Wenn er gebeten wird, ein Rätsel zu lösen, gerät er in eine mentale Sackgasse.

Dieser Artikel ist ein Diagnosebericht darüber, warum das passiert und wie man es beheben kann. Hier ist die Geschichte dessen, was die Forscher herausfanden, in alltäglichen Worten erzählt.

1. Das Problem: Der „kaputte Plattenspieler"-Effekt

Die Forscher stellten fest, dass DeepSeek, wenn sie ihn aufforderten, dasselbe Mathe-Rätsel immer wieder zu lösen (nur mit leicht unterschiedlichen Zufallswerten, wie beim Würfeln), stets denselben ersten Schritt versuchte.

Die Analogie: Stellen Sie sich vor, Sie versuchen, eine verschlossene Tür zu öffnen. Sie stecken den Schlüssel ins Schloss. Es funktioniert nicht. Sie versuchen es erneut. Es funktioniert immer noch nicht. Sie versuchen es ein drittes Mal und ein hunderttes Mal. Selbst wenn Sie es 64 Mal versuchen, stecken Sie einfach denselben Schlüssel auf dieselbe Weise in dasselbe Schloss. Sie erkunden keine anderen Schlüssel oder andere Wege, die Tür zu öffnen.
Das Ergebnis: In der Studie führte die Verdopplung der Versuche von 32 auf 64 nicht zur Lösung eines einzigen neuen Rätsels. Der Schüler war in einen „Modus-Kollaps" geraten – er war auf einem schmalen Pfad festgefahren und konnte an nichts anderes denken.

2. Die Lösung: Ein „erster Schritt"-Hinweis

Die Forscher erkannten, dass der Schüler nicht faul war; er war einfach zu sehr in seiner Routine gefangen. Also versuchten sie einen neuen Trick: Bevor sie den Schüler aufforderten, das Rätsel zu lösen, gaben sie ihm eine spezifische Anweisung, wie er beginnen sollte.

Die Analogie: Anstatt nur zu sagen: „Löse dieses Rätsel", sagten die Forscher: „Beginne damit, die Zahlen zu vereinfachen" oder „Beginne damit, eine neue Variable einzuführen". Es ist, als würde man dem Schüler einen spezifischen Schlüssel zum ersten Versuch geben, anstatt ihn raten zu lassen.
Das Ergebnis: Dieser einfache Impuls durchbrach die Sackgasse. Der Schüler begann plötzlich, viel mehr Rätsel zu lösen. Die „Sackgasse" lag nicht daran, dass der Schüler schlecht in Mathe war; sie lag daran, dass er zu starr war, wie er begann.

3. Das „Warum": Es ist ein Trainingsproblem, kein Gehirnproblem

Die Forscher wollten wissen: Ist der Schüler von Natur aus schlecht in Mathe, oder hat das Training ihn starr gemacht?

Das Experiment: Sie testeten den Schüler, bevor er das spezielle Mathe-Training erhielt (das „Basis"-Modell).
Die Erkenntnis: Der untrainierte Schüler konnte keine Rätsel lösen. Er gab einfach auf oder wiederholte die Frage.
Die Schlussfolgerung: Das spezielle Training (Bestärkendes Lernen) war es, das dem Schüler überhaupt erst beibrachte, Rätsel zu lösen. Aber genau dieses gleiche Training war es auch, das ihn starr machte und in eine Sackgasse führte. Das Training schuf die Fähigkeit, aber es schuf auch das „kaputte Plattenspieler"-Problem.

4. Wer hat sonst noch dieses Problem?

Die Forscher testeten andere „Schüler" (verschiedene KI-Modelle), um zu sehen, ob dies ein universelles Problem ist.

Der „SFT"-Schüler: Ein Schüler wurde anders trainiert (Supervised Fine-Tuning). Dieser Schüler war insgesamt tatsächlich besser darin, Rätsel zu lösen, aber er hatte kein „Sackgassen"-Problem. Als die Forscher ihm Hinweise gaben, wurde er dadurch sogar leicht schlechter. Er war bereits flexibel genug, um seinen eigenen Weg zu finden.
Die „RL"-Schüler: Die Schüler, die mit der speziellen „Bestärkenden Lern"-Methode trainiert wurden (wie DeepSeek), waren diejenigen, die feststeckten. Sie benötigten die „ersten Schritt"-Hinweise, um aus ihrem engen Denken auszubrechen.

5. Der „erster Zug"-Beweis

Um zu beweisen, dass dies kein Zufall war, betrachteten die Forscher die tatsächlichen „ersten Züge", die die Schüler machten.

Die Erkenntnis: Bei 64 Versuchen an einem einzigen Rätsel verwendete der „sackgassenhafte" Schüler in fast der Hälfte der Fälle exakt denselben ersten Zug. Er war unglaublich vorhersehbar.
Die Metapher: Wenn man einen Menschen auffordern würde, 64 Mal eine Geschichte zu schreiben, könnte er mit „Es war einmal", „Die Sonne schien" oder „Es war eine dunkle Nacht" beginnen. Aber dieser KI-Schüler würde 32 Mal mit „Es war einmal" und 30 Mal mit „Die Sonne schien" beginnen. Er hatte fast keine Vielfalt in seiner Eröffnung.

Zusammenfassung

Der Artikel kommt zu dem Schluss, dass Bestärkendes Lernen (eine bestimmte Art, KI zu trainieren) ein zweischneidiges Schwert schafft:

Es lehrt die KI, formale mathematische Beweise zu lösen (was sie vorher nicht konnte).
Aber es macht die KI auch so fokussiert auf einige wenige „gewinnende" Strategien, dass sie aufhört, neue zu erkunden.

Die Lösung besteht nicht darin, der KI mehr Rechenleistung oder mehr Zeit zum Nachdenken zu geben; es geht darum, ihr strukturelle Anleitung zu geben – einen einfachen Impuls, wie man den Beweis beginnt. Dies zwingt die KI, ihre Routine zu durchbrechen und neue Wege zu erkunden, wodurch Lösungen freigeschaltet werden, die sie zuvor zu stur war, um sie zu finden.

Technische Zusammenfassung: Diversität zur Inferenzzeit bei mit RL trainierten Lean-Theorembeweisern

Problemstellung

Neuere neuronale Theorembeweiser, insbesondere solche, die mit Reinforcement Learning (RL) und verifizierbaren Belohnungen (RLVR) trainiert wurden, haben starke Leistungen auf formalen Beweis-Benchmarks wie miniF2F erzielt. Die vorherrschende Annahme ist, dass ausreichendes RL-Training und eine erhöhte Rechenleistung zur Inferenzzeit (durch i.i.d.-Abtastung) es Modellen ermöglichen, die für formale Beweise notwendigen strukturellen Priors zu internalisieren.

Dieses Papier stellt diese Annahme in Frage und diagnostiziert ein Phänomen des Mode Collapse (Modus-Kollaps) zur Inferenzzeit bei mit RL trainierten Lean-Beweisern. Konkret beobachten die Autoren, dass eine Erhöhung des Abtastbudgets ( $k$ ) viel früher als erwartet abnehmende Grenzerträge liefert. Auf dem miniF2F-test-Benchmark mit DeepSeek-Prover-V1.5-RL führt eine Verdopplung des Abtastbudgets von $k=32$ auf $k=64$ zu keinen zusätzlichen gelösten Theoremen (stecken bei 42/244). Das Modell konvergiert auf einen engen Satz von Beweisstrategien und versagt darin, Alternativen zu erkunden, selbst wenn zusätzliche stochastische Stichproben bereitgestellt werden.

Methodik

Die Studie verwendet einen kontrollierten Diagnoserahmen mit DeepSeek-Prover-V1.5-RL und seiner nicht-RL-Basisvariante sowie modellübergreifende Vergleiche mit DeepSeek-Prover-V2-7B (RL) und Goedel-Prover (nur SFT).

1. Die Skelett-Zeitplan-Intervention

Um zu testen, ob das Plateau auf einen Mangel an struktureller Vielfalt und nicht auf einen Mangel an Rechenleistung zurückzuführen ist, führen die Autoren einen festen, deterministischen Zeitplan von 15 Taktik-Skeletten ein.

Struktur: Ein $15 \times 8 = 120$ -Gitter, das 15 handverlesene Lean-Taktik-Skelette (z. B. simp, intro, constructor, aesop) mit 8 Ziel-Hinweis-Kommentaren (natürlichsprachliche Vorschläge) kombiniert.
Ausführung: Für ein Budget $k$ versucht das Modell die ersten $k$ Einträge dieses Gitters. Dies zwingt das Modell, Beweise mit spezifischen strategischen Eröffnungen zu beginnen, anstatt sich auf zufällige Abtastung zu verlassen.
Ablationen: Um die Quelle der Verbesserung zu isolieren, vergleichen die Autoren:
- B-RL (Skelett): Der strukturierte Zeitplan mit 15 Skeletten.
- C1 (Paraphrase): 16 semantisch äquivalente Paraphrasen der Anweisung (keine Taktikstruktur).
- C2 (Irrelevante Kommentare): 16 inhaltsleere Lean-Kommentare.
- C3 (NL-only): Eine dedizierte Bedingung, die nur natürliche Sprachhinweise ohne Taktik-Präfixe verwendet.

2. Schwierigkeitsstratifizierung

Die Autoren definieren einen empirischen Formalisierungs-Schwierigkeits-Score ( $\sigma$ ) mittels einer Leave-One-Out-Konstruktion. Für ein Ziel-Theorem zählt $\sigma$ , wie viele andere Basis-Modelle (Goedel-Prover, V2-7B) es ohne Intervention lösen. Dies stratifiziert Theoreme in Buckets: Frontier (von anderen ungelöst), Hard, Medium, Easy und Trivial.

3. Direkte Verteilungsmessung

Um über Verhaltensplateaus hinauszugehen, analysieren die Autoren die Vielfalt der ersten Taktik-Köpfe über 13.159 stochastische Stichproben. Sie zählen die Anzahl der verschiedenen führenden Taktik-Identifikatoren (z. B. have, rw, norm_num), die pro Theorem generiert werden.

Wichtige Ergebnisse

1. Durchbrechen des Plateaus durch strukturelle Führung

Basis-Kollaps: DeepSeek-Prover-V1.5-RL mit i.i.d.-Abtastung löst 38 Theoreme bei $k=16$ , 42 bei $k=32$ und bleibt bei $k=64$ auf 42 stehen.
Wirksamkeit der Skelette: Der feste Skelett-Zeitplan durchbricht dieses Plateau und löst 55 Theoreme bei $k=16$ (+45 % relative Verbesserung) und findet weiterhin neue Beweise bis $k=64$ (insgesamt 60).
Ablations-Ergebnisse:
- Struktur vs. Vielfalt: Anweisungs-Paraphrasen (C1) erzielen denselben pass@16-Wert wie die Basis (38/244), während irrelevante Kommentare (C2) die Leistung auf 25/244 verschlechtern. Dies bestätigt, dass die Gewinne durch strukturelle Führung und nicht durch bloße Prompt-Vielfalt getrieben werden.
- NL vs. Taktiken: Die NL-only-Bedingung (C3) löst 48/244, was zwischen Basis und vollen Skeletten liegt. Dies zeigt, dass natürliche Sprachhinweise etwa 58 % der Lücke schließen, während wörtliche Taktik-Präfixe den Rest beitragen.

2. Lokalisierung des Gewinns

Der strukturelle Gewinn ist in den Easy- und Trivial-Buckets konzentriert (Theoreme, die von anderen Open-Source-Beweisern gelöst werden können, aber von der i.i.d.-Abtastung von V1.5-RL verpasst werden).

In der kombinierten Easy+Trivial-Spalte ergibt die Skelett-Intervention einen Nettogewinn von +15, während Paraphrasen 0 und irrelevante Kommentare -14 ergeben.
Keine Störung schließt den „Frontier"-Bucket auf (Theoreme, die von keinem Basis-Modell gelöst werden), was darauf hindeutet, dass die Intervention die Untererforschung bekannter lösbarer Probleme behebt und nicht die Grenze der Fähigkeiten erweitert.

3. RL-Spezifität des Mode Collapse

Basis-Modell-Kontrast: DeepSeek-Prover-V1.5-Base (nicht-RL) beweist unter keiner Bedingung (i.i.d. oder Skelette) ein einziges Theorem. Dies stellt fest, dass RL sowohl der Ursprung der Beweisfähigkeit als auch der Ort des nachfolgenden Mode Collapse ist. Das Basis-Modell verfügt nicht über die Fähigkeit, gültige Beweise zu generieren; die RL-Phase schafft die Fähigkeit, kollabiert sie jedoch in eine enge Policy.
Modellübergreifender Kontrast:
- V2-7B (RL): Zeigt einen flachen aggregierten Gewinn (+1), schließt aber +3 Frontier-Theoreme auf, die für keine i.i.d.-Basis erreichbar sind.
- Goedel-Prover (SFT): Zeigt einen negativen Gewinn (-10,0 $\pm$ 4,4) mit Skeletten. SFT-trainierte Modelle scheinen bereits einen breiten Satz von Taktik-Stämmen zu erkunden, was den festen Skelett-Zeitplan redundant oder einschränkend macht.

4. Direkte Evidenz des Kollapses

Die Verteilungsanalyse zeigt, dass das mediane Theorem über 64 Stichproben hinweg nur 2 verschiedene erste Taktik-Köpfe erhält, wobei 49 % des Benchmarks eine deterministische einzelne strategische Eröffnung erhalten. Die beobachtete Shannon-Entropie beträgt $\le 8\%$ der theoretischen Kapazität, was einen schweren Mode Collapse bestätigt.

Bedeutung und Behauptungen

Das Papier rahmt die Erzählung von „Taktik-Skelette verbessern die Leistung" um zu „RL-trainierte Beweiser erkunden den Taktik-Raum zur Inferenzzeit stark unzureichend".

RL als dualer Agent: Die Autoren behaupten, dass RL eine duale Rolle spielt: Es ist die Phase, die Beweisfähigkeit schafft (da das Basis-Modell keine hat), und gleichzeitig die Phase, die diese Fähigkeit auf eine enge Policy kollabiert.
Skalierung zur Inferenzzeit: Die Ergebnisse deuten darauf hin, dass eine reine Skalierung der Inferenz-Rechenleistung durch i.i.d.-Abtastung viel früher als angenommen abnehmende Grenzerträge hat. Strukturelle Vielfalt (Variation von Beweisstrategien über Prompts) ist ein effizienterer Skalierungsansatz.
Behandelbarkeit: Der Mode Collapse ist spezifisch für RL-trainierte Modelle. SFT-trainierte Modelle zeigen denselben durch strukturelle Hinweise wiederherstellbaren Kollaps nicht; tatsächlich leiden sie darunter. Dies impliziert, dass zukünftige Interventionen (Entropie-Regularisierung während des Trainings oder Skelett-Wiedergewinnung zur Inferenzzeit) den Trade-off zwischen der Schaffung von Fähigkeit und der Aufrechterhaltung der Vielfalt navigieren müssen.

Die Studie kommt zu dem Schluss, dass der „Mode Collapse" ein reales, pipeline-abhängiges Phänomen ist, das dem RL-Fine-Tuning-Prozess in Domänen der formalen Verifikation inhärent ist, und dass feste strukturelle Interventionen die verlorene Erkundung effektiv wiederherstellen können, ohne zusätzliches Training zu erfordern.