💻 computer science

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

L'article présente VeriScale, un cadre adversarial qui étend et distille des suites de tests pour créer des benchmarks plus rigoureux tels que VerinaPlus et VerinaLite, lesquels révèlent des faiblesses significatives dans les capacités de génération de code et de spécification des LLMs les plus avancés, faiblesses que les benchmarks existants ne parviennent pas à détecter.

Auteurs originaux : Yifan Bai, Xiaoyang Liu, Zihao Mou, Guihong Wang, Jian Yu, Shuhan Xie, Yantao Li, Yangyu Zhang, Jingwei Liang, Tao Luo

Publié 2026-05-22

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yifan Bai, Xiaoyang Liu, Zihao Mou, Guihong Wang, Jian Yu, Shuhan Xie, Yantao Li, Yangyu Zhang, Jingwei Liang, Tao Luo

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous embauchiez un chef robot pour préparer un repas complexe. Vous donnez au robot une recette (la « spécification ») et lui demandez de préparer le plat (le « code »). Pour vérifier si le robot est compétent, vous goûtez la nourriture.

Le Problème : Le Piège du « Quiz Facile »
Actuellement, les tests que nous utilisons pour évaluer ces chefs IA ressemblent à un quiz très facile. Nous ne leur donnons que quelques ingrédients simples (comme du « sel » et de l'« eau ») et demandons un résultat simple (« soupe »). Si le robot prépare de la soupe, nous lui attribuons un A+.

Mais voici le piège : le robot pourrait tricher. Il pourrait avoir mémorisé la réponse pour « sel + eau = soupe », mais si vous lui donnez un ingrédient bizarre comme du « dentifrice », il pourrait quand même essayer de faire de la soupe et affirmer que c'est correct. Ou alors, il pourrait écrire une recette disant « ajouter du sel », mais oublier de préciser « ne pas ajouter de poison ». Comme le test n'incluait ni « dentifrice » ni « poison », le robot réussit, même s'il est en réalité dangereux ou défectueux.

L'article soutient que les tests actuels sont trop limités et trop faciles, donnant à l'IA une apparence plus intelligente qu'elle ne l'est réellement.

La Solution : VeriScale (Le Cadre de « Test de Stress »)
Les auteurs ont créé un nouveau système appelé VeriScale. Imaginez cela comme un « test de stress » ou un exercice de « Red Team » pour le code de l'IA. Au lieu de simplement demander à l'IA de préparer de la soupe, VeriScale tente de piéger l'IA pour qu'elle échoue.

Il fonctionne en deux étapes principales :

Étape 1 : Le « Parcours du Combattant » (Expansion)

D'abord, VeriScale crée un parcours du combattant massif et chaotique d'ingrédients.

La Graine : Il commence avec des ingrédients normaux.
La Mutation : Il utilise une « machine de mutation » pour tordre et transformer ces ingrédients. Il transforme une tasse d'eau en un seau de glace, ou une pincée de sel en une montagne de sel. Il crée des scénarios étranges et limites que l'IA n'a jamais rencontrés.
Le Chef « Tricheur » (Synthèse Adversaire) : C'est la partie ingénieuse. VeriScale demande à une autre IA, très intelligente, d'agir en tant que « Tricheur ». Ce Tricheur tente d'écrire une fausse recette qui semble respecter les règles mais produit en réalité des déchets.
- Exemple : Si la règle est « La soupe doit être chaude », le Tricheur pourrait écrire une recette qui produit de la « Glace » mais affirme : « Eh bien, techniquement, la glace est un aliment, donc j'ai suivi la règle ! »
- VeriScale exécute ces recettes de Tricheur contre les règles de l'IA. Si les règles de l'IA acceptent la Glace comme « Soupe Chaude », VeriScale détecte le défaut. Il génère une longue liste de ces moments « pris la main dans le sac ».

Étape 2 : La « Liste de Contrôle Essentielle » (Réduction)

Maintenant, VeriScale possède des milliers de ces cas de test astucieux. Les exécuter tous sur chaque IA prendrait une éternité et coûterait une fortune. Il effectue donc une « Réduction ».

Il se demande : « Parmi ces 1 000 astuces, lesquelles sont les plus importantes ? »
Il conserve les astuces spécifiques qui détectent le plus d'erreurs et élimine celles qui sont de simples répétitions.
Le résultat est un test compact et ultra-défiant, assez petit pour être exécuté rapidement, mais qui détecte toujours chaque défaut que la liste massive aurait trouvé.

Les Résultats : Le « Sérum de Vérité »
Les auteurs ont testé ce nouveau système sur les meilleurs modèles d'IA disponibles (comme GPT-5.5 et autres).

L'Ancien Test : Les IA ont obtenu des scores comme 96 % ou 98 %. Elles semblaient être des génies.
Le Test VeriScale : Lorsqu'elles ont été soumises au test de stress, les scores ont chuté drastiquement. Le score d'un modèle de premier plan est passé de 96 % à 86 % pour le codage, et de 68 % à 44 % pour la rédaction des règles (spécifications).

La Grande Conclusion
L'article montre que les anciens tests nous mentaient. Ils surestimaient la capacité de l'IA à écrire du code sûr et correct. Les nouveaux tests « VeriScale » révèlent que, si l'IA est excellente pour écrire du code qui semble correct, elle est toujours très mauvaise pour écrire des règles qui détectent chaque erreur possible.

Ils ont également publié deux versions de ce nouveau test :

VERINAPLUS : Le test de stress massif et complet (83 fois plus grand que l'original).
VERINALITE : La version « légère ». Elle est 14 fois plus grande que l'original mais utilise l'astuce de « Réduction » pour être rapide et peu coûteuse, tout en détectant les mêmes erreurs.

En résumé : VeriScale est un outil qui nous empêche d'être dupes par une IA qui ne sait que réussir des tests faciles. Il force l'IA à prouver qu'elle peut gérer le monde réel, étrange, désordonné et piégeant.

Résumé technique : VeriScale : Mise à l'échelle de suites de tests adverses pour la génération de code vérifiable

Énoncé du problème

Alors que les grands modèles de langage (LLM) sont de plus en plus déployés pour l'ingénierie logicielle, l'évaluation de leur capacité à générer non seulement du code fonctionnel, mais aussi des spécifications et des preuves formellement vérifiables, est devenue cruciale. Les benchmarks existants pour la génération de code vérifiable, tels que VERINA et CLEVER, reposent fortement sur l'évaluation par suite de tests pour évaluer la génération de spécifications (SpecGen) et la génération de code (CodeGen). Cependant, ces benchmarks souffrent d'une limitation fondamentale : ils sont contraints par une pénurie de cas de tests de haute qualité, en particulier de cas de tests négatifs (entrées inattendues et sorties inattendues).

Les benchmarks actuels fournissent généralement un nombre limité de paires entrée-sortie positives. Par conséquent, les modèles peuvent atteindre des taux de réussite gonflés en satisfaisant ces tests épars sans véritablement capturer l'intention du programme ni assurer la validité et l'exhaustivité de leurs spécifications générées. Cela conduit à une surestimation des capacités des modèles, où des implémentations incorrectes ou des spécifications non valides passent l'évaluation simplement parce que la suite de tests échoue à révéler des défauts logiques ou des violations de limites.

Méthodologie : Le cadre VeriScale

Pour remédier à ces limitations, les auteurs proposent VeriScale, un nouveau cadre piloté par des implémentations adverses pour mettre systématiquement à l'échelle et affiner les suites de tests pour la génération de code vérifiable. Le cadre fonctionne en deux étapes principales : l'expansion de la suite de tests et la réduction de la suite de tests.

1. Expansion de la suite de tests

L'objectif de cette étape est de construire un ensemble diversifié et difficile de cas de tests, incluant des paires entrée-sortie attendues, des entrées inattendues et des sorties inattendues.

Génération de graines et mutation consciente des types : S'inspirant d'EvalPlus, VeriScale utilise des LLM pour synthétiser des entrées de graines initiales. Ces graines sont ensuite étendues via une stratégie de mutation itérative et consciente des types. Le cadre formalise la mutation comme un processus à cinq éléments ( $M = (T, D, O, p, q)$ ) qui préserve les types d'entrée tout en introduisant des perturbations structurelles. Cela inclut la réutilisation de valeurs contextuelles depuis un « pool d'ingrédients » ou l'application d'heuristiques spécifiques aux types pour générer des cas limites complexes.
Classification des entrées guidée par les préconditions : Les entrées candidates sont rigoureusement classées par rapport aux préconditions de vérité terrain en utilisant un pipeline de vérification en deux étapes dans Lean.
- Filtre syntaxique : S'assure que les candidats sont des expressions Lean syntaxiquement valides.
- Vérification bidirectionnelle : Utilise #guard decide et une recherche de preuve plausible pour classer les entrées comme « attendues » (satisfaisant la précondition) ou « inattendues » (la violant).
Synthèse adverse de sorties inattendues : C'est l'innovation centrale. Au lieu de s'appuyer sur des LLM pour halluciner des sorties incorrectes aléatoires, VeriScale synthétise des implémentations adverses.
- Un modèle capable agit comme une « équipe rouge », générant des spécifications formelles pour un problème.
- Un autre modèle (ou le même dans un rôle différent) tente de concevoir des implémentations adverses destinées à exploiter les faiblesses de ces spécifications.
- Ces implémentations sont exécutées sur des entrées attendues. Si une implémentation adverse produit une sortie qui diffère de la vérité terrain mais qui est faussement acceptée par les postconditions générées, cette sortie est conservée comme une « sortie inattendue » de haute qualité. Ce processus garantit que les cas de tests sont véritablement informatifs pour révéler l'invalidité des spécifications.

2. Réduction de la suite de tests

Pour gérer le coût computationnel des suites étendues, VeriScale emploie des stratégies de réduction pour distiller le grand ensemble en des suites compactes mais discriminatives.

Réduction préservant les limites (pour les entrées inattendues) : Au lieu d'un échantillonnage aléatoire, cette stratégie privilégie les entrées correspondant à des violations de limites courantes (par exemple, conteneurs vides, valeurs zéro, longueurs incohérentes). Elle conserve des exemples représentatifs des buckets de limites critiques pour assurer la couverture des violations de préconditions typiques.
Réduction par élimination de l'adversaire (pour les entrées attendues) : Cette stratégie réutilise les implémentations adverses synthétisées lors de la phase d'expansion. Chaque paire entrée-sortie attendue est évaluée en fonction du nombre d'implémentations « mutantes » (adverses) qu'elle peut « éliminer » (c'est-à-dire produire une sortie différente). La réduction est formulée comme un problème de couverture d'ensemble, sélectionnant de manière gloutonne les paires qui couvrent le nombre maximal de mutants précédemment non éliminés. Cela garantit que la suite réduite conserve la capacité de distinguer les spécifications défectueuses.

Contributions clés

Cadre VeriScale : Les auteurs proposent un cadre général qui exploite les implémentations adverses pour piloter à la fois l'expansion systématique et la réduction des suites de tests pour la génération de code vérifiable.
VERINAPLUS et VERINALITE : Le cadre est instancié sur le benchmark VERINA pour créer deux nouveaux jeux de données :
- VERINAPLUS : Un benchmark étendu avec des suites de tests mises à l'échelle de plus de 83× (spécifiquement 62,83× pour les entrées attendues, 87,79× pour les sorties inattendues et 183,08× pour les entrées inattendues).
- VERINALITE : Une variante légère mise à l'échelle de 14×, optimisée par les stratégies de réduction pour maintenir un pouvoir discriminant avec des coûts d'évaluation réduits.
Validation empirique : L'article démontre que les benchmarks originaux surestiment considérablement les capacités des modèles. Les benchmarks améliorés révèlent des faiblesses substantielles dans les LLM de l'état de l'art qui étaient auparavant cachées.

Résultats expérimentaux

Les auteurs ont évalué huit LLM de l'état de l'art (incluant GPT-5.5, Claude-Sonnet-4.6 et DeepSeek-V4-Pro) sur VERINA, VERINAPLUS et VERINALITE.

Révélation des faiblesses des modèles : Les benchmarks augmentés ont provoqué des chutes brutales de performance. Par exemple, GPT-5.5 a vu son score SpecGen chuter de 68,78 % sur VERINA à 44,44 % sur VERINAPLUS, et son score CodeGen passer de 96,83 % à 86,24 %. Cela indique que les cas de tests épars du benchmark original permettaient aux modèles de passer sans véritable compréhension.
Réduction de l'incertitude d'évaluation : Les suites de tests étendues ont considérablement réduit les barres d'erreur dans l'évaluation SpecGen. Dans le benchmark original, des résultats de vérification indéterminés créaient de larges écarts entre les bornes supérieure et inférieure (par exemple, un écart de 13,23 % pour Claude-Opus-4.7). Sur VERINAPLUS, cette ambiguïté a été résolue, réduisant l'écart à 4,76 %, offrant une évaluation statistiquement plus fiable.
Écart de robustesse : Les résultats mettent en évidence une disparité fondamentale : les modèles sont nettement plus compétents en CodeGen qu'en SpecGen. Alors que les scores CodeGen ont connu des baisses modérées, les scores SpecGen ont subi des chutes précipitées, suggérant que la synthèse de spécifications formelles valides et exhaustives reste un goulot d'étranglement majeur pour les LLM actuels.
Efficacité de la réduction : VERINALITE a obtenu des profils de dégradation de performance presque identiques à VERINAPLUS mais avec une surcharge computationnelle considérablement réduite. Le temps d'évaluation pour VERINALITE n'était que 1,38× (SpecGen) et 1,05× (CodeGen) par rapport à la ligne de base, contre 1,80× et 1,50× pour la suite complète VERINAPLUS.

Importance et affirmations

L'article affirme que VeriScale fournit une norme cruciale et hautement fiable pour faire progresser la génération de code vérifiable basée sur les LLM. En allant au-delà des tests positifs épars pour inclure des cas négatifs synthétisés de manière adverse, le cadre offre une évaluation plus rigoureuse qui empêche la surestimation des capacités des modèles.

Les auteurs positionnent VeriScale comme complémentaire aux efforts existants ; plutôt que d'introduire de nouvelles tâches, il renforce les benchmarks existants en augmentant la qualité et la quantité des signaux de test. Le travail souligne la nécessité d'une mise à l'échelle des tests adverses pour révéler la fragilité des modèles actuels dans les tâches de raisonnement formel.

Limites reconnues :
Les auteurs notent que VeriScale dépend de la disponibilité de préconditions de vérité terrain et d'implémentations de référence. De plus, la qualité des sorties inattendues synthétisées est limitée par les capacités de raisonnement du LLM agissant en tant qu'« équipe rouge ». Enfin, la phase de construction reste intensive en calcul, nécessitant un échantillonnage massif de LLM et des exécutions Lean.

Travaux futurs :
Les auteurs proposent d'évoluer VeriScale vers un système de réparation en boucle fermée pour guider les modèles dans le correctif des spécifications défectueuses. Ils prévoient également d'utiliser VeriScale comme moteur de données adverses pour synthétiser des corpus d'entraînement pour des modèles d'autoformalisation dédiés et de généraliser le cadre à d'autres backends de vérification comme Dafny.