StepFun-Prover Preview est un modèle de langage à grande échelle conçu pour la démonstration formelle de théorèmes via un raisonnement intégré aux outils. Grâce à un pipeline d'apprentissage par renforcement intégrant des interactions avec les outils, StepFun-Prover atteint des performances robustes en générant des preuves Lean 4 avec un échantillonnage minimal. Cette approche permet au modèle d'améliorer ses preuves de manière itérative grâce à des retours environnementaux en temps réel, imitant ainsi des stratégies de résolution de problèmes de type humain. Lors du test miniF2F, StepFun-Prover atteint un taux de réussite de 70,0 %. Au-delà de l'amélioration des performances du test, nous présentons un cadre d'entraînement complet pour le développement de modèles de raisonnement intégrés aux outils, suggérant des pistes prometteuses pour la démonstration automatisée de théorèmes et les assistants mathématiques d'IA.
