CriticLean: Critic-gesteuertes Reinforcement Learning für die mathematische Formalisierung

Die Übersetzung natürlichsprachlicher mathematischer Aussagen in formellen, ausführbaren Code stellt eine grundlegende Herausforderung im Bereich der automatischen Theorembeweisung dar. Während bisherige Arbeiten sich auf die Generierung und Kompilierungserfolg konzentriert haben, wurde der Critics-Phase – der Bewertung, ob die generierten Formalisierungen tatsächlich die semantische Absicht des ursprünglichen Problems erfassen – wenig Aufmerksamkeit geschenkt. In dieser Arbeit stellen wir CriticLean vor, ein neuartiges, von einem Critic geleitetes Reinforcement-Learning-Framework, das die Rolle des Critics von einem passiven Validierer zu einer aktiven Lernkomponente erhöht. Insbesondere schlagen wir zunächst CriticLeanGPT vor, das durch überwachtes Feinjustieren und Reinforcement Learning trainiert wird, um die semantische Treue von Lean 4-Formalisierungen streng zu bewerten. Anschließend führen wir CriticLeanBench ein, einen Benchmark, der entwickelt wurde, um das Vermögen von Modellen zu messen, semantisch korrekte von inkorrekten Formalisierungen zu unterscheiden. Wir zeigen, dass unsere trainierten CriticLeanGPT-Modelle erheblich bessere Ergebnisse als starke Open-Source- und Closed-Source-Baselines erzielen können. Aufbauend auf dem CriticLean-Framework erstellen wir FineLeanCorpus, einen Datensatz mit über 285.000 Problemen, der eine reiche Domänenvielfalt, breite Schwierigkeitsgradabdeckung und hohe Korrektheit auf Basis menschlicher Bewertung aufweist. Insgesamt unterstreichen unsere Ergebnisse, dass die Optimierung der Critics-Phase für die Erstellung verlässlicher Formalisierungen entscheidend ist. Wir hoffen, dass unser CriticLean wertvolle Erkenntnisse für zukünftige Fortschritte im Bereich der formalen mathematischen Beweisführung bieten wird.