RefactorProof : les preuves des LLM cèdent après un refactoring du code

Les benchmarks de génération de code vérifiable testent généralement la preuve sur une seule implémentation figée. Les auteurs de RefactorProof ont voulu savoir ce qui se passe quand on réécrit l'implémentation en conservant son comportement. À partir des 185 tâches de VERINA qui compilent dans leur environnement figé, ils ont construit 458 variantes certifiées par Lean. La spécification et la preuve vérifiable n'ont pas changé d'un seul octet. Résultat : sur les refactorings structurels, les preuves cessent massivement de passer la vérification. Pour les preuves de référence de VERINA, la part de preuves survivantes (task-normalized structural PSR) s'élève à 4,3%, et à 13,3–26,8% pour les prouveurs LLM spécialisés.

Comment fonctionne le test de fragilité

L'idée est simple et brutale. Une preuve formelle est liée au texte précis du programme : noms, ordre des définitions, structure des expressions. Si un développeur extrait une fonction, change la forme d'un calcul ou renomme une variable, rien ne change sur le plan logique, mais la preuve Lean peut ne plus se construire. En développement réel, le refactoring est permanent : la question de savoir si une preuve survit à une modification est donc d'ordre pratique.

VERINA ne fournit des preuves de référence que pour 46 tâches, toutes issues du split de base. Les auteurs construisent donc leurs principales comparaisons entre modèles et références sur 21–25 tâches courtes et non récursives, choisies pour que tous les participants partent sur un terrain commun. L'échantillon est étroit, et la portée des conclusions doit se lire à cette aune.

Les machines sont fragiles, mais les humains le sont davantage

Retournement inattendu : les preuves des modèles se révèlent plus robustes que les preuves de référence. Sur les tâches comparables, la part globale de preuves survivantes non modifiées est plus élevée pour les modèles que pour les artefacts de VERINA. Les intervalles de confiance à 95% n'incluent pas zéro pour les trois modèles.

• DeepSeek-Prover-V2-7B : +15,6 points par rapport à la référence
• Goedel-Prover-V2-32B : +18,8 points
• Goedel-Prover-V2-8B : +20,3 points

L'ordre se maintient lorsqu'on exclut les variantes T1, que toutes les preuves sans exception survivent, lorsqu'on agrège en équilibrant les familles de refactorings, et avec d'autres règles de sélection de la preuve valide applicables en pratique. La cause probable : les preuves de référence sont écrites pour une forme de code précise et lui sont étroitement liées, tandis que les modèles produisent plus souvent des preuves plus directes, moins dépendantes des détails de construction. Il s'agit d'une hypothèse : les auteurs ne démontrent pas ce mécanisme.

Cassé ne veut pas dire coûteux à réparer

La principale réserve de l'article concerne le coût d'une casse. Des corrections prédéfinies d'un seul identifiant réparent 51 des 54 échecs structurels éligibles des preuves de référence et 58 des 85 échecs éligibles des preuves de modèles. Autrement dit, l'essentiel de la « fragilité » disparaît avec une correction peu coûteuse, et presque tout se répare pour les références. Pour les modèles, le tableau est moins favorable : environ 68% contre 94%.

RefactorProof mesure donc précisément la stabilité d'une preuve non modifiée face au refactoring. Il n'évalue pas le coût de maintenance d'une preuve après sa casse, et les auteurs le soulignent explicitement.

Paramètres clés de l'étude

• Benchmark : RefactorProof, dérivé de VERINA
• Tâches sources : 185 (compilent dans l'environnement Lean figé)
• Variantes certifiées : 458
• Preuves de référence de VERINA : 46 tâches, split de base uniquement
• Échantillon comparable : 21–25 tâches courtes et non récursives
• PSR structurel des preuves de référence : 4,3%
• PSR structurel des prouveurs spécialisés : 13,3–26,8%
• Modèles testés : DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B
• Réparation par correction d'un seul identifiant : 51/54 pour les références, 58/85 pour les modèles
• Publication : NeurIPS 2026 Workshop on AI for Verifiable Coding ; catégories cs.AI, cs.LO, cs.SE

Ce qu'il faut changer en pratique

Les équipes qui construisent des pipelines du type « le LLM écrit le code et la preuve, Lean vérifie » reçoivent un signal clair : une vérification sur une seule implémentation figée surestime la fiabilité. Ajoutez à la CI des variantes refactorées du programme et exécutez la preuve contre elles. Si la preuve échoue, essayez d'abord des corrections automatiques peu coûteuses sur les identifiants : d'après les données de l'étude, elles couvrent une part importante des cas.

Pour évaluer des modèles prouveurs, ne regardez pas seulement la part de tâches résolues, mais aussi la survie des preuves lorsque le code change. Pour les auteurs de benchmarks, la conclusion est tout aussi directe : il faut mesurer à la fois la stabilité et le coût de réparation. Ce second indicateur n'existe pas encore dans RefactorProof.