Chaque ingénieur expérimenté a une histoire où une fonctionnalité a été livrée, a fonctionné sur le chemin heureux, puis a silencieusement fait la mauvaise chose dans un cas limite auquel personne n'avait pensé. Si l'on remonte suffisamment loin la trace du bogue, elle se termine rarement dans le code; elle se termine dans une phrase d'un document d'exigences qui signifiait une chose pour la personne qui l'a écrite et autre chose pour la personne qui l'a implémentée.

Les bogues dans vos exigences

Les bogues d'exigences se répartissent en quatre classes, et elles sont toutes très difficiles à repérer à la première lecture :

Mauvais niveau de détail : l'exigence est en réalité un énoncé de thèse (« le système doit prendre en charge l'authentification ») ou une recette d'implémentation (« le système doit utiliser des jetons JWT avec une durée de vie de 15 minutes »), et non une contrainte vérifiable sur un comportement observable.
Ambiguïté : la même phrase a deux interprétations plausibles, et deux développeurs l'implémenteraient différemment. Nous ne sommes généralement pas conscients de notre propre biais d'interprétation, si bien que ce qui vous semble parfaitement clair peut ne pas l'être pour quelqu'un d'autre ayant un biais d'interprétation différent.
Incohérence : deux exigences, chacune sensée en isolation, ne peuvent pas être vraies simultanément. Cela est généralement découvert tardivement dans le processus de développement et force un arbitrage. Différents développeurs peuvent résoudre le conflit différemment, et dans certains cas, les problèmes sont résolus au niveau de l'implémentation sans être soulevés et clarifiés au niveau de la spécification.
Incomplétude : l'exigence décrit ce que le système doit faire seulement pour certaines entrées, laissant le comportement non spécifié pour des régions entières de l'espace d'entrée. Différents développeurs peuvent décider d'agir différemment sur ces entrées et introduire un comportement non spécifié.

Les problèmes de niveau de détail et d'ambiguïté sont difficiles à détecter parce qu'ils concernent ce qui n'est pas explicitement énoncé dans la spécification et la façon dont différentes personnes ou agents de programmation par IA peuvent interpréter les exigences. Les problèmes d'incohérence sont difficiles à détecter parce qu'ils exigent de raisonner sur plusieurs exigences simultanément pour trouver des déclencheurs communs et analyser les conséquences. Les problèmes de complétude sont également difficiles à détecter, car ils exigent de raisonner sur l'ensemble de la spécification en une seule fois pour voir s'il reste des lacunes.

L'ingénierie assistée par l'IA aggrave ce problème de deux façons. Premièrement, la requête que vous donnez à l'agent est désormais l'exigence de facto. Votre requête initiale est le seul artefact tangible qui capture « ce que nous voulons construire ». Chaque requête vague produit un spec ou un plan vague, et l'agent d'IA qui implémente ce spec produit du code plein de décisions non divulguées prises en votre nom, sans que vous en soyez conscient ni que vous ayez donné votre accord. Deuxièmement, les agents d'IA génèrent du code plus rapidement que les humains ne peuvent le réviser, si bien que l'écart entre ce que vous vouliez construire et ce qui a été construit ne cesse de s'élargir.

Ce n'est pas une intuition. Des travaux récents qui ont expérimenté la transformation de requêtes claires en requêtes ambiguës, incomplètes ou contradictoires montrent des chutes de Pass@1 de 20 à 40 %, avec 60 à 90 % du code syntaxiquement valide qui est sémantiquement incorrect (Larbi et al., 2025). Le code fonctionne, mais ne fait pas ce que vous voulez qu'il fasse. Une étude distincte sur la sous-spécification des requêtes constate que les LLM comblent silencieusement les lacunes des exigences non spécifiées, et que les requêtes sous-spécifiées sont environ deux fois plus susceptibles de régresser lors de changements de modèle ou de requête, parfois avec des chutes de précision dépassant 20 % (Yang et al., 2025). Le code compile, les tests passent, et le comportement diverge tout de même de ce qui était prévu, parce que les modèles plus récents comblent les lacunes avec un biais non divulgué et différent des modèles précédents. Les spécifications vagues ont un coût mesurable, et ce coût ne se révèle qu'après avoir dépensé des jetons pour générer une première version du code.

