Meituan veröffentlicht ein Open-Source-Modell zur Beweisführung mit 560 Milliarden Parametern, das bei 72 Schritten Inferenz eine Durchsatzrate von 97,1 % erreicht und den Open-Source-Stand der Technik (SOTA) neu definiert.

Gate News Nachrichten, 21. März: Das Meituan LongCat-Team hat LongCat-Flash-Prover open source gestellt. Es handelt sich um ein MoE-Modell mit 560 Milliarden Parametern, das sich auf mathematische Beweisaufgaben in der formalen Theoriebildungssprache Lean4 spezialisiert hat. Die Modellgewichte werden unter MIT-Lizenz veröffentlicht und sind auf GitHub, Hugging Face und ModelScope verfügbar.

Das Modell zerlegt formale Schlussfolgerungen in drei unabhängige Fähigkeiten: automatische Formalisierung (Umwandlung natürlicher Sprachmathematik in Lean4-formale Aussagen), Skizzen-Erstellung (Erzeugung von Beweisrahmen im Lemma-Stil) und vollständige Beweisgenerierung. Alle drei Fähigkeiten werden durch das Agent-Toolkit integriert, das reasoning (TIR) mit dem Lean4-Compiler in Echtzeit interaktiv überprüft.

Im Trainingsprozess schlägt das Team den Hybrid-Experts Iteration Framework vor, um Cold-Start-Daten zu generieren, und führt im Reinforcement-Learning-Abschnitt den HisPO-Algorithmus ein, um das MoE-Modell bei langfristigen Aufgaben stabil zu trainieren. Zudem werden Theorem-Konsistenz- und Legalitätsprüfmechanismen eingesetzt, um Reward-Hacking zu verhindern.

Benchmark-Tests zeigen, dass LongCat-Flash-Prover bei offenen Gewichtsmodellen die SOTA in automatischer Formalisierung und Theorem-Beweis erreicht. Beim MiniF2F-Test liegt die Durchdringungsrate nach nur 72 reasoning-Schritten bei 97,1 %, ProverBench und PutnamBench erreichen 70,8 % bzw. 41,5 %, wobei die Anzahl der reasoning-Schritte pro Aufgabe 220 nicht übersteigt.