Das Kimi-Technikteam hat kürzlich einen technischen Bericht zur Vorschauversion von Kimina-Prover veröffentlicht und die distillierten Versionen des Modells mit 1,5 B und 7 B Parametern, das für die Datengenerierung verwendete Modell Kimina-Autoformalizer-7B und den überarbeiteten miniF2F-Benchmark-Datensatz als Open Source bereitgestellt. Kimina-Prover ist ein von Numina und dem Kimi-Team gemeinsam entwickeltes Modell zum Beweis mathematischer Theoreme. Es verwendet im Bereich der formalen Beweisführung ein neuartiges, schlussfolgerungsgesteuertes Explorationsverfahren und zeigt eine herausragende Leistung.
Kimina-Prover basiert auf dem Qwen2.5-72B-Modell und wird mit dem groß angelegten Reinforcement-Learning-(RL)-Verfahren von Kimi k1.5 trainiert. In dem anerkannten miniF2F-Benchmark für formale Mathematik erreicht die Vorschauversion von Kimina-Prover mit einem geringeren Stichprobenbudget (pass@8192) eine Erfolgsquote von 80,7 % und übertrifft damit deutlich die bisherigen besten Ergebnisse: BFS Prover mit 72,95 % (pass@2048×2×600+) und DeepSeek-Prover mit 50,0 % (pass@65536).
Der formale Beweis von Theoremen ist ein wichtiger Bereich in der Mathematik und Informatik. Dabei werden strenge mathematische Logik und Computerprogramme verwendet, um die Richtigkeit mathematischer Theoreme zu verifizieren. Es ist jedoch eine große Herausforderung, KI die Fähigkeit zum formalen Beweis zu vermitteln. Traditionelle Methoden stoßen oft an ihre Grenzen bei komplexen mathematischen Problemen, die tiefes Verständnis und Kreativität erfordern. Der jüngste Aufstieg großer Sprachmodelle (LLMs) bietet neue Hoffnung in diesem Bereich, aber bestehende Methoden weisen oft Einschränkungen auf, wie z. B. die Abhängigkeit von externen Suchen, die Schwierigkeit, tiefes Schlussfolgern zu erfassen, und das Fehlen von Skalierungseffekten.
Um diese Einschränkungen zu überwinden, verfolgt Kimina-Prover einen neuen Ansatz: Die enge Verknüpfung von groß angelegtem Reinforcement Learning (RL) mit einem „formallogischen Inferenzmuster“, um die interne „Strategie“ des Modells zur Generierung vollständiger Beweise direkt zu optimieren. Dieser Ansatz ermöglicht es dem Modell, während der Generierung von Tokens implizit den riesigen Beweisraum zu erkunden, selbstständig Inferenzpfade zu navigieren, den Rechenaufwand erheblich zu reduzieren und dem Modell eine flexiblere, der menschlichen Intuition näher kommende Explorationsweise zu verleihen. Darüber hinaus führt Kimina-Prover Belohnungssignale ein, die auf dem Endergebnis basieren. Der RL-Trainingsprozess ist zielorientiert, wobei nur vollständig korrekte und kompilierbare Beweise eine positive Belohnung erhalten.
Die ersten Forschungsergebnisse von Kimina-Prover zeigen bemerkenswerte Fortschritte. Im miniF2F-Benchmark erreicht Kimina-Prover eine Erfolgsquote von 80,7 % und übertrifft damit deutlich die bisherigen besten Ergebnisse. Es zeigt auch eine sehr hohe Stichprobeneffizienz und erzielt selbst bei sehr wenigen Stichproben wettbewerbsfähige Ergebnisse. Darüber hinaus verbessert sich die Leistung von Kimina-Prover mit zunehmender Modellgröße kontinuierlich. Dies ist der erste Nachweis eines so klaren Skalierungseffekts bei neuronalen Theorembeweisern im Bereich der formalen Mathematik. Im Vergleich zu den besten universellen Inferenz-LLMs zeigt Kimina-Prover einen überwältigenden Vorteil bei formalmathematischen Aufgaben und kann stabil formal korrekte Beweise generieren, die vom Lean-Compiler überprüft werden können.
Der Denkprozess von Kimina-Prover ist sehr gut erklärbar. Benutzer können sehen, wie das Modell schrittweise einen Beweis ableitet. Dies erleichtert das Verständnis des Modellverhaltens und die Diagnose von Fehlern und bietet das Potenzial als Hilfsmittel im Mathematikunterricht. Das Forschungsteam gibt an, dass die Leistung von Kimina-Prover mit zunehmender Modellgröße und Kontextlänge deutlich verbessert werden kann, was das Potenzial von „schlussfolgerungsbasierten neuronalen Beweisern“ bestätigt. Dieser Ansatz, der groß angelegtes Reinforcement Learning und menschenähnliche Inferenzmuster kombiniert, wird neue Wege für automatisiertes Schlussfolgern und sogar für die Entwicklung allgemeiner künstlicher Intelligenz (AGI) eröffnen.
Um die Beteiligung der Community und den Fortschritt der Forschung zu fördern, hat das Kimi-Technikteam die distillierten Versionen von Kimina-Prover mit 1,5 B und 7 B Parametern, das für die Datengenerierung verwendete Modell Kimina-Autoformalizer-7B und den überarbeiteten miniF2F-Benchmark-Datensatz als Open Source veröffentlicht.
Arxiv-Technischer Bericht: https://arxiv.org/abs/2504.11354
GitHub-Code-Repository: https://github.com/MoonshotAI/Kimina-Prover-Preview
Hugging Face Modell-Download: https://huggingface.co/collections/AI-MO/kimina-prover-preview-67fb536b883d60e7ca25d7f9
