CriticLean: Kritikergesteuertes Reinforcement Learning für mathematische Formalisierung

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

July 8, 2025

papers.authors: Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, Ge Zhang

cs.AI

papers.abstract

Die Übersetzung von mathematischen Aussagen in natürlicher Sprache in formalen, ausführbaren Code stellt eine grundlegende Herausforderung im Bereich des automatisierten Theorembeweisens dar. Während sich frühere Arbeiten auf den Erfolg bei der Generierung und Kompilierung konzentriert haben, wurde der Kritikerphase – der Bewertung, ob generierte Formalisierungen die semantische Absicht des ursprünglichen Problems tatsächlich erfassen – wenig Aufmerksamkeit geschenkt. In diesem Artikel stellen wir CriticLean vor, ein neuartiges, kritikergestütztes Reinforcement-Learning-Framework, das die Rolle des Kritikers von einem passiven Validator zu einer aktiven Lernkomponente erhebt. Konkret schlagen wir zunächst CriticLeanGPT vor, das durch überwachtes Fein-Tuning und Reinforcement Learning trainiert wird, um die semantische Treue von Lean 4-Formalisierungen rigoros zu bewerten. Anschließend führen wir CriticLeanBench ein, einen Benchmark, der entwickelt wurde, um die Fähigkeit von Modellen zu messen, semantisch korrekte von inkorrekten Formalisierungen zu unterscheiden, und zeigen, dass unsere trainierten CriticLeanGPT-Modelle starke Open- und Closed-Source-Baselines deutlich übertreffen können. Aufbauend auf dem CriticLean-Framework erstellen wir FineLeanCorpus, einen Datensatz mit über 285.000 Problemen, der eine reiche Domänenvielfalt, eine breite Schwierigkeitsabdeckung und eine hohe Korrektheit basierend auf menschlicher Bewertung aufweist. Insgesamt unterstreichen unsere Ergebnisse, dass die Optimierung der Kritikerphase entscheidend für die Erstellung zuverlässiger Formalisierungen ist, und wir hoffen, dass unser CriticLean wertvolle Einblicke für zukünftige Fortschritte im formalen mathematischen Denken liefern wird.

English

Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving. While prior work has focused on generation and compilation success, little attention has been paid to the critic phase-the evaluation of whether generated formalizations truly capture the semantic intent of the original problem. In this paper, we introduce CriticLean, a novel critic-guided reinforcement learning framework that elevates the role of the critic from a passive validator to an active learning component. Specifically, first, we propose the CriticLeanGPT, trained via supervised fine-tuning and reinforcement learning, to rigorously assess the semantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench, a benchmark designed to measure models' ability to distinguish semantically correct from incorrect formalizations, and demonstrate that our trained CriticLeanGPT models can significantly outperform strong open- and closed-source baselines. Building on the CriticLean framework, we construct FineLeanCorpus, a dataset comprising over 285K problems that exhibits rich domain diversity, broad difficulty coverage, and high correctness based on human evaluation. Overall, our findings highlight that optimizing the critic phase is essential for producing reliable formalizations, and we hope our CriticLean will provide valuable insights for future advances in formal mathematical reasoning.