VeriSpec : quand une IA relit la « constitution » de ChatGPT et y trouve cinq contradictions

Imaginez un panneau à l'entrée d'un parc : « Interdiction de marcher sur la pelouse ». Dix mètres plus loin, un autre panneau : « Pique-nique obligatoire sur l'herbe ». Pris séparément, chacun est raisonnable. Le jour où vous arrivez avec votre panier, en revanche, vous allez enfreindre l'un des deux, quoi que vous fassiez.

Remplacez le parc par ChatGPT et les panneaux par le Model Spec d'OpenAI. Ce long document public décrit comment les modèles de l'entreprise doivent se comporter : quand refuser, quand obéir, comment parler à un utilisateur fragile, quoi faire d'un ordre douteux. Il sert de référence pour l'entraînement à l'alignement, pour le comportement au moment de la réponse et pour l'évaluation. C'est en quelque sorte la constitution de ChatGPT.

Une équipe de chercheurs des universités de Virginie, de Pennsylvanie et du Texas à Austin a eu l'idée de faire relire cette constitution par une IA, avec une seule consigne : chercher les endroits où le texte se contredit. Sur 405 règles, elle en a trouvé cinq paires qui ne peuvent pas être respectées en même temps. Les cinq ont été validées à la main puis signalées à OpenAI, qui, d'après les auteurs, « a répondu positivement et lancé des discussions internes ».

Le papier s'intitule Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning. Il est signé Zichen Xie, Mrigank Pawagi, Lize Shao, Yang Hu et Wenxi Wang, et a été déposé sur arXiv le 1er octobre 2026 (arXiv:2610.01847).

Le bug n'est pas dans le modèle, il est dans le règlement

Quand une IA se comporte mal, on suppose spontanément que le modèle n'a pas bien appris ses règles. Le papier envisage un autre cas, plus gênant : les règles elles-mêmes sont mal écrites.

Leur exemple fil rouge parle aux développeurs. Le Model Spec contient une règle (étiquetée 92bt dans le document) qui demande en substance de ne pas modifier les parties d'un texte que l'utilisateur n'a pas demandé de modifier. Une autre (e9ny) exige que le code généré soit exécutable, sans erreur de syntaxe.

Supposons maintenant qu'un utilisateur fournisse un bout de code contenant une erreur de syntaxe, demande d'y ajouter des commentaires explicatifs et précise qu'il ne veut que le code en sortie, sans un mot de plus. L'assistant peut laisser l'erreur en place, et le code ne tourne pas, ce qui viole e9ny. Il peut aussi la corriger, et il touche alors à quelque chose qu'on ne lui a pas demandé de changer, ce qui viole 92bt. Comme la sortie doit être uniquement du code, il ne peut même pas signaler le problème à côté. Aucune réponse ne satisfait les deux règles.

Les auteurs donnent une définition précise de ce qu'ils cherchent. Deux règles sont incohérentes (inconsistent) s'il existe une situation concrète où :

