Leanstral 1.5 : l’abondance de preuves pour tous
(mistral.ai)- Dans un mouvement visant à rapprocher l’usage de la vérification formelle du travail de développement réel, Mistral AI a publié Leanstral 1.5, un modèle Apache-2.0 pour Lean 4
- Le modèle n’active que 6B paramètres sur 119B paramètres au total, et apprend à la fois la rédaction de preuves et le travail sur des dépôts de code via pré-entraînement intermédiaire, fine-tuning supervisé et apprentissage par renforcement CISPO
- Il atteint 100 % sur miniF2F, 587/672 sur PutnamBench, 87 % sur FATE-H et 34 % sur FATE-X, montrant de solides performances sur les benchmarks de preuves mathématiques et les évaluations d’ingénierie de preuve réelle
- Dans la vérification de code réel, il a prouvé la complexité temporelle en O(log n) des arbres AVL et a trouvé 11 vrais bugs dans 57 dépôts via un pipeline Rust-to-Lean
- Les poids et l’API gratuite
leanstral-1-5sont publiés, ce qui permet de l’appliquer directement à l’ingénierie de preuve pratique, comme la démonstration de théorèmes, le débogage de preuves et les contributions à des dépôts
Publication de Leanstral 1.5 et caractéristiques du modèle
- Leanstral 1.5 est un modèle conçu pour réaliser de l’ingénierie de preuve dans Lean 4
- Sa licence est Apache-2.0, et sa taille est de 119B paramètres au total, dont 6B paramètres actifs
- En améliorant les performances de vérification formelle, il peut être utilisé non seulement sur des benchmarks mathématiques, mais aussi pour vérifier des propriétés de code réel
- Il sature miniF2F, résout 587 des 672 problèmes de PutnamBench et atteint 87 % sur FATE-H et 34 % sur FATE-X
Un entraînement en 3 étapes qui apprend à partir du retour sur les preuves
- L’entraînement se compose de 3 étapes : pré-entraînement intermédiaire, fine-tuning supervisé et apprentissage par renforcement basé sur CISPO
- Deux environnements sont utilisés pour l’apprentissage par renforcement
- Environnement multi-tours : le modèle reçoit un énoncé de théorème, le prouve ou le réfute, puis modifie itérativement la preuve à partir des retours du compilateur Lean
- Si la preuve compile, c’est un succès ; sinon, la boucle continue jusqu’à ce que le problème soit résolu ou que le budget soit épuisé
- Environnement d’agent de code : le modèle modifie des fichiers dans un système de fichiers brut comme un développeur, exécute des commandes bash et consulte en temps réel les objectifs, erreurs et informations de types via le Lean language server
- L’environnement d’agent de code traite des tâches longues, comme compléter des preuves partielles dans un dépôt, écrire des lemmes auxiliaires et poursuivre le travail même après plusieurs compressions de contexte
- La correction finale est vérifiée dans le fork SafeVerify de Mistral, à partir de la liste des théorèmes cibles
Benchmarks de mathématiques et d’ingénierie de preuve
- L’évaluation utilise miniF2F, PutnamBench, FATE-H/FATE-X et FLTEval
- miniF2F est un benchmark de mathématiques formelles couvrant des problèmes élémentaires jusqu’au niveau IMO
- PutnamBench est composé de 672 problèmes de la Putnam Mathematical Competition
- FATE-H et FATE-X sont respectivement des benchmarks d’algèbre abstraite de niveau master/doctorat
- FLTEval évalue la difficulté d’ingénierie de preuve à partir de vraies pull requests du dépôt de Fermat’s Last Theorem
- Sur miniF2F, il atteint 100 % à la fois sur l’ensemble de validation et l’ensemble de test
- Sur PutnamBench et FATE-H/X, il est comparé à Goedel-Architect, Seed-Prover 1.5 high et AxProverBase sans guide de preuve en langage naturel
- Performances FATE-H/X :
- FATE-H atteint 87 % et FATE-X 34 %, établissant un nouveau meilleur niveau de performance
- Sur PutnamBench, il résout 7 problèmes de plus que Seed-Prover 1.5 high, pour un coût d’environ 4 dollars par problème
- La configuration high de Seed-Prover utilise un budget de 10 H20-days par problème, pour un coût estimé à plus de 300 dollars
- Certains prouveurs mieux classés reçoivent un guide de preuve en langage naturel ou fonctionnent dans d’autres conditions, comme Aleph Prover, qui coûte 54 à 68 dollars par problème
Passage à l’échelle avec de longs budgets de raisonnement et FLTEval
- Sur PutnamBench, les performances Pass@8 de Leanstral 1.5 augmentent de façon fluide et monotone à mesure que le budget de tokens augmente
- Dans une expérience où le budget de tokens par tentative passe de 25k à 4M, le nombre de problèmes résolus augmente comme suit
- 50k tokens : 44 problèmes
- 200k tokens : 244 problèmes
- 1M tokens : 493 problèmes
- 4M tokens : 587 problèmes
- Le fait de poursuivre le raisonnement, l’édition de fichiers et les corrections sur des millions de tokens sans s’interrompre dans les longues preuves se traduit par de meilleures performances
- FLTEval est également publié entièrement en open source
- Sur FLTEval, Leanstral 1.5 fait passer le pass@1 de 21,9 à 28,9, et le pass@8 de 31,9 à 43,2
- Un pass@8 de 43,2 dépasse les 39,6 d’Opus 4.6, avec un coût 7 fois inférieur
- Il affiche aussi de meilleures performances que des modèles open source 3 à 10 fois plus grands
Cas de vérification de code réel
-
Preuve de complexité temporelle des arbres AVL
- Un arbre AVL est un arbre binaire de recherche auto-équilibré qui maintient une hauteur en O(log n) grâce au rééquilibrage lors des insertions et suppressions
- Leanstral 1.5 vérifie que les insertions et suppressions sont en O(log n) dans une implémentation réelle
- Cette tâche nécessite une induction structurelle reflétant la structure récursive de l’arbre, le traitement du suivi temporel basé sur une monade, et une analyse exhaustive des cas sur les chemins de rééquilibrage
- La preuve se déroule sur plus de 2,7 millions de tokens et 22 compressions de contexte
- Leanstral déplie systématiquement chaque couche de la monade TimeM pour faire apparaître les calculs mêlés au flot de contrôle
- Pour l’insertion, il établit une borne de 48 étapes par unité de hauteur, proche d’un terme constant, puis relie la hauteur et la taille de l’arbre par une relation logarithmique
-
Trouver des bugs dans du code Rust
- L’expérience de détection de bugs repose sur un pipeline où Aeneas convertit le code Rust en Lean, puis Leanstral infère l’intention utilisateur à partir du code et génère des propriétés de cohérence
- Leanstral tente de prouver chaque propriété 4 fois, et si toutes échouent, tente ensuite de prouver sa négation 4 fois
- Dans 57 dépôts, 47 propriétés violées sont signalées, dont 11 pointent vers de vrais bugs
- Parmi ces vrais bugs, 5 n’avaient pas été signalés auparavant sur GitHub
- Un cas a été trouvé dans la fonction de signe du décodage zigzag de la bibliothèque datrs/varinteger
- Lorsque l’entrée vaut
Std.U64.MAX, l’expression(value + 1)déborde - En mode debug, cela provoque un crash ; en mode release, une corruption silencieuse des données
- Ce cas limite est typiquement difficile à détecter par les tests et le fuzzing classiques
Publication et mode d’emploi
- Les poids sont publiés sur Hugging Face
- L’endpoint d’API gratuit est fourni dans la model card sous le nom
leanstral-1-5 - Mistral Vibe est recommandé comme environnement d’utilisation
- La procédure de démarrage consiste à configurer Mistral Vibe, installer Leanstral 1.5, exécuter l’agent, installer éventuellement Lean LSP MCP, puis commencer les tâches de preuve
- Il est recommandé d’installer Lean LSP MCP en l’ajoutant à
~/.vibe/config.toml - S’il n’existe pas de serveur MCP, il peut être nécessaire de supprimer
mcp_servers = [] - Leanstral peut être utilisé pour résoudre des théorèmes, déboguer des preuves et contribuer à des dépôts
1 commentaires
Commentaires sur Hacker News
La critique selon laquelle Mistral aurait du mal à rivaliser avec les grands modèles est valable, mais en réalité, je pense qu’ils se concentrent sur la fourniture de fonctionnalités spécifiques de haute qualité dans de petits modèles.
J’utilise Mistral pour des tâches comme l’OCR ou l’analyse de fichiers ; avec 100 dollars sur mon compte, ça tourne pendant un an sans que j’aie à me soucier du volume de requêtes.
Le coût est tellement faible que, même si cela ne rivalise pas avec Opus 4.8, cela a largement de la valeur.
Une qualité correcte à bas prix ressemble davantage à une niche que de payer 10 fois plus cher plus tard pour obtenir la meilleure qualité et réduire les erreurs.
L’OCR est déjà presque devenu une commodité, et il est proposé de base par des modèles open source ou par des acteurs comme AWS.
De plus, avec un tarif annuel de 100 dollars, il est difficile de créer de la fidélité ; il n’y a pas non plus de coût de migration, donc si un prix plus bas apparaît, les clients peuvent partir immédiatement.
Sans verrouillage client sur un outil bon marché facilement réplicable, on est plus proche d’une fonctionnalité que d’une entreprise.
C’est bien pour les acheteurs, mais si l’on veut qu’une entreprise européenne rivalise à long terme avec des concurrents mondiaux sur les capacités produit, cela ressemble à une mauvaise stratégie.
Le travail en lui-même est bon, mais l’exemple de bug trouvé m’a semblé étrange.
Ils disent que, dans la fonction sign du décodage zigzag, avec
Std.U64.MAXen entrée,(value + 1)déborde, ce qui provoque un crash en mode debug et une corruption silencieuse en mode release ; je ne sais pas si l’on peut vraiment appeler cela un cas limite que les tests « ratent généralement ».De mauvais tests le rateraient, mais une personne prudente ou un système de codage basé sur le machine learning sait assez bien qu’il faut « tester les valeurs extrêmes ». Surtout s’il s’agit de code qui parse des entrées utilisateur.
Je me demande s’ils avaient trouvé un bug plus intéressant, mais difficile à expliquer rapidement, et ont donc utilisé cet exemple.
Pour ce genre de bibliothèque d’encodage, le fuzzing serait une attente de base pour du code correct, et il l’aurait presque certainement trouvé en quelques secondes.
En pratique, j’ai créé un test aller-retour très simple avec
proptest, et en moins d’une seconde j’ai obtenu des dizaines d’échecs ainsi que le résultat ci-dessous :thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:Test failed: attempt to multiply with overflow.minimal failing input: value = 4611686018427387904successes: 2local rejects: 0global rejects: 0L’avantage de Lean apparaît bien : il réduit le besoin de choisir intelligemment les exemples à tester.
Ça me rend curieux du parcours des auteurs.
Tous les systèmes de tests basés sur les propriétés inventés vers 1980 explorent les valeurs limites.
Les tests réels peuvent être difficiles à cause de la sémantique de C et C++, ou de son absence. Le compilateur a en effet le droit de considérer comme « tests réussis » toutes les entrées menant à un comportement indéfini.
Au milieu de l’article, il y a plusieurs comparaisons avec des LLM de pointe, mais ce sont tous des modèles d’il y a six mois.
Ça m’a fait rire : on dirait « notre nouveau modèle est meilleur que des modèles chinois vieux de trois générations ».
La bibliothèque en question est https://github.com/datrs/varinteger.
Le même problème avait déjà été signalé dans ce dépôt une semaine avant la publication de l’article, donc c’est probablement bien celle-là : https://github.com/datrs/varinteger/issues/8
Je ne sais pas si cette personne est employée de Leanstral, ou si Leanstral a simplement repris cette issue.
Cette bibliothèque est petite, ses tests sont étonnamment faibles, et elle n’a quasiment pas été touchée depuis 8 ans : https://github.com/datrs/varinteger/blob/master/tests/test.r...
Les téléchargements semblent assez faibles, autour de 1 000 par jour : https://crates.io/crates/varinteger
Il est donc difficile d’y voir une réussite assez impressionnante pour être présentée comme l’unique exemple. La détection automatique est bien utile, mais je ne suis pas sûr que ce soit un résultat remarquable dans ce sous-domaine.
Je n’ai jamais utilisé de LLM de rédaction de preuves, mais comme les données d’entraînement sont plutôt rares, je ne serais pas surpris qu’ils soient plus bruts que les modèles de codage généralistes.
À noter que https://crates.io/crates/varinteger indique https://github.com/mafintosh/varinteger-rs, mais comme cette adresse redirige vers https://github.com/datrs/varinteger, il semble s’agir de la même bibliothèque malgré les apparences.
Le point essentiel n’est pas de trouver des bugs, mais de prouver que certains types de bugs sont absents sous certaines hypothèses.
Mais cette histoire est difficile à vendre, donc le marketing glisse souvent vers « nous avons trouvé ce bug ».
Cela peut-il être utile même à quelqu’un qui ne connaît pas du tout Lean ? Je veux vérifier un logiciel sur lequel je travaille, mais je n’ai aucune expérience en vérification formelle
Je me demande si l’on peut obtenir des résultats exploitables avec seulement la spécification, le code et un temps d’apprentissage limité
C’est moins proche des mathématiques que de la lecture de types Haskell, avec surtout beaucoup de vocabulaire emprunté aux maths
On pourrait aussi obtenir de l’aide, par la conversation, pour écrire du code Lean destiné à vérifier une application, mais je n’en suis pas certain
Sinon, on ne peut pas valider la sortie
On a peut-être prouvé une proposition vérifiée comme mécaniquement correcte, mais si l’on ne sait pas ce que signifie cette proposition, ni si elle couvre réellement ce que l’on voulait vérifier, cela n’a pas de sens
C’est étonnant de voir à quel point les modèles sont systématiquement à l’aise avec Lean4. Pas seulement les modèles de pointe, mais aussi de petits modèles locaux ; les LLM semblent tout simplement bien comprendre Lean4
Il me reste encore du chemin avant de pouvoir me dire expert Lean4, mais je n’ai désormais plus absolument besoin d’assistance pour créer des programmes utiles
Le fait de pouvoir faire confiance à des parties que l’on ne comprend pas entièrement, même avec très peu de connaissances au départ, accélère énormément l’apprentissage. Obtenir des programmes sur lesquels on peut s’appuyer malgré une connaissance imparfaite est pratique et motivant
J’ai l’impression que la limite n’est pas tant l’ensemble des étapes intermédiaires de la preuve, mais plutôt la partie du langage qui décrit ses propres axiomes et l’interface des propositions. Avec le temps, il faudra comprendre davantage pour faire davantage, mais, d’une certaine manière, on peut travailler en sécurité au niveau N+1
Lean4 est aussi un langage de programmation agréable indépendamment de son rôle de prouveur de théorèmes, et il est étonnamment rapide
Je l’utilise avec
io_uring, et dans beaucoup de cas il est nettement plus rapide que C++/libuv ou Rust/TokioParfois, quand on observe une grosse queue sur des métriques comme la latence p99.99, il faut faire du tuning, par exemple passer les nombres en largeur fixe, mais C++ et Rust nécessitent aussi du tuning
Il est intéressant de voir Lean 4 mis en avant pour la vérification formelle
Je pensais que ce domaine relevait plutôt d’Isabelle/HOL et de TLA+
J’aurais au moins pensé qu’on entraînerait un modèle à utiliser les trois. Isabelle/Isar me semble aussi meilleur pour les dérivations directes en algèbre linéaire ; quelqu’un peut-il l’expliquer ?
Dans ce domaine, même Agda a été davantage utilisé
Cela dit, Lean gagne actuellement beaucoup d’élan comme alternative, notamment grâce à ses capacités de langage de programmation fonctionnel généraliste
Personnellement, je trouve plus pratiques les approches fondées sur la logique de Hoare ou la logique de séparation, qui facilitent l’alignement entre exigences et spécifications. J’aime bien Dafny et F*
J’ai trouvé amusant que les développeurs fassent une allusion discrète à Le Chaton Fat dans l’annonce sur Twitter
Qu’ils aient réellement été impliqués ou non dans Le Chaton Fat, on dirait bien qu’un vrai « nouveau grand modèle généraliste » arrive bientôt
Ils l’ont mentionné directement même après l’agitation médiatique, donc c’est prometteur. J’espère que le nom sera plus créatif que « Large 4 »
On peut essayer Leanstral 1.5 dans la dernière version d’OpenATP
OpenATP est un package Python open source et une CLI pour les prouveurs automatiques de théorèmes agentiques ; il prend en charge nativement l’exécution locale dans Docker ou l’exécution distante dans un sandbox Modal
GitHub : https://github.com/henryrobbins/open-atp
Docs : https://open-atp.henryrobbins.com