LongCat-Flash-Prover -- Formale Beweisfuehrung durch agentic Reinforcement Learning
Das LongCat-Team von Meituan hat im Maerz 2026 LongCat-Flash-Prover vorgestellt -- ein Open-Source Mixture-of-Experts-Modell mit 560 Milliarden Parametern, das auf formale mathematische Beweisfuehrung in Lean4 spezialisiert ist. Das Modell setzt neue Bestmarken auf mehreren Benchmarks fuer formales Reasoning und uebertrifft dabei alle bisherigen Open-Weights-Baselines deutlich.
Kernaussagen
LongCat-Flash-Prover erreicht eine Pass-Rate von 97.1% auf dem MiniF2F-Test-Benchmark (bei 72 Inferenzen pro Problem), 70.8% auf ProverBench und 41.5% auf PutnamBench. Diese Ergebnisse liegen deutlich ueber allen bisherigen Open-Weights-Modellen. Der zentrale Beitrag ist die Zerlegung formalen Reasonings in drei komplementaere Faehigkeiten: Auto-Formalisierung (natuerlichsprachige Aussagen in Lean4-Syntax uebersetzen), Sketching (Beweisstrategien auf hoher Ebene entwerfen) und Proving (die eigentlichen Beweisschritte ausfuehren). Modell und Code sind auf GitHub und HuggingFace offen verfuegbar.
Methodik
Das Herzstueck ist der neue RL-Algorithmus HisPO (Hierarchical Importance Sampling Policy Optimization), der speziell fuer lange Interaktionshorizonte entwickelt wurde. Klassisches RL scheitert bei formaler Beweisfuehrung oft an der Laenge der Trajektorien -- ein Beweis kann dutzende Interaktionsschritte mit dem Lean4-Verifier erfordern. HisPO stabilisiert das Training, indem es eine hierarchische Gewichtung der Samples einfuehrt, die fruehe Explorationsschritte staerker beruecksichtigt. Das Modell interagiert dabei direkt mit Lean4 als externem Tool: es formuliert Beweisschritte, erhaelt Feedback vom Verifier und passt seine Strategie entsprechend an. Dieser agentic-RL-Ansatz macht den Verifier zum integralen Bestandteil der Trainingsschleife.
Relevanz fuer die Praxis
Formale Verifikation gilt als einer der vielversprechendsten Wege zu zuverlaessigem AI-generiertem Code. Wenn ein Modell mathematische Aussagen formal beweisen kann, laesst sich dieses Prinzip potenziell auf die Verifikation von Software-Eigenschaften uebertragen. Der agentic-RL-Ansatz ist dabei besonders interessant: statt Beweisfuehrung als reines Textgenerierungsproblem zu behandeln, nutzt das Modell den Lean4-Verifier als Tool und lernt aus dessen Feedback. Dieses Muster -- RL mit externen Verifizierungstools -- duerfte sich auf andere Domaenen uebertragen lassen, etwa auf Code-Generierung mit Compiler-Feedback oder auf wissenschaftliche Hypothesenbildung mit Experiment-Feedback.