AlphaProof Code vs MathForm-8B : deux étapes d’un même pipeline Lean, pas deux rivaux

Lisez attentivement l’article AlphaProof Code et un chiffre saute aux yeux, que l’annonce ne met pas en avant : sur les quatre semaines que les cinq chercheurs de DeepMind ont passées à vérifier Signal, la partie qui ne pouvait pas être automatisée était le front. Des experts humains ont travaillé avec un mélange de modèles pour traduire les objectifs de sécurité de Signal en spécifications formelles Lean, et un expert a examiné chacune d’entre elles avant que le moindre travail de preuve ne commence. C’est là le goulot d’étranglement. MathForm-8B, le modèle d’autoformalisation à 8 milliards de paramètres d’OpenBMB publié sur Hugging Face le 14 août 2026, est une tentative directe d’automatiser précisément cette étape — prendre un énoncé mathématique en langage naturel et produire un énoncé de théorème Lean 4 prêt à être démontré par quelqu’un d’autre. Mettez-les côte à côte : vous ne comparez pas deux produits. Vous regardez deux étapes consécutives d’un même pipeline, séparées par la différence entre les mathématiques et la sécurité des protocoles.

Le pipeline, dans l’ordre où le travail se déroule

La vérification formelle de logiciels réels comporte trois tâches. Premièrement, déterminer ce qui doit être vrai et l’écrire dans un langage formel. Deuxièmement, prouver que l’implémentation le satisfait. Troisièmement, vérifier les preuves mécaniquement, car une preuve erronée est pire que pas de preuve.

MathForm-8B accomplit la première tâche, pour une classe d'entrées étroite : des énoncés mathématiques de style manuel. Donnez-lui « pour tout nombre réel x, x² est positif ou nul » et il renvoie les imports, les types et un en-tête de théorème en Lean 4. Ce qu'il ne renvoie pas, c'est une preuve, et ses auteurs disent explicitement que la recherche de preuve est le problème de quelqu'un d'autre. Ses chiffres rapportés, tous rapportés par le fournisseur et non reproduits, sont 88,06 % de Pass@8 moyen selon un contrôle syntaxique et 72,37 % selon le contrôle de cohérence plus strict sur six benchmarks — l'écart entre ces deux chiffres est la mesure honnête de la fréquence à laquelle un énoncé syntaxiquement valide signifie autre chose que ce qui a été demandé.

AlphaProof Code s'acquitte des tâches deux et trois, ainsi que d'une étape de spécification que MathForm-8B ne pouvait pas aborder. Les objectifs de sécurité de Signal ne sont pas des affirmations mathématiques au sens où MathForm a été entraîné ; ce sont des énoncés concernant un protocole — que les messages restent protégés avant et après qu'un appareil est temporairement compromis, que l'initiateur et le répondeur sont bien ceux qu'ils prétendent être. Les transformer en Lean exigeait une expertise protocolaire qu'aucun autoformaliseur 8B ne possède. Une fois la spécification établie, le travail de preuve a été entièrement confié à des agents, et la vérification a été confiée au noyau de Lean ainsi qu'à un agent gardien utilisant un comparateur par rapport à une copie de spécification gardée à part.

Ce que chacun vous coûte réellement à utiliser

• Poids — MathForm-8B : téléchargeables, Apache 2.0, quatre shards safetensors en BF16, affinés à partir de Qwen3-8B. AlphaProof Code : aucun. La publication est constituée d'un développement Lean, d'une sémantique AArch64 et d'une liaison libsignal à github.com/google-deepmind/code-verification.

• L'exécuter — MathForm-8B : Transformers, vLLM ou SGLang, tous exposant un point de terminaison compatible OpenAI, sur du matériel que vous possédez. AlphaProof Code : pas de point de terminaison, pas d'API, pas de liste d'attente, pas de prix ; c'est un cadre de recherche dont DeepMind affirme qu'il nécessite des « recherches continues » avant de passer à l'échelle.

• Entrée — MathForm-8B : un énoncé mathématique en langage naturel. AlphaProof Code : une spécification formelle, plus le binaire dont vous voulez prouver la conformité à celle-ci.

• Sortie — MathForm-8B : un énoncé de théorème Lean 4, non prouvé. AlphaProof Code : une preuve vérifiée par machine, ou une réfutation lorsque le code est défectueux.

• Revue humaine — MathForm-8B : vous relisez l’énoncé émis et, avec 72,37 % de cohérence, vous en relirez beaucoup. AlphaProof Code : des experts examinent chaque spécification avant le début du travail de preuve, puis les agents signalent environ 1 % de la base de code pour un second examen.

• Limites connues — MathForm-8B : uniquement des énoncés mathématiques, pas de génération de preuves, et le dépôt de code lié dans son README était encore un espace réservé au moment de la publication. AlphaProof Code : aucune garantie post-quantique pour la réparation SPQR, aucune confidentialité de la charge utile, une session par promotion, et une borne de falsification MAC qui devient vide près de 25 000 messages dans une session unique.

L'écart que MathForm-8B devrait combler

