Kimina-Prover-Vorschau: Schritte hin zu großen formalen Schlussfolgerungsmodellen mit Verstärkungslernen

Wir stellen Kimina-Prover Preview vor, einen großen Sprachmodell, das ein neuartiges, reasoning-getriebenes Erkundungsparadigma für die formale Beweisführung einleitet, wie in dieser Vorschauversion demonstriert wird. Kimina-Prover wurde mit einer großskaligen Reinforcement-Learning-Pipeline auf Basis von Qwen2.5-72B trainiert und zeigt herausragende Leistung bei der Generierung von Beweisen in Lean 4, indem es ein strukturiertes Schlussfolgerungsmuster verwendet, das wir als \textit{formales Schlussfolgerungsmuster} bezeichnen. Dieser Ansatz ermöglicht es dem Modell, menschliche Problemlösungsstrategien in Lean nachzuahmen, indem es Beweisschritte iterativ generiert und verfeinert. Kimina-Prover erreicht eine neue Sollwert-Leistung auf dem miniF2F-Benchmark mit 80,7 % bei pass@8192. Neben der verbesserten Benchmark-Leistung liefert unsere Arbeit mehrere zentrale Erkenntnisse: (1) Kimina-Prover zeichnet sich durch eine hohe Stichproben-Effizienz aus und erzielt bereits mit minimaler Stichprobengröße (pass@1) starke Ergebnisse, wobei sich die Leistung effektiv mit steigendem Rechenaufwand skaliert – eine Eigenschaft, die auf seinem einzigartigen Schlussfolgerungsmuster und der RL-Trainingsstrategie beruht; (2) wir zeigen eine klare Leistungssteigerung mit wachsender Modellgröße, ein Trend, der bisher bei neuronalen Beweisführern im Bereich der formalen Mathematik nicht beobachtet wurde; (3) der erlernte Schlussfolgerungsstil unterscheidet sich deutlich von traditionellen Suchalgorithmen und zeigt Potenzial, die Kluft zwischen formaler Verifikation und informeller mathematischer Intuition zu überbrücken. Wir stellen ausgewählte, komprimierte Versionen von Kimina-Prover mit jeweils 1,5 B und 7 B Parametern als Open Source zur Verfügung.