Leanstral 1.5 : l’abondance de preuves pour tous

Depuis son lancement, Leanstral propose une approche ouverte et pragmatique de l’ingénierie de preuve dans Lean 4. Nous publions aujourd’hui Leanstral 1.5, un modèle gratuit sous licence Apache-2.0, avec 119B paramètres au total et seulement 6B paramètres actifs. Il apporte un gain de performance qui rend la vérification formelle plus puissante et plus accessible.

Leanstral 1.5 sature miniF2F, résout 587/672 problèmes PutnamBench, et atteint un nouvel état de l’art de 87 % sur FATE-H et 34 % sur FATE-X. Au-delà des benchmarks, il vérifie des propriétés complexes de code et met au jour des bugs jusque-là inconnus dans des dépôts open source — ce qui montre que les méthodes formelles rigoureuses peuvent être à la fois efficaces et pratiques pour des usages réels.

Entraîner Leanstral

Leanstral 1.5 suit un processus en trois étapes : mid-training, fine-tuning supervisé et apprentissage par renforcement avec CISPO. Leanstral 1.5 s’appuie sur un entraînement étendu dans deux environnements RL :

Dans l’environnement multitour, le modèle reçoit l’énoncé d’un théorème et doit soit le prouver, soit le réfuter. Le modèle soumet une preuve, reçoit le retour du compilateur Lean, puis affine son approche à chaque tentative. Si la preuve compile, il réussit ; sinon, la boucle continue jusqu’à ce que le modèle résolve le problème ou épuise son budget.

Dans l’environnement d’agent de code, Leanstral fonctionne comme un développeur dans un système de fichiers brut : il modifie des fichiers, exécute des commandes bash et utilise le serveur de langage Lean pour inspecter les objectifs, les erreurs et les informations de type en temps réel. Il peut ainsi traiter des tâches longues, comme compléter des preuves partielles dans un dépôt, construire des lemmes auxiliaires et poursuivre le travail sur plusieurs cycles de compaction du contexte. Le modèle apprend à parcourir tout le workflow d’ingénierie de preuve, puis sa correction est finalement vérifiée par notre fork de SafeVerify à partir d’une liste de théorèmes cibles.

Évaluation

Nous évaluons Leanstral sur les benchmarks suivants :

• miniF2F est un benchmark inter-systèmes pour les mathématiques formelles. Il va des problèmes élémentaires aux défis de niveau IMO, et teste des capacités de preuve variées en algèbre, en combinatoire et en théorie des nombres.

• PutnamBench comprend 672 problèmes issus de la Putnam Mathematical Competition. Leur résolution exige un raisonnement approfondi et de longues chaînes de preuve.

• FATE-H et FATE-X sont des benchmarks d’algèbre abstraite pour des problèmes de niveau master et doctorat, respectivement. Ils testent le raisonnement avancé dans des domaines comme la théorie des groupes, la théorie des anneaux et la théorie des modules.

• FLTEval s’appuie sur de vraies pull requests du dépôt du dernier théorème de Fermat, et teste l’ingénierie de preuve pratique avec une complexité issue de cas réels.

Nous saturons complètement miniF2F, avec 100 % sur les ensembles de validation et de test. Sur PutnamBench et FATE-H/X, nous comparons Leanstral 1.5 à Goedel-Architect sans guidage en langage naturel, à Seed-Prover 1.5 avec son réglage élevé et à AxProverBase. Leanstral atteint un nouvel état de l’art sur FATE-H/X, en résolvant respectivement 87 et 34 problèmes. Sur PutnamBench, il devance Seed-Prover 1.5 high de 7 problèmes, pour un coût nettement inférieur : environ 4 $ par problème, contre une estimation de 300 $ ou plus pour Seed-Prover, dont le réglage élevé utilise un budget de 10 jours-H20 par problème. Les seuls prouveurs mieux classés fonctionnent dans des conditions différentes : certains reçoivent un guidage de preuve en langage naturel, d’autres coûtent beaucoup plus cher à exécuter, comme Aleph Prover à 54–68 $ par problème.