Il est tentant de dire qu’un auto-formaliseur aurait pu écrire les spécifications de Signal et épargner aux chercheurs leurs semaines de travail en amont. Le récit de l’article lui-même dit le contraire, et la raison est précise. La spécification d’un protocole n’est pas une reformulation d’une affirmation ; c’est un choix concernant le modèle d’adversaire. Le travail sur Signal comporte un volet symbolique dans le cadre de Dolev–Yao avec un attaquant quantique qui casse Diffie–Hellman après la poignée de main, et un volet calculatoire avec des adversaires classiques et une borne concrète. Ces deux volets énoncent des théorèmes différents à propos du même code, et choisir entre eux est une décision d’ingénierie aux conséquences de sécurité. Aucun modèle entraîné à transformer « montrer que x² ≥ 0 » en Lean ne va prendre cette décision.

Ce qu’un autoformaliseur pourrait vraisemblablement faire, c’est la partie mécanique de ce travail : étant donné un objectif de sécurité en prose et une bibliothèque de définitions Lean existantes, produire une première ébauche de l’énoncé dans l’idiome propre au projet, pour qu’un expert la corrige. C’est un gain réel, et bien plus modeste que ne le suggère le titre. L’article rapporte un catalogue d’écarts par rapport aux spécifications de plus de 200 entrées computationnelles et d’environ 35 entrées symboliques — dont quinze lacunes ou bogues dans l’analyse de Double Ratchet —, ce qui correspond à ce qu’a trouvé l’étape de revue humaine. Un modèle qui rédige des énoncés devrait être évalué à l’aune de ce catalogue, et non d’un score Pass@8 sur des benchmarks mathématiques.

Lorsque les deux nombres ne sont pas du tout comparables

MathForm-8B avec 88,06 % et AlphaProof Code avec 6,5 millions de lignes mesurent des choses différentes et ne devraient jamais être placés dans la même colonne. L’un est un taux de réussite sur une suite d’évaluation construite par les auteurs ; l’autre est une quantité de preuves produites pour une seule cible. L’éditeur reconnaît franchement que les 88,06 % reposent sur un contrôle syntaxique, qui est un critère faible — une affirmation peut compiler et formaliser malgré tout une assertion erronée, ce qui explique pourquoi le chiffre de cohérence est inférieur de 16 points.

Le chiffre d'AlphaProof Code d'une saveur comparable est le travail de validation : deux bugs Signal précédemment corrigés, un bug d'état faible et un bug de petit sous-groupe, ont été réintroduits dans une copie isolée, et dans les deux cas le système a produit une preuve vérifiée par machine que la version buguée échoue au théorème de sécurité. C'est un test négatif, et un test négatif est ce qui manque entièrement à un benchmark d'autoformaliseur. MathForm-8B ne rapporte aucun résultat de la forme « étant donné un énoncé délibérément erroné, le modèle l'a dit ».

Comment vous les utiliseriez réellement ensemble

Concrètement, et c'est le seul volet de la comparaison qui dispose d'une voie à court terme : utiliser un autoformaliseur pour rédiger une ébauche, un modèle généraliste performant pour critiquer cette ébauche, et un agent de preuve pour tenter la démonstration. Chaque étape a un mode de défaillance différent, et faire passer les trois par une seule clé constitue le compromis pratique. Sur OrcaRouter, plus de 200 modèles sont accessibles derrière une seule API au prix catalogue des fournisseurs, avec 0 % de marge, de sorte qu'une boucle de rédaction de spécifications qui envoie le même énoncé à deux modèles et compare leurs sorties Lean est un simple appel à un DSL de routage, plutôt que trois contrats et trois SDK. Le basculement automatique en cas de défaillance couvre le cas où le modèle que vous avez choisi passe un mauvais moment.

Ce que rien de tout cela ne fournit, c’est la garantie. MathForm-8B vous donne un énoncé, les modèles vous donnent une critique, et quelque chose doit encore le prouver. À l’heure actuelle, le seul système publié qui ferme cette boucle sur du code réellement déployé est AlphaProof Code, et il n’est pas à vendre.

La raison de lire les deux articles plutôt que de désigner un vainqueur

MathForm-8B est un artefact utile avec une tâche étroite et un plafond de précision réel et mesuré. AlphaProof Code est une démonstration de flux de travail dont le constat le plus transposable n'est pas le volume de preuves mais la répartition : le travail de spécification appelle des humains et un modèle général puissant, le travail de preuve appelle des équipes d'agents et un noyau, et la frontière entre les deux est là où réside toute la difficulté. Quiconque construit un pipeline de vérification devrait prendre cette répartition au sérieux et considérer l'autoformalisation comme la pièce qui réduit le coût de la première étape — et non comme celle qui la remplace.

Le résumé honnête pour une équipe qui décide quoi télécharger ce mois-ci : MathForm-8B, oui, si vous travaillez avec Lean et voulez une aide à la rédaction. AlphaProof Code, lisez le dépôt d’artefacts et le catalogue des écarts par rapport aux spécifications, car le catalogue vous en dit plus sur ce que la vérification formelle du code de production ne peut toujours pas atteindre que ne le fera jamais n’importe quelle annonce.