Le flux de travail axé sur les specs de Kiro s'attaque à ce problème en guidant les développeurs à travers un flux de travail plus structuré pour le développement agentif : Requête → Requirements → Design → Tasks → Code. Votre conversation initiale avec l'agent produit des exigences explicites en notation EARS. Kiro les transforme en un document de conception qui concrétise les décisions architecturales et algorithmiques, définit une stratégie de vérification par des tests basés sur les propriétés, et produit une liste de tâches. L'agent exécute ensuite chaque tâche en se référant à la spécification et à la conception.

Le document de spécification est la source de vérité dans ce processus, mais il peut néanmoins souffrir des problèmes décrits ci-dessus.

C'est pourquoi nous avons introduit l'analyse des exigences, une nouvelle étape optionnelle dans le flux de travail de Kiro qui analyse votre requirements.md pour les classes de problèmes énumérées ci-dessus, avant qu'aucun design ou code ne soit généré. L'analyse des exigences utilise des techniques neurosymboliques pour vérifier que les exigences ont le bon niveau de détail, signaler les critères d'acceptation qui admettent plusieurs interprétations plausibles, et détecter les contradictions ou les lacunes de complétude. Chaque type de constat est présenté sous forme de question simple à deux choix. Vous choisissez une réponse (ou vous laissez un critique basé sur un LLM sélectionner une réponse pour vous); l'exigence est mise à jour; le pipeline continue. Sous le capot, l'analyse encode automatiquement la spécification en logique formelle à l'aide de LLM et utilise des solveurs SMT pour générer les constats, mais vous n'avez pas besoin de connaissances en méthodes formelles pour l'utiliser, et la formalisation reste hors de vue.

Qu'est-ce qui fait une bonne spécification?

La partie difficile de l'ingénierie des spécifications est qu'il n'existe aucun oracle pour la justesse d'une spécification autre que l'utilisateur. Seul vous savez ce que vous vouliez réellement dire et si la spécification capture ou non votre intention. Comment quoi que ce soit peut-il être vérifié automatiquement si la vérité fondamentale réside dans la tête de quelqu'un? Heureusement, au-delà de la capture de l'intention spécifique pour un système donné, toute spécification doit obéir à une poignée de propriétés de qualité génériques qui sont indépendantes du domaine. Celles-ci peuvent être vérifiées automatiquement. Ce qui reste, choisir l'interprétation qui correspond le mieux à l'intention réelle, est là où l'utilisateur doit intervenir. L'analyse des exigences automatise la première partie et présente la seconde sous la forme d'un petit nombre de questions concrètes que l'utilisateur peut répondre rapidement.

Les propriétés génériques que nous attendons de toute spécification raisonnable sont :

Vérifiable. Une bonne spécification doit décrire des conditions observables sur des quantités observables. En la lisant, vous devriez pouvoir nommer les entrées, les sorties et les conditions dans lesquelles la réponse du système est celle requise. « Le système doit authentifier les utilisateurs » échoue à ce test : vous ne pouvez pas nommer de sortie. « Lorsqu'un utilisateur soumet des identifiants qui correspondent à un compte valide, le système doit retourner un jeton de session authentifié » réussit, car les entrées, les sorties et la condition sont toutes explicites.
Sans solution. Une bonne exigence décrit ce que le système fait, pas comment. « Le système doit implémenter la suppression logicielle pour conserver les enregistrements dans la base de données à des fins d'audit » prescrit un mécanisme. « Lorsqu'un enregistrement est marqué comme supprimé, le système doit l'exclure des vues destinées à l'utilisateur tout en le conservant pour l'accès administratif » décrit le comportement observable et laisse l'implémentation ouverte.
Sans ambiguïté. Deux lecteurs indépendants formaliseraient une exigence sans ambiguïté de la même manière. « Le système doit supprimer l'enregistrement » est ambigu : un lecteur entend suppression définitive et un autre entend suppression logicielle. « Le système doit marquer l'enregistrement comme supprimé de telle sorte qu'il ne soit plus visible dans aucune vue destinée à l'utilisateur » fixe le résultat observable.
Cohérente. Prises ensemble, les exigences doivent admettre au moins une implémentation, ce qui signifie qu'il ne doit y avoir aucune situation où deux critères d'acceptation exigent des comportements incompatibles du système.
Complète. Le comportement du système doit être spécifié pour toute combinaison d'entrées; il ne doit y avoir aucun état où les exigences ne prescrivent pas ce que le système doit faire.