Leanstral 1.5 montre le meilleur scaling au moment du test que nous ayons observé sur un modèle de raisonnement formel. La figure ci-dessous suit Pass@8 sur PutnamBench lorsque nous augmentons le budget de tokens par tentative de 25k à 4M : la performance progresse de manière régulière et monotone tout au long du parcours, de 44 problèmes résolus à 50k à 244 à 200k, 493 à 1M et 587 à 4M. Plutôt que d’abandonner lorsqu’une preuve devient longue, Leanstral continue à raisonner, à modifier des fichiers et à réviser sur plusieurs millions de tokens. Il transforme directement ce budget en problèmes résolus — le même comportement que pour la preuve sur les arbres AVL ci-dessous, qui a utilisé plus de 2,7 millions de tokens sur 22 compactions.

Avec cette version, nous publions aussi FLTEval entièrement en open source. Leanstral 1.5 fait passer le pass@1 du benchmark de 21,9 à 28,9 et le pass@8 de 31,9 à 43,2, dépassant les 39,6 d’Opus 4.6 pour un septième du coût. Il creuse aussi l’écart avec des modèles open source 3 à 10 fois plus grands, comme le montre la figure ci-dessous.

Études de cas sur la vérification de code

Bien qu’entraîné principalement pour les mathématiques, Leanstral 1.5 montre de fortes capacités en vérification de code. Nous présentons deux études de cas critiques pour illustrer son impact.

Arbres AVL : prouver la complexité temporelle

Les arbres AVL sont des arbres binaires de recherche auto-équilibrés qui maintiennent une hauteur O(log n) grâce au rééquilibrage lors des insertions et des suppressions. Leanstral 1.5 a prouvé ces garanties de complexité temporelle pour une implémentation réelle — une tâche qui nécessitait une induction structurelle pour refléter la structure récursive de l’arbre, une gestion précise du suivi temporel monadique et une analyse exhaustive des cas pour les chemins de rééquilibrage. Sur plus de 2,7 millions de tokens et 22 compactions, Leanstral a systématiquement déplié chaque couche de la monade TimeM, exposant les calculs sous-jacents malgré leur imbrication avec le flux de contrôle. Il a établi une borne presque serrée de 48 étapes par unité de hauteur, plus une constante pour l’insertion, puis a relié la hauteur à la taille de l’arbre par une relation logarithmique. Il produit ainsi des preuves complètes et vérifiées que l’insertion et la suppression sont bien en O(log n).

Découverte de bugs : trouver les défauts cachés

Pour tester les capacités de Leanstral à détecter les bugs, nous avons construit un pipeline automatisé : Aeneas traduit du code Rust vers Lean, tandis que Leanstral infère l’intention de l’utilisateur et génère des propriétés de correction à partir du code. Leanstral tente ensuite de prouver chaque propriété en quatre tentatives. Si elles échouent toutes, il essaie à la place de prouver la négation, également en quatre tentatives. Sur 57 dépôts testés, ce processus a signalé 47 propriétés violées, dont 11 pointaient vers de vrais bugs — 5 d’entre eux n’avaient jamais été signalés sur GitHub.

L’un de ces bugs se trouvait dans la fonction de signe pour le décodage zigzag de la bibliothèque datrs/varinteger. Avec l’entrée Std.U64.MAX, l’expression (value + 1) débordait, provoquant des plantages en mode debug et une corruption silencieuse en mode version — un cas limite que les tests et le fuzzing manquent généralement. Le pipeline de Leanstral l’a détecté automatiquement, ce qui montre que la vérification formelle peut déjà s’appliquer à des bases de code réelles et trouver des bugs que certaines méthodes traditionnelles laissent passer.

Démarrer

Leanstral 1.5 est sous licence Apache-2.0 . Les poids sont disponibles sur Hugging Face, et le modèle est aussi disponible dès maintenant comme endpoint API gratuit sous le nom leanstral-1-5. Nous recommandons de l’utiliser dans Mistral Vibe. Pour démarrer, récupérez une clé API, puis :

1. Configurer Mistral Vibe

uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup

2. Installer Leanstral 1.5

/leanstall
exit

3. Lancer l’agent

vibe --agent lean

4. Installer Lean LSP MCP (facultatif)

Nous recommandons fortement d’installer Lean LSP MCP en ajoutant ce qui suit à votre ~/.vibe/config.toml

[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600

S’il n’existe aucun serveur MCP, vous devrez peut-être supprimer mcp_servers = [].

5. Commencer à prouver

Demandez à Leanstral de traiter un théorème, de déboguer une preuve ou de contribuer à un dépôt. C’est aussi simple que cela.