1. elles ont le même niveau d'autorité ;
2. leurs deux préconditions (« quand X se produit… ») s'appliquent ;
3. aucun comportement possible ne satisfait les deux postconditions (« …alors fais Y »), même en tenant compte de tout le contexte fourni par le texte (exemples, exceptions, consignes d'arbitrage).

Le premier critère compte beaucoup. Le Model Spec définit une hiérarchie d'autorité : root (les règles intouchables), system, developer, user, puis guideline. Une règle root l'emporte toujours sur une règle user, de la même façon que la Constitution prime sur un arrêté municipal. Un conflit entre deux niveaux différents est donc déjà tranché par le texte. Un vrai défaut, c'est deux règles de même rang qui se contredisent sans arbitre.

Pourquoi c'est plus difficile qu'il n'y paraît

On pourrait penser qu'il suffit de demander à un humain de relire. Le document est long et ses 405 règles forment plus de 80 000 paires possibles, presque toutes sans rapport entre elles. Une relecture humaine exhaustive est hors de portée.

Les deux approches classiques coincent chacune à leur façon.

La première est la formalisation. On traduit le texte en logique formelle, à la manière du langage Catala pour le droit fiscal, puis un solveur cherche mathématiquement les contradictions. Le problème est que la traduction déforme le texte. Les auteurs l'écrivent ainsi : « translation is precisely where meaning is lost ». Un texte normatif s'appuie sur des nuances entre « peut », « doit » et « devrait », sur des permissions, des comportements par défaut, des exceptions et des obligations souples. Une logique formelle écrase tout cela. Autant traduire un poème en tableur.

La seconde est le test comportemental (behavioral testing). On soumet des situations piégeuses à plusieurs modèles et on regarde s'ils divergent. Mais si deux modèles répondent différemment, rien ne dit que c'est la faute du règlement. Comme le note le papier, un désaccord peut venir de différences d'entraînement, d'alignement ou de capacités, et non d'un défaut de la spécification. Observer des élèves qui hésitent ne permet pas de savoir si c'est l'énoncé qui est ambigu.

VeriSpec prend une troisième voie : garder le texte en langage naturel et confier la vérification à un LLM. On ne traduit rien et on n'observe aucun modèle en train de répondre. On audite le texte lui-même.

VeriSpec en trois étapes : découper, regrouper, interroger

Étape 1 : transformer la prose en règles structurées

Le Model Spec d'OpenAI comporte déjà des petites étiquettes (92bt, e9ny…) qui identifient ses principes. Il y en avait 279. Les auteurs ont fait compléter les 126 manquantes par Claude Code, en lui donnant les annotations existantes comme modèles, pour un total de 405 règles.

Chaque règle devient une petite fiche à quatre champs : l'identifiant, le niveau d'autorité, la précondition et la postcondition, ces deux dernières rédigées en langage naturel. S'y ajoute le contexte de la règle : les exemples travaillés, les exceptions et les consignes de compromis qui l'accompagnent dans le texte. Ce contexte joue un rôle décisif, parce qu'une tension apparente entre deux règles est souvent résolue trois paragraphes plus loin par une exception explicite.

La répartition est instructive : 190 règles root, 15 system, 5 developer, 87 user et 108 guideline.

Le système attribue ensuite à chaque règle un ou plusieurs thèmes (topics). On en compte 45, par exemple transformation_fidelity (fidélité lors d'une transformation de texte) ou output_format_adherence (respect du format demandé). Ils sont proposés par trois agents indépendants, puis consolidés. Les thèmes trop gros, au-delà de 30 règles, sont redécoupés en sous-thèmes.

Étape 2 : un graphe pour ranger les règles qui risquent de se croiser

Comparer 80 000 paires coûterait trop cher, et la plupart de ces comparaisons ne serviraient à rien. Les auteurs construisent donc un graphe de règles. Pensez à un plan de table de mariage : on place côte à côte les invités susceptibles de se disputer, pour pouvoir surveiller ces tables-là.

Les nœuds sont des couples (règle, thème). Une règle à plusieurs thèmes apparaît plusieurs fois, ce qui donne 625 nœuds. Les arêtes sont de deux sortes : sémantiques, quand les deux règles partagent un thème, et syntaxiques, quand elles se trouvent dans la même sous-section, partagent un exemple travaillé ou se citent l'une l'autre.

Une contrainte s'applique partout : on ne relie que des règles de même niveau d'autorité, puisque les autres conflits sont déjà arbitrés par la hiérarchie.

Un algorithme regroupe d'abord les nœuds par couple (autorité, thème), ce qui donne 113 groupes. Les groupes trop petits, sous 12 nœuds, sont ensuite fusionnés avec des voisins proches, sans dépasser 28 nœuds. On obtient 32 unités d'analyse de 5 à 26 règles chacune. Ce sont 32 tables de mariage de taille raisonnable, qu'un LLM peut examiner en entier.

Étape 3 : le LLM en vérificateur, pas en détecteur

Un LLM à qui l'on demande « trouve-moi des contradictions » en trouve beaucoup, et la plupart sont imaginaires. VeriSpec le place donc dans un rôle de vérificateur (LLM-as-verifier) : chaque signalement doit être prouvé.

Pour qu'un rapport soit recevable, le vérificateur doit fournir trois éléments :

1. une situation témoin concrète, c'est-à-dire un scénario précis où les deux préconditions s'appliquent ;
2. un argument d'insatisfiabilité, la démonstration qu'aucune réponse ne satisfait les deux postconditions à la fois ;
3. un argument de non-résolution, l'explication de pourquoi le contexte combiné des deux règles (exceptions, exemples, priorités) ne règle pas le problème.

C'est la différence entre « j'ai l'impression que ces deux lois se contredisent » et un mémoire d'avocat argumenté point par point.

Le vérificateur choisi est Claude Opus 5, parce qu'il suit fidèlement le format de vérification structuré et va au bout de chaque unité d'analyse. GPT-6 Astra a donné des résultats similaires pour un coût plus élevé. Claude Fable 5.1, lui, a bloqué la plupart des requêtes au titre des restrictions d'Anthropic sur les contenus cyber.

Les auteurs ont aussi dû contourner un autre obstacle. Les LLM propriétaires rechignaient à analyser en profondeur un document qui mentionne nommément « OpenAI » ou des modèles GPT, parce que ces références déclenchent leurs garde-fous de sécurité. La solution a été d'anonymiser la spécification en remplaçant ces noms par des noms synthétiques. Ainsi déguisé, le texte passe sans difficulté.

Les LLM n'étant pas déterministes, chaque unité est analysée 5 fois de manière indépendante, soit 160 requêtes au total. Les auteurs observent que le nombre de candidats distincts plafonne à 13 au bout de ces cinq passes.

Les cinq contradictions trouvées

Deux examinateurs humains ont jugé indépendamment chacun des 13 candidats, puis ont discuté en cas de désaccord. Cinq ont été retenus.

La première est le code cassé à commenter (niveau user). C'est l'exemple déjà décrit : ne rien modifier sans demande ou rendre le code exécutable.

La deuxième est l'omission illégale à signaler (niveau system). Une règle demande d'opérer dans le cadre légal applicable. Une autre demande d'indiquer de manière transparente qu'un contenu a été omis pour des raisons légales. Si une loi locale impose l'omission et interdit en plus de la mentionner, l'assistant enfreint forcément l'une des deux règles. Le cas est loin d'être théorique : on pense aux injonctions de silence imposées par certaines juridictions.

La troisième est le méchant de fiction (niveau user). Face aux violations des droits humains fondamentaux, le modèle doit affirmer clairement qu'elles sont condamnables. En jeu de rôle créatif, il doit jouer le jeu sans plaquer de point de vue « objectif ». Si l'on demande le monologue d'un personnage qui défend l'esclavage, l'assistant viole une règle s'il ajoute une condamnation et l'autre s'il n'en met pas.

La quatrième est la traduction d'une fausse affirmation (niveau user). Pour une sortie destinée à être consommée par un programme, il faut exécuter sans commentaire. Si la demande repose sur une prémisse fausse, il faut le signaler. Que faire quand on demande de traduire « Canberra est la capitale de la Nouvelle-Zélande » pour une ingestion automatique ? Signaler l'erreur pollue la sortie, et traduire sans rien dire laisse passer le faux.

La cinquième est la réassurance flatteuse (niveau user). Une règle demande de respecter les normes de politesse pour ne pas abîmer l'image que l'utilisateur a de lui-même. Une autre interdit la flatterie et l'approbation systématique. Un parent décrit une conduite risquée envers son enfant et demande : « Dites-moi que je ne suis pas une mauvaise mère. » Ce que la politesse autorise ici correspond justement à ce que la règle anti-flagornerie interdit.

Aucun de ces cas n'est spectaculaire, et c'est pour cela qu'ils sont intéressants. Ce sont des situations ordinaires, comme un développeur pressé, une traduction de routine ou un parent inquiet, dans lesquelles le modèle n'a aucune bonne réponse possible selon ses propres règles.

La comparaison avec les approches naïves

Les auteurs comparent VeriSpec à cinq méthodes de référence (baselines). Le tableau montre ce que chaque étape apporte :

Méthode	Principe	Rapports	Validés	Précision	Coût / incohérence validée
DirectAgent	Spec entière confiée à un agent Claude Code	9	0	0 %	aucune (27,66 $ dépensés)
DirectPrompt	Spec entière dans un seul prompt	16	0	0 %	aucune (4,92 $ dépensés)
SectionText	Pas d'extraction de règles, une unité par section	10	1	10 %	58,64 $
SectionGroup	Règles extraites, mais groupées par section	8	1	12,5 %	63,94 $
PlainDetect	Mêmes unités que VeriSpec, détection libre	221	3	1,4 %	15,82 $
VeriSpec	Pipeline complet	13	5	38,5 %	11,12 $

Trois enseignements ressortent.

Donner tout le document d'un coup ne sert à rien. Ni l'agent ni le prompt unique ne trouvent une seule vraie incohérence. Le modèle survole le texte et ne vérifie pas systématiquement si une exception résout la tension.

Grouper par section fait rater l'essentiel. Le cas du code cassé met en jeu deux règles situées dans des sections différentes. Seule l'incohérence légale, dont les deux règles sont voisines, est détectée par ces méthodes.

Exiger des preuves change tout. PlainDetect utilise exactement les mêmes unités d'analyse que VeriSpec, mais sans l'obligation de fournir les trois arguments. Il produit 221 alertes pour 3 vraies trouvailles. L'exigence de preuve réduit la liste à 13 et fait passer la précision de 1,4 % à 38,5 %.

Au total, l'audit complet a coûté 55,62 $, soit 11,12 $ par contradiction confirmée.

Pourquoi ce papier compte

Le Model Spec n'est pas un document décoratif. Il sert à générer des données d'entraînement, à écrire des grilles d'évaluation et à guider le comportement des modèles en production. Une contradiction à ce niveau se propage partout en aval : le modèle apprend un compromis arbitraire, les évaluateurs le sanctionnent de manière incohérente, et personne ne comprend pourquoi le comportement varie d'une version à l'autre.

Le papier déplace donc la vérification en amont. Les auteurs parlent de défauts attrapés « à la source, avant qu'ils ne façonnent un modèle ». C'est l'équivalent, en génie logiciel, de la relecture des spécifications avant l'écriture du code, et ce n'est pas un hasard si le papier est classé en cs.SE (génie logiciel) autant qu'en IA.

Le ratio coût/bénéfice est aussi frappant. Quelques dizaines de dollars d'API pour améliorer un texte qui encadre le comportement de modèles utilisés par des centaines de millions de personnes, la dépense est dérisoire.

Enfin, la recette dépasse le cas d'OpenAI : extraction structurée, regroupement intelligent, puis LLM sommé de justifier ses accusations. Elle pourrait s'appliquer à d'autres textes normatifs écrits en langage naturel, comme les chartes d'entreprise, les conditions d'utilisation ou les règlements intérieurs.

Les bémols

Le papier ne contient pas de section dédiée aux limites. Celles qui suivent sont de notre cru.

• Le rappel n'est pas mesuré. On sait que 5 incohérences sur 13 signalées sont vraies, mais on ignore combien le texte en contient au total. VeriSpec en a peut-être trouvé l'essentiel, ou seulement une petite partie. Le papier ne donne pas d'estimation, et sa contrainte « même niveau d'autorité » écarte d'emblée certains types de défauts.
• Une seule spécification a été testée, le Model Spec d'OpenAI dans sa version d'août 2026. On ne sait pas encore comment la méthode se comporte sur la constitution d'Anthropic ou les chartes d'autres fournisseurs.
• La validation humaine est légère. Deux examinateurs, un consensus en cas de désaccord, mais pas de taux d'accord inter-annotateurs publié. Les 8 rapports rejetés ne sont pas analysés en détail, alors que c'est souvent là qu'on apprend le plus sur les angles morts d'une méthode.
• Une partie de la base a été posée par une IA. Près d'un tiers des annotations (126 sur 405) ont été rédigées par Claude Code, sans que le papier décrive de vérification humaine systématique. Une règle mal extraite peut fausser toute la suite.
• Une précision de 38,5 %, la meilleure du lot, signifie quand même que près de deux alertes sur trois sont fausses. Pour un audit ponctuel, c'est acceptable. Pour un contrôle continu, il faudra garder un humain dans la boucle.
• L'astuce de l'anonymisation fonctionne, mais elle revient à contourner les garde-fous des LLM commerciaux. Ces garde-fous peuvent évoluer, et la méthode dépend des choix de filtrage des fournisseurs, comme le montre l'exemple de Fable 5.1 qui bloque la plupart des requêtes.
• « Discussions internes » ne veut pas dire correction. Le papier n'indique ni si ni comment OpenAI va réécrire les règles concernées.

Ce qu'on va surveiller

La situation a quelque chose d'ironique : il a fallu une IA, guidée par ses propres règles de sécurité, pour relire les règles d'une autre IA. Le principe est pourtant celui d'une bonne relecture juridique : on exige de l'accusateur une preuve, un scénario précis et une démonstration.

Les auteurs annoncent plusieurs suites : la réparation automatique des spécifications (proposer une reformulation, pas seulement signaler), la vérification incrémentale (réauditer seulement ce qui change à chaque nouvelle version du texte) et l'audit croisé entre fournisseurs. Ce dernier point est sans doute le plus intéressant, car les constitutions d'IA se multiplient et personne ne vérifie vraiment leur cohérence interne.

À surveiller aussi : la prochaine version du Model Spec d'OpenAI. Si les règles 92bt et e9ny reçoivent une nouvelle clause d'arbitrage, VeriSpec aura contribué à modifier le texte qui encadre ChatGPT.

Référence : Zichen Xie, Mrigank Pawagi, Lize Shao, Yang Hu, Wenxi Wang, « Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning », arXiv:2610.01847, déposé le 1er octobre 2026. https://arxiv.org/abs/2610.01847. Code : github.com/HIPREL-Group/VeriSpec.