Ces propriétés ne sont pas nouvelles : elles proviennent de décennies de pratique en ingénierie des systèmes. Ce qui est nouveau, c'est que les LLM peuvent désormais effectuer la majeure partie du travail visant à les faire respecter automatiquement : réécrire des exigences vagues en exigences vérifiables, repérer quand un langage d'implémentation s'est glissé dans une spécification. Au cours de nos expériences, nous avons remarqué que la plupart des exigences générées à partir de la conversation initiale avec l'agent sur une idée de fonctionnalité commencent au niveau de la thèse : trop vagues ou trop abstraites pour être formalisées et analysées de manière significative en matière de cohérence ou de complétude. Ce n'est pas une critique de Kiro ni des LLM, un humain produirait un premier jet similaire. Le point est que le premier jet n'est que le point de départ d'une passe de raffinement censée amener les exigences au bon niveau de détail, à partir duquel la formalisation, l'analyse de cohérence et de complétude deviennent réellement utiles.

Ce qui est également nouveau est que les techniques neurosymboliques permettent de traduire le langage naturel en énoncés logiques formels et de détecter automatiquement les problèmes de cohérence et de complétude. Ce que les techniques neurosymboliques ne peuvent pas faire est de décider pour vous, parmi plusieurs interprétations formelles plausibles d'une exigence, laquelle correspond réellement à votre intention initiale. Néanmoins, nous pouvons vous aider à décider sans vous submerger de logique formelle en générant des scénarios qui révèlent une divergence sémantique, en localisant précisément la cause profonde de la divergence, et en vous la présentant sous forme de questions à deux choix qui vous permettent de clarifier votre propre interprétation.

Ce que l'analyse des exigences vous présente

Le pipeline d'analyse des exigences contient trois étapes principales : d'abord le raffinement (pour amener les exigences à un niveau de détail approprié pour la formalisation), puis l'auto-formalisation (où les exigences sont automatiquement traduites en logique formelle à l'aide d'un LLM), et enfin l'analyse logique où un moteur de raisonnement automatisé analyse la complétude et la cohérence des exigences formalisées.

L'étape de raffinement produit de nouveaux critères d'acceptation EARS. Les phases d'auto-formalisation et d'analyse logique produisent différents types de constats techniques. Cependant, afin de rendre l'expérience utilisateur plus uniforme, chaque type de constat technique est traduit en une question en langage naturel avec deux réponses possibles : la réponse A signifie toujours conserver l'exigence telle quelle; la réponse B signifie toujours la modifier d'une certaine manière, avec une proposition précise.

Voici un exemple de constat d'ambiguïté pour une exigence « Delete Property ». Les constats d'ambiguïté sont détectés pendant l'étape d'auto-formalisation lorsque nous découvrons qu'un critère d'acceptation donné admet plusieurs traductions logiques sémantiquement divergentes :

Loading code example...

Le constat d'ambiguïté technique serait présenté sous forme de question

La phrase « supprimer l'enregistrement » pourrait signifier que l'enregistrement est entièrement disparu, ou marqué comme supprimé et conservé pour audit. Que vouliez-vous dire?

A) Conserver tel quel : l'enregistrement a disparu.

B) Modifier : l'enregistrement est conservé, mais caché des vues destinées à l'utilisateur.

Nous présentons cinq types de constats de cette manière :

Questions d'ambiguïté : une phrase a deux significations plausibles et vous en choisissez une.
Questions de conflit : deux règles peuvent se déclencher dans la même situation et exiger des résultats incompatibles; vous choisissez laquelle l'emporte, ou vous en restreignez une.
Questions de complétude : une situation accessible n'a aucune règle définissant un comportement; vous décidez si ce silence est intentionnel.
Questions de scénario accepté : la spécification permet actuellement un certain comportement (utiliser des données en cache lorsque des données fraîches sont disponibles, par exemple); vous confirmez que la permission est intentionnelle.
Questions de scénario rejeté : le miroir. La spécification interdit actuellement un certain comportement (rejeter les requêtes contenant uniquement des espaces avant élagage); vous confirmez que l'interdiction est intentionnelle.

