Seed-Prover de ByteDance: SOTA en Preuve Mathématique Automatisée

Les grands modèles linguistiques (LLM) ont démontré des avancées significatives en matière de raisonnement mathématique, exploitant souvent leurs capacités linguistiques naturelles pour améliorer les performances sur des benchmarks comme MATH et AIME. Cependant, un défi majeur dans l'entraînement de ces modèles avec l'apprentissage par renforcement (RL) est la difficulté de vérifier la correction des preuves en langage naturel, ce qui nécessite généralement une vérification manuelle méticuleuse de chaque étape. Cette limitation entrave l'application plus large du RL dans le développement de modèles de preuve de théorèmes mathématiques. Bien que des langages formels tels que Lean fournissent une vérification automatique de la correction, les prouveurs formels actuels basés sur les LLM rencontrent encore des limitations. Par exemple, les prouveurs au niveau des étapes génèrent du code de manière incrémentielle mais nécessitent souvent un support structurel spécifique et ont des difficultés avec le raisonnement de haut niveau.

En réponse, l'équipe Seed de ByteDance a introduit Seed-Prover, un nouveau modèle de raisonnement de preuve complète de style lemme. Seed-Prover affine itérativement les preuves en intégrant le feedback de Lean, en utilisant des lemmes précédemment établis et en employant l'auto-résumé. Il intègre trois stratégies d'inférence spécialisées au moment du test, permettant des capacités de raisonnement profondes et étendues pour aborder des problèmes complexes, y compris ceux rencontrés lors des Olympiades Internationales de Mathématiques (OIM). Son innovation fondamentale réside dans l'adoption d'une approche de preuve de style lemme, qui centre le processus de raisonnement autour des lemmes plutôt que des méthodes traditionnelles de génération de preuve étape par étape ou monolithique. En complément, Seed-Geometry est également introduit, un moteur de raisonnement géométrique spécialisé conçu pour surmonter les limitations de Lean dans le traitement des problèmes géométriques.

L'interaction entre Seed-Prover et Lean est facilitée par un cadre d'apprentissage par renforcement multi-étapes et multi-tâches basé sur VAPO. L'ensemble de données d'entraînement combine des ensembles de données publiquement disponibles avec les problèmes formels internes de ByteDance. Un composant «proposeur» est utilisé pour générer des variations plus simples de tâches difficiles, tandis que les problèmes trop simples (avec des taux de preuve supérieurs à 25%) sont exclus. Le backend de Seed-Geometry prend en charge la génération de problèmes à grande échelle, ayant identifié plus de 230 millions de problèmes uniques en sept jours, démontrant une amélioration octuple de l'efficacité de la recherche. Bien que des modèles de politique et de valeur séparés soient entraînés, des tests approfondis ont indiqué que les modèles de valeur pouvaient parfois réduire les performances en raison d'erreurs d'estimation, ce qui a conduit à l'adoption de la génération étape par étape avec recherche en faisceau dans des configurations distribuées.

Seed-Prover a atteint des résultats de pointe sur plusieurs benchmarks mathématiques. Aux OIM 2025, Seed-Prover a réussi à résoudre 5 problèmes sur 6 ; plus précisément, Seed-Geometry a instantanément résolu le problème 2, et Seed-Prover a dérivé des preuves pour les problèmes restants en utilisant divers paramètres d'inférence. Sur les problèmes passés des OIM, il a prouvé 121 tâches sur 155, atteignant un taux de succès de 78,1% sur tous les niveaux de difficulté. Cette performance inclut la résolution de 47 problèmes faciles sur 55, 47 problèmes moyens sur 56 et 27 problèmes difficiles sur 44. Les taux de succès par matière étaient également solides, avec 72 sur 85 en algèbre, 42 sur 55 en théorie des nombres et 7 sur 14 en combinatoire.

Sur le benchmark MiniF2F, les chercheurs ont rapporté un taux de preuve de 99,6 % pour les ensembles de validation et de test dans des réglages moyens, résolvant avec succès des problèmes difficiles tels que l'OIM 1990 P3. Les résultats de PutnamBench ont montré une amélioration significative, passant de 201 à 331 problèmes résolus sur 657 lors de la mise à niveau des réglages d'inférence légers à moyens, marquant un saut de performance notable par rapport aux systèmes de raisonnement mathématique de niveau universitaire précédents. Bien que Seed-Prover ait résolu 30 problèmes sur 100 de combinatoire sur CombiBench, surpassant les méthodes existantes, les résultats ont également mis en évidence les défis persistants en matière de raisonnement combinatoire. De plus, Seed-Prover a atteint un taux de succès de 81,8 % sur MiniCTX-v2, démontrant de fortes capacités de généralisation au-delà des problèmes spécifiques aux compétitions et surpassant la ligne de base o4-mini de 44,3 % à Pass@8.

En résumé, l'équipe Seed de ByteDance a introduit Seed-Geometry et Seed-Prover, deux méthodes de raisonnement formel qui intègrent efficacement les capacités des LLM. Seed-Geometry fournit une vérification accélérée et des mécanismes de recherche améliorés pour les problèmes géométriques, tandis que Seed-Prover utilise un raffinement itératif et des stratégies complexes d'inférence au moment du test pour les preuves mathématiques générales. La réussite de la résolution de 5 problèmes sur 6 aux OIM 2025 souligne l'efficacité pratique de ces méthodes pour aborder les compétitions mathématiques d'élite. L'adoption de langages formels comme Lean fournit une vérification rapide des preuves qui est à la fois plus rentable que les experts humains et plus fiable que les juges basés sur les LLM. La recherche future se concentrera sur la combinaison plus poussée des systèmes formels avec les LLM pour aborder les conjectures mathématiques ouvertes.