Seed-Prover : raisonnement profond et large pour la démonstration automatique de théorèmes

Les modèles de langage à très grande échelle (LLM) ont fait preuve d'une capacité remarquable à raisonner mathématiquement en exploitant l'apprentissage par renforcement avec des chaînes de raisonnement longues. Toutefois, ils peinent encore à prouver des théorèmes en raison du manque de signaux de supervision clairs lorsqu’ils ne s’appuient que sur le langage naturel. Des langages spécifiques dédiés, comme Lean, offrent une supervision précise grâce à la vérification formelle des preuves, permettant ainsi une formation efficace par apprentissage par renforcement. Dans ce travail, nous proposons Seed-Prover, un modèle de raisonnement global basé sur le style des lemmes. Seed-Prover peut itérativement affiner sa preuve en s'appuyant sur les retours de Lean, sur les lemmes déjà prouvés et sur une auto-synthèse. Pour résoudre des problèmes de niveau Olympiade Internationale (IMO), nous avons conçu trois stratégies d’inférence à l’évaluation (test-time) permettant à la fois un raisonnement profond et large. Seed-Prover parvient à prouver 78,1 % des problèmes d’IMO formalisés, atteint la saturation sur MiniF2F, et obtient un taux supérieur à 50 % sur PutnamBench, surpassant largement l’état de l’art précédent. Pour pallier le manque de prise en charge de la géométrie dans Lean, nous introduisons un moteur de raisonnement géométrique, Seed-Geometry, qui dépasse les moteurs formels de géométrie précédents. Nous avons utilisé ces deux systèmes pour participer à l’IMO 2025, où nous avons réussi à prouver entièrement 5 des 6 problèmes. Ce travail représente une avancée significative dans le domaine du raisonnement mathématique automatisé, démontrant l’efficacité de la vérification formelle combinée à un raisonnement par chaîne de pensée longue.