Le reste de ce billet porte sur la façon dont l'analyse des exigences produit ces questions. Nous avons trois étapes : le raffinement réécrit les phrases de niveau thèse en phrases vérifiables; l'auto-formalisation traduit le langage naturel en un modèle formel; l'analyse logique utilise ce modèle pour trouver des contradictions, des lacunes et énumérer des exemples de comportements du système qui sont soit acceptés, soit rejetés par les exigences.

Raffinement : amener les exigences au bon niveau de détail

Avant d'analyser la cohérence ou la complétude à l'aide de techniques neurosymboliques, les exigences ont besoin de suffisamment de détails et de structure pour que la formalisation et l'analyse en vaillent la peine. Un critère d'acceptation de niveau thèse comme « le système doit implémenter la suppression logicielle » se formalise en un seul booléen opaque : il n'y a pas grand-chose à raisonner. Le raffinement est l'étape qui transforme les phrases de niveau thèse en critères vérifiables, sans solution, qui nomment leurs événements, entrées, états et sorties, et les conditions logiques qui doivent tenir entre eux avec suffisamment de précision.

L'analyse des exigences raffine automatiquement les exigences à gros grain en utilisant un LLM et en travaillant à rebours à partir de l'histoire utilisateur avec une approche de raisonnement abductif. Le raffinement exige une compréhension du contexte et de la créativité, c'est pourquoi il est piloté par un LLM. Étant donné l'histoire « en tant que propriétaire d'une propriété, je veux supprimer une propriété, afin de pouvoir retirer les propriétés que je ne gère plus », et la version initiale des critères d'acceptation, le processus de raffinement demande à quoi ressemble l'état de succès et quels prérequis doivent être remplis pour que cet état soit atteint sans échec. Pour chaque prérequis, il demande : qu'est-ce qui pourrait empêcher ceci? Quels chemins d'erreur devraient exister? La condition est-elle déjà capturée par un critère d'acceptation existant, ou en faut-il un nouveau? En cours de route, il vérifie chaque critère d'acceptation existant pour un mauvais usage du modèle EARS, des qualificatifs vagues et un langage de niveau implémentation. Tout cela est fait pour vous en coulisses, automatiquement.

Voici à quoi cela ressemble sur un exemple réel. L'exigence originale « Delete Property » a cinq critères d'acceptation :

WHEN a Property Owner initiates property deletion, THE Platform SHALL prompt for confirmation before proceeding
WHEN a Property Owner confirms deletion, THE Platform SHALL remove the Property record from the Platform
WHEN a Property is deleted, THE Platform SHALL display a confirmation message and redirect to the properties list
THE Platform SHALL implement soft deletion to retain Property records in the database for audit purposes while hiding them from the user interface
WHEN a Property Owner attempts to delete a Property that does not belong to their User Account, THE Platform SHALL deny the deletion and display an authorization error message

Lus un par un, les critères d'acceptation semblent corrects. Cependant, l'analyse de raffinement révèle trois types de problèmes :

Le critère 2 contredit le critère 4. Le critère 2 dit « supprimer l'enregistrement », ce qui est une suppression définitive. Le critère 4 dit « implémenter la suppression logicielle pour conserver les enregistrements dans la base de données », donc l'enregistrement reste. Lequel est-ce? Un développeur lisant la spécification devrait deviner.
Le critère 4 mélange le quoi et le comment. « Implémenter la suppression logicielle » et « conserver les enregistrements dans la base de données » sont des choix d'implémentation. Les conditions observables que nous voulons ne sont pas énoncées clairement : l'enregistrement doit rester récupérable pour l'accès d'audit, mais ne doit pas apparaître dans les vues destinées à l'utilisateur.
Le critère 5 utilise le mauvais modèle EARS. « N'appartient pas à leur compte utilisateur » est une condition d'erreur. En EARS, les conditions d'erreur doivent utiliser le modèle IF-THEN; les modèles WHEN sont pour les conditions nominales. Une réécriture bien formée serait : « IF the property does not belong to the requesting user, THEN the Platform SHALL reject the deletion ».

