Les preuves Lean du code généré par IA s'effondrent après refactoring dans 13 à 27 % des cas

Quand une preuve formelle tient-elle le coup face au refactoring ?

Lorsqu'un modèle de langage écrit du code et y adjoint immédiatement une preuve mathématique formelle de sa correction en Lean, cela semble robuste : le programme fait garantie ce qu'on attend de lui. Mais tous les tests existants ne vérifient la preuve que sur une seule version figée du code. Or, dans le développement réel, le code est constamment réécrit — on extrait une logique répétitive dans une fonction séparée, on change l'ordre des opérations, on inverse des conditions — sans que le comportement du programme change. La question est de savoir si l'ancienne preuve résiste à ce remaniement, même si le sens du code reste identique.

Les auteurs de l'étude ont proposé une méthodologie, RefactorProof, pour mesurer cela. Ils ont pris 185 problèmes du benchmark bien connu VERINA (qui vérifie à la fois le code et les preuves en Lean) et ont appliqué à chaque problème cinq types de réécritures mécaniques, entièrement automatiques : extraction d'un bout de logique dans une fonction séparée, permutation des opérandes dans des opérations commutatives, inversion de conditions, etc. Pour chaque réécriture, on prouvait séparément — via Lean — que le comportement du programme n'avait pas changé. Au total, 458 variantes de code vérifiées ont été obtenues. Ensuite, on appliquait à chaque variante la preuve originale (identique au bit près) et on observait si Lean la considérait toujours valide.

Ce qui s'est révélé fragile, et ce qui a tenu

Les preuves de référence, écrites à la main par les auteurs de VERINA pour 46 problèmes, ont survécu au refactoring presque sans pertes — avec un taux d'échec de seulement 4,3 %. Mais cela ne signifie pas que les preuves manuelles sont intrinsèquement plus fiables : ces 46 problèmes sont les plus simples du benchmark, avec une longueur médiane de code d'une seule ligne, et seulement 6,5 % d'entre eux sont récursifs.

Les preuves générées par des modèles spécialisés dans la démonstration — DeepSeek-Prover-V2-7B et deux versions de Goedel-Prover-V2 (8B et 32B) — ont cassé bien plus souvent : le taux d'échec s'élève à 13,3-26,8 %. Mais si l'on compare les modèles et la référence sur un ensemble de problèmes comparable, le tableau s'inverse : les preuves des modèles survivent plus souvent au refactoring que les preuves de référence — de 15,6 points de pourcentage pour DeepSeek-7B, 18,8 points pour Goedel-32B et 20,3 points pour Goedel-8B. La différence est statistiquement significative dans les trois cas.

Pourquoi certaines preuves s'effondrent et d'autres tiennent

Les chercheurs ont identifié un mécanisme concret de robustesse. Les preuves de référence commencent généralement par la commande `unfold`, qui déploie la définition de la fonction directement dans le texte. Les preuves des modèles, elles, nomment plus souvent explicitement l'appel de fonction et son corps comme égaux via la tactique `rfl` (ce qu'on appelle un « pont définitionnel »), avant de prouver le reste par automatisation.

Lorsque le code est déplacé vers une fonction séparée (extraction de logique), ce « pont » fonctionne nettement mieux : au niveau des problèmes, les preuves avec pont survivent dans 6 cas sur 6, tandis que les autres stratégies ne survivent que dans 6 cas sur 31. Mais cette technique a un revers : si la réécriture modifie substantiellement le corps de la fonction lui-même (et non simplement son emplacement), le pont, lié au texte précis du corps, cesse de se typer correctement — ces preuves ne survivent alors que dans 0 cas sur 3, contre 17 sur 19 pour les preuves plus générales, non liées à une formulation spécifique.

Une rupture n'est pas une catastrophe

La conclusion pratique principale est la suivante : le fait qu'une preuve échoue après un refactoring ne signifie pas forcément une réécriture coûteuse. Les chercheurs ont vérifié cela directement : ils ont pris les preuves cassées et tenté de les réparer avec une seule retouche simple et ciblée — le renommage d'un identifiant. Sur 54 ruptures éligibles de preuves de référence, 51 ont ainsi pu être réparées ; sur 85 ruptures de preuves issues de modèles, 58 l'ont été.

Pour les équipes qui s'appuient sur la génération de code vérifiable par des modèles d'IA, la conclusion est simple : le seul fait qu'une preuve cesse de passer après un refactoring n'est pas une raison de paniquer, ni un indicateur que le modèle est fondamentalement moins bon pour produire des preuves. C'est plutôt un signal indiquant qu'il faudrait intégrer dans le pipeline de vérification une vérification automatique et une réparation légère des preuves après toute modification du code, plutôt que de considérer une rupture comme un verdict définitif sur la qualité du modèle.