Aperçu de Kimina-Prover : Vers de grands modèles de raisonnement formel par apprentissage par renforcement

Nous présentons Kimina-Prover Preview, un modèle de langage à grande échelle qui introduit un nouveau paradigme d’exploration guidée par le raisonnement pour la preuve formelle de théorèmes, tel qu’illustré dans cette version préliminaire. Entraîné via un pipeline d’apprentissage par renforcement à grande échelle à partir de Qwen2.5-72B, Kimina-Prover obtient des performances remarquables dans la génération de preuves Lean 4 en adoptant un schéma de raisonnement structuré que nous appelons pattern de raisonnement formel. Cette approche permet au modèle de reproduire des stratégies humaines de résolution de problèmes dans Lean, en générant itérativement et en affinant progressivement les étapes de preuve. Kimina-Prover établit un nouveau record sur le benchmark miniF2F, atteignant 80,7 % avec pass@8192. Au-delà de ces performances améliorées sur les benchmarks, notre travail fournit plusieurs observations clés : (1) Kimina-Prover présente une efficacité élevée en échantillonnage, offrant de bons résultats même avec un nombre minimal d’échantillons (pass@1), tout en se généralisant efficacement avec l’augmentation du budget computationnel, grâce à son schéma de raisonnement original et à son entraînement par renforcement ; (2) nous démontrons une évolution claire des performances avec la taille du modèle, un phénomène jusque-là non observé chez les prouveurs automatiques neuronaux en mathématiques formelles ; (3) le style de raisonnement appris, distinct des algorithmes de recherche classiques, montre un potentiel à réduire l’écart entre la vérification formelle et l’intuition mathématique informelle. Nous mettons à disposition sous licence open source des versions distillées de Kimina-Prover de 1,5 milliard et 7 milliards de paramètres.