Le raffinement corrige les trois, puis va plus loin, en travaillant à rebours à partir de l'état de succès pour se demander ce qui pourrait empêcher une suppression réussie. Que se passe-t-il si la propriété n'existe pas? Que se passe-t-il si elle a des baux actifs? Que se passe-t-il si l'utilisateur annule l'invite de confirmation? Aucun de ces chemins n'est couvert par l'exigence initiale. Trois nouveaux critères d'acceptation sont ajoutés pour combler les lacunes. Le résultat final est cinq critères d'acceptation modifiés (contradiction résolue, langage d'implémentation supprimé, modèles EARS corrigés) plus trois nouveaux critères d'acceptation couvrant les chemins d'erreur manquants :

Le texte détaillé des exigences raffinées :

WHEN a Property Owner initiates property deletion, THE Platform SHALL prompt for confirmation before proceeding (INCHANGÉ).
WHEN a Property Owner confirms deletion, THE Platform SHALL mark the Property record as deleted such that it is no longer visible in any user-facing view (MODIFIÉ).
WHEN a Property is deleted, THE Platform SHALL display a confirmation message and redirect to the properties list (INCHANGÉ).
WHEN a Property record is marked as deleted, THE Platform SHALL retain the record for admin/audit access while excluding it from all user-facing views (MODIFIÉ).
IF the Property does not belong to the requesting Property Owner's User Account, THEN THE Platform SHALL reject the deletion and display an authorization error (MODIFIÉ).
IF the Property has active leases, THEN THE Platform SHALL reject the deletion and indicate active leases exist (AJOUTÉ).
IF the Property does not exist, THEN THE Platform SHALL display a not-found error (AJOUTÉ).
WHEN a Property Owner cancels the confirmation prompt, THE Platform SHALL abort deletion and return to the previous view (AJOUTÉ).

L'exigence réécrite et ses critères d'acceptation sont maintenant vérifiables, sans solution, et sans contradictions internes immédiatement apparentes. Le raffinement ne peut pas exclure complètement l'ambiguïté, parce que certains mots ont réellement plus d'une signification plausible, et il ne peut pas garantir que l'ensemble des critères réécrits est réellement logiquement cohérent et complet dans son ensemble. Cependant, l'exigence raffinée est maintenant susceptible d'être formalisée en logique, ce qui nous permettra ensuite de vérifier si les critères d'acceptation formalisés sont réellement logiquement cohérents et complets. La formalisation permet également la génération de scénarios : des exemples de scénarios acceptés ou rejetés par vos exigences vous permettent de vérifier que votre intention est bien capturée par les exigences. La formalisation est l'étape où nous détectons les critères d'acceptation qui sont ambigus dans le sens qu'ils admettent plus d'un encodage plausible en logique, et nécessitent une clarification de l'intention de l'utilisateur.

Auto-formalisation : du langage naturel à un modèle formel

Une fois qu'une exigence est au bon niveau de détail, l'étape suivante consiste à la traduire en un modèle logique formel qu'un moteur de raisonnement automatisé peut analyser. Aujourd'hui, le modèle formel est exprimé dans le langage formel SMT-lib. Concrètement, il comporte trois parties :

Un schéma déclarant les symboles formels dont parlent les exigences : les entités (p. ex. Property, Order), leurs attributs (p. ex. order_state, inventory_available), les événements qui peuvent survenir (order_submitted, order_canceled), les entrées et les sorties (ce que le système fait en réponse). Chaque symbole porte une courte description en langage naturel afin de pouvoir être retracé jusqu'au texte source.
Un ensemble d'assertions encodant les critères d'acceptation comme des implications logiques antecedent => consequent exprimées sur les symboles déclarés dans le schéma. Chaque clause EARS se traduit clairement en une implication : les clauses WHERE/WHILE/WHEN/IF deviennent l'antécédent, la clause THE ... SHALL devient le conséquent.
Un ensemble d'assertions d'arrière-plan, qui modélise des contraintes supplémentaires entre les symboles du schéma encodant des connaissances implicites d'arrière-plan sur la façon dont les symboles sont liés, mais non explicitement mentionnées dans les exigences : par exemple, les durées sont positives (duration >= 0), lorsque la variable timeout_occurred est vraie, alors cela signifie que duration > max_duration, etc.

La formalisation est effectuée par un LLM. La traduction par LLM a une particularité importante : elle est non déterministe. Demandez la version formelle du même critère d'acceptation dix fois et vous pourriez obtenir plusieurs réponses différentes. Parfois, les différences sont cosmétiques (noms de variables, ordre des conditions dans une conjonction). Parfois, elles sont sémantiques : un échantillon décide que « supprimer l'enregistrement » signifie suppression définitive tandis qu'un autre décide qu'il signifie « suppression logicielle »; un échantillon lit « la durée est positive » comme strictement supérieure à zéro tandis qu'un autre permet zéro dans l'intervalle. Ces différences sont exactement les types de problèmes d'ambiguïté que nous essayons de détecter : elles révèlent une véritable ambiguïté dans le langage naturel, ou des endroits qui entraînent une confusion du LLM, se manifestant sous forme d'encodages formels sémantiquement divergents.

Nous transformons ce non-déterminisme en mécanisme de détection en mesurant l'entropie sémantique de la traduction. Nous échantillonnons plusieurs formalisations candidates de chaque exigence et utilisons le moteur de raisonnement automatisé pour les regrouper par équivalence logique : les candidats qui se comportent de manière identique pour toutes les entrées possibles se retrouvent dans le même groupe (même s'ils diffèrent syntaxiquement), tandis que les candidats qui divergent sur au moins certaines entrées se retrouvent dans des groupes différents. L'entropie sémantique mesure à quel point le LLM est en désaccord avec lui-même sur le sens de l'exigence, et nous définissons deux seuils configurables low_entropy et high_entropy :

L'entropie sémantique est inférieure à low_threshold : le LLM est confiant. Nous faisons confiance à la formalisation et sélectionnons le représentant du groupe majoritaire comme interprétation formelle de l'énoncé EARS naturel.
L'entropie sémantique est supérieure au seuil high_entropy : le LLM ne peut pas formaliser l'énoncé EARS de manière fiable et hallucine probablement, donc nous nous abstenons d'utiliser le résultat de la traduction. L'énoncé EARS doit être reformulé.
L'entropie sémantique se situe entre les seuils low_entropy et high_entropy : le LLM produit de manière robuste quelques interprétations dominantes de l'énoncé EARS. Cela nécessite une clarification de l'utilisateur. Nous calculons une diff sémantique entre les deux meilleurs candidats, une caractérisation précise des situations où les candidats divergent et de la partie de l'énoncé EARS qui est formalisée différemment entre les candidats. La diff sémantique formelle est ensuite retraduite en une question de clarification en langage naturel : « dans cette situation, ces deux lectures ne s'accordent pas sur la question de savoir si l'enregistrement existe toujours après la suppression, laquelle vouliez-vous dire? »

Dans quelle mesure l'auto-formalisation fonctionne-t-elle réellement en pratique? Une étude du MIT et d'Airbus sur l'ingénierie des exigences assistée par LLM à l'échelle d'Airbus a trouvé des résultats solides pour la classification et l'extraction d'entités, mais des preuves faibles pour la formalisation et la génération des exigences (Norheim et al., 2024). Notre propre évaluation raconte une histoire plus nuancée. Les LLM semblent plutôt bons pour raffiner et formaliser des critères d'acceptation individuels tels qu'explicitement énoncés dans les documents d'exigences. Ce qui nécessite plus de travail à l'avenir, c'est l'extraction des connaissances implicites du domaine à partir de l'utilisateur et des LLM. La connaissance implicite du domaine est la « matière noire » des exigences qui les fait tenir ensemble, que nous, en tant qu'humains, n'écrivons généralement pas parce que toutes les personnes opérant dans le même domaine en sont déjà conscientes : le fait qu'une commande ne peut pas être annulée avant d'avoir été soumise, qu'une propriété ne peut pas avoir deux propriétaires actifs, qu'un paiement remboursé ne peut pas être remboursé à nouveau. Sans ce modèle explicite de ce qui est et n'est pas possible dans le domaine, le moteur de raisonnement automatisé peut détecter des problèmes d'ambiguïté, d'incohérence et d'incomplétude qui peuvent survenir dans des situations impossibles selon ces contraintes implicites. L'analyse des exigences telle que publiée aujourd'hui aborde cet aspect en échantillonnant plusieurs fois des assertions de connaissances d'arrière-plan à partir du LLM et en retenant un sous-ensemble selon un seuil de fréquence. Mais pour véritablement déverrouiller l'analyse des exigences à grande échelle, c'est dans la construction de bons modèles formels de domaine que réside le plus grand potentiel d'amélioration.

Analyse logique : trouver des contradictions et des lacunes

Avec un modèle formel en main, le moteur de raisonnement peut répondre de manière fiable à des questions telles que : existe-t-il une quelconque situation dans laquelle tous les critères d'acceptation tiennent simultanément? Existe-t-il une quelconque situation dans laquelle aucun d'entre eux ne s'applique? Existe-t-il une quelconque paire d'assertions dont les antécédents peuvent s'activer simultanément alors que leurs conséquents sont incohérents?

Voici un exemple pour concrétiser cela. Cinq critères d'acceptation pour un système de traitement de commandes, spécifiant l'interaction entre l'émission de commande, l'annulation de commande, les remboursements et la mise en attente de réapprovisionnement :

R1. WHEN an order is submitted AND inventory is available for the order, THE Order System SHALL fulfill the order.

R2. WHEN an order is submitted AND inventory is not available for the order, THE Order System SHALL place the order on backorder.

R3. THE Order System SHALL NOT place any order on backorder.

R4. WHEN an order is canceled, THE Order System SHALL refund all payments associated with the order.

R5. WHILE an order is in a canceled-and-refunded state, THE Order System SHALL NOT fulfill the order.

Chaque exigence semble raisonnable isolément. Mais l'ensemble dans son intégralité ne peut pas être implémenté parce qu'elles se contredisent. L'auto-formalisation produit un schéma avec quelques variables d'événement (order_submitted, order_canceled), quelques variables d'état (inventory_available, order_state), et quelques sorties (order_fulfilled, order_backordered, payments_refunded). Chaque exigence devient une seule implication :

Loading code example...

Le premier constat est un conflit évident. Nous demandons au moteur de raisonnement s'il existe une situation où les cinq règles tiennent et où la garde de R2 est active. Réponse : insatisfiable. Lorsqu'une commande est soumise et que l'inventaire n'est pas disponible, R2 exige que la commande soit mise en attente de réapprovisionnement, et R3, la règle omniprésente, interdit exactement cela. Le moteur retourne l'ensemble minimal de règles responsables de la contradiction : {R2, R3}. Un lecteur attentif pourrait repérer celui-ci à l'œil, mais le moteur le détecte automatiquement.

Le second constat est une contradiction conditionnelle impliquant plusieurs règles et un raisonnement par cas. Le moteur vérifie un scénario avec quatre conditions : la commande est dans un état annulé-et-remboursé, et un nouvel événement order_submitted arrive (imaginez un client resoumettant une commande précédemment annulée). Le moteur fait une distinction de cas sur la disponibilité de l'inventaire :

Inventaire disponible. R1 dit d'honorer. R5 dit de ne pas honorer. Il y a une contradiction sur la sortie order_fulfilled. Le sous-ensemble de règles contradictoires est {R1, R5}.
Inventaire non disponible. R2 dit de mettre en attente de réapprovisionnement. R3 dit de ne pas mettre en attente de réapprovisionnement. Il y a une contradiction sur la sortie order_backordered. Le sous-ensemble de règles contradictoires est {R2, R3}.

Dans tous les cas, aucune implémentation ne peut satisfaire les cinq règles, puisqu'il n'existe aucun chemin réalisable à travers ces règles qui n'entraîne pas de contradiction logique.

Le troisième constat est une lacune de complétude. Nous demandons au moteur de raisonnement : existe-t-il une situation dans laquelle aucune de R1, R2, R4 ou R5 ne s'applique? (R3 est omniprésente et s'applique toujours, mais c'est exactement le point : une règle omniprésente ne définit pas de comportement pour un scénario particulier, elle impose simplement une contrainte générale.) Réponse : oui. Lorsque order_submitted = false, order_canceled = false, et que la commande n'est pas annulée-et-remboursée, aucune des règles ne se déclenche. La commande peut être présente dans le système mais se trouver dans un état où aucune règle n'indique au système quoi faire. Pour rendre la spécification complète, nous devons ajouter une règle supplémentaire décrivant le comportement attendu du système dans cette situation.

Le moteur de raisonnement automatisé produit deux autres types de constats :

scénarios acceptés : des exemples de comportements concrets du système permis par les exigences
scénarios rejetés : des exemples de comportements concrets du système interdits par les exigences

Ces comportements sont échantillonnés directement à partir du modèle formel, et peuvent aider l'utilisateur à confirmer que son intention a été fidèlement capturée (on peut voir la génération de scénarios comme « simuler la spécification »). Cependant, il peut y avoir bien trop de scénarios à montrer. Pour éviter de submerger l'utilisateur de scénarios, nous utilisons un juge basé sur un LLM pour analyser chaque scénario dans le contexte de l'histoire utilisateur. En essence, nous demandons au juge LLM de répondre à la question : « Le fait que ce comportement du système soit accepté (respectivement rejeté) est-il surprenant, compte tenu de ce que nous essayons d'accomplir dans l'histoire utilisateur? »

Pour les scénarios jugés surprenants, nous présentons à l'utilisateur une question décrivant le scénario accepté (respectivement rejeté) et offrant deux options. Option A : conserver l'exigence telle quelle; Option B : modifier l'exigence pour rejeter (respectivement accepter) le scénario. En choisissant l'option A, l'utilisateur reconnaît que ce scénario est accepté (ou rejeté) comme souhaité. En choisissant l'option B, l'utilisateur confirme que le scénario est surprenant, et déclenche une révision de l'exigence.

Conclusion

Les bogues d'exigences sont coûteux. Ils se propagent à travers la conception détaillée, dans la planification des tâches, et finalement dans le code, sont difficiles à détecter à la première lecture, et coûteux à corriger. La programmation assistée par l'IA augmente les enjeux, parce que le code généré à partir de spécifications vagues peut atteindre la production plus rapidement qu'aucun humain ne peut le réviser pour ces classes de bogues subtils.

L'analyse des exigences aide à rehausser la qualité de vos spécifications en trois étapes utilisant une approche neurosymbolique : Premièrement, le raffinement utilise un raisonnement piloté par un LLM pour transformer des exigences de niveau thèse en exigences plus vérifiables, sans solution, et plus cohérentes et complètes. Deuxièmement, l'auto-formalisation produit un modèle formel qui représente fidèlement le langage naturel, détectant l'ambiguïté sémantique à la volée et demandant une clarification lorsque nécessaire. Troisièmement, l'analyse logique utilise un moteur de raisonnement automatisé pour détecter les problèmes de cohérence et de complétude sur le modèle formel, et génère des scénarios illustrant les comportements du système acceptés et rejetés. Chaque constat est présenté sous forme de question concise avec deux options de réponse concrètes. Une fois que vous avez répondu aux questions, un LLM réécrit les exigences concernées pour refléter explicitement vos choix, produisant une spécification mise à jour qui est mieux alignée avec votre intention, prête pour la conception détaillée et l'implémentation.

Notes

La notation EARS que Kiro utilise dans les documents d'exigences
Le Guide de rédaction des exigences de l'INCOSE codifie les propriétés des exigences de manière plus détaillée
Larbi, M., Akli, A., Papadakis, M., Bouyousfi, R., Cordy, M., Sarro, F., & Le Traon, Y. (2025). When Prompts Go Wrong: Evaluating Code Model Robustness to Ambiguous, Contradictory, and Incomplete Task Descriptions. https://arxiv.org/abs/2507.20439.
Yang, C., Shi, Y., Ma, Q., Liu, M. X., Kästner, C., & Wu, T. (2025). What Prompts Don't Say: Understanding and Managing Underspecification in LLM Prompts. arXiv preprint arXiv:2505.13360.
Norheim JJ, Rebentisch E, Xiao D, Draeger L, Kerbrat A, de Weck OL. Challenges in applying large language models to requirements engineering tasks. Design Science. 2024;10:e16. doi:10.1017/dsj.2024.8.

Analyse des exigences : détecter les bogues d'exigences avant qu'ils ne deviennent du code