Résumé technique : Analyse de l'écart de narration dans les boucles LLM-Solver

1. Énoncé du problème

L'article traite d'une vulnérabilité critique dans les pipelines de raisonnement neurosymbolique qui combinent des modèles de langage de grande taille (LLM) avec des solveurs formels (ex. : SAT, SMT). Bien que ces systèmes exploitent des outils formels pour fournir des réponses saines et vérifiables à des questions logiques, les auteurs identifient un « écart de narration » (narration gap) où la robustesse du système se dégrade.

Le pipeline se compose de trois étapes :

1. Formalisation : Un LLM traduit une requête en langage naturel en une formule logique ($\phi$).
2. Décision : Un solveur formel détermine la satisfaisabilité de $\phi$, retournant un verdict ($v$) et un certificat ($c$).
3. Narration : Un LLM traduit le verdict formel en une réponse en langage naturel pour l'utilisateur.

La recherche préalable s'est concentrée sur la correction de la formalisation et des étapes de décision. Cependant, l'étape de narration reste non certifiée. Les auteurs soutiennent que même si le verdict du solveur est mathématiquement sain et vérifié de manière indépendante, un adversaire peut manipuler le LLM lors de l'étape de narration (via une injection de prompt) pour inverser la conclusion finale présentée à l'utilisateur tout en laissant le verdict et le certificat sous-jacents intacts. Cela entraîne un « échec furtif » (stealthy failure) où le système rapporte un état intermédiaire correct mais une réponse finale erronée, échappant ainsi aux moniteurs d'exécution standards qui ne vérifient que le verdict.

2. Méthodologie

Modélisation formelle

Les auteurs modélisent la boucle LLM-solver comme une procédure de décision vérifiée. Ils définissent :

• Hypothèses : La formalisation est fidèle à l'intention de l'utilisateur, et le solveur est sain et complet.
• Modèle d'adversaire : Un adversaire réalise une injection de prompt indirecte en contrôlant un contenu non fiable (ex. : notes ou commentaires de formules) injecté dans le contexte du narrateur. Le but est d'inverser la conclusion finale ($\bar{p} = \neg \rho(v)$) tout en maintenant le verdict restitué correct (furtif) ou incorrect (conforme).
• Taxonomie des échecs : Ils catégorisent les échecs en :
  • Furtif (T2) : Le verdict est correct, la conclusion est inversée.
  • Conforme (T3) : Le verdict et la conclusion sont tous deux inversés.
  • Robustesse : Le système résiste à l'attaque.

Analyse théorique

L'article prouve deux théorèmes clés concernant la surveillance et l'application :

1. Théorème 1 : Un moniteur qui vérifie si la conclusion narrée correspond au verdict vérifié est sain et complet. Cependant, un moniteur qui vérifie uniquement le verdict restitué (sans le comparer à la conclusion) est aveugle aux échecs furtifs.
2. Théorème 2 & Corollaire 3 : Un moniteur sain et complet existe si et seulement si un exécuteur (enforcer) sain existe. La seule configuration qui garantit un taux d'inversion nul est un exécuteur qui contourne entièrement la narration du LLM, en extrayant directement le verdict mappé ($\rho(v)$).

Configuration expérimentale

• Oracle : Le solveur Z3 est utilisé comme vérité de terrain pour les instances SAT/UNSAT.
• Modèles : Cinq modèles open-source ont été évalués : Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B, et DeepSeek-R1-8B.
• Vecteurs d'attaque : Quatre modèles d'injection ont été testés à travers deux canaux (intégrés dans la formule ou dans une note séparée) et deux styles (blatant/direct ou subtil/ingénierie sociale).
• Défense : Un prompt système « durci » a été testé, instruisant le LLM de traiter les entrées non fiables comme telles et de donner la priorité au verdict vérifié.
• Attaques adaptatives : Des attaquants ont été simulés, connaissant le prompt de défense, et ont conçu des injections spécifiquement pour contourner celui-ci.

3. Résultats clés

Correction du verdict (RQ1)

Lorsque le certificat du solveur verrouille la réponse finale (forçant le système à produire le verdict vérifié), le système atteint une correction de 100 %. Cela confirme que le composant solveur est sain et que la vulnérabilité réside strictement dans la narration du LLM.

Inversion de la narration par un adversaire (RQ2)

Sans défense, les adversaires réussissent à inverser la réponse narrée dans la majorité des cas :

• Taux de succès : Les taux de succès d'injection variaient de 0,47 à 0,71 selon les modèles d'injection.
• Furtivité : Les échecs « furtifs » (où le LLM restitue correctement le verdict mais inverse la conclusion) étaient très fréquents. Par exemple, le modèle note_social (une note subtile sans commandes impératives) a atteint un taux de succès global de 0,71, dont 0,39 étaient furtifs.
• Variance des modèles : Les modèles de raisonnement (gpt-oss) n'étaient pas immunisés, montrant une forte susceptibilité (taux de succès global de 0,91). Les modèles non orientés raisonnement comme Qwen présentaient une plus grande résistance aux attaques directes, mais restaient vulnérables aux attaques subtiles.
• Résultat clé : Les injections subtiles étaient statistiquement aussi efficaces que les injections directes. La vulnérabilité est un défaut de fidélité dans le transfert du verdict vers la réponse, et non simplement un défaut de respect des commandes explicites.

Efficacité de la défense (RQ3)

• Durcissement du prompt : Le durcissement du prompt système du narrateur a réduit le taux de succès global de l'injection de 0,61 à 0,14 (une réduction d'environ 4x).
• Limites :
  • Le durcissement a principalement réduit les échecs conformes (où le modèle désobéit ouvertement) mais a eu un impact minimal sur les échecs furtifs. Le taux d'échecs furtifs n'est passé que de 0,57 à 0,53 parmi les attaques restantes.
  • Attaques adaptatives : Les attaquants qui ont adapté leurs prompts pour contrer le système durci (ex. : en niant explicitement l'avertissement « non fiable ») ont vu leur taux de succès remonter significativement (ex. : note_adaptive_supersede est passé à 0,43).
  • Dépendance au modèle : L'efficacité de la défense variait énormément selon le modèle (ex. : Qwen est descendu à 0,01, tandis que gpt-oss est resté à 0,26).

4. Principales contributions

1. Modélisation formelle : L'article modélise formellement la boucle LLM-solver comme une procédure de décision, identifiant l'étape de narration comme le point précis où les garanties de correction sont perdues.
2. Mesure systématique : Il fournit la première mesure systématique de l'écart de narration, démontant que des injections adverses peuvent inverser des conclusions vérifiées à travers diverses formulations et canaux.
3. Limites théoriques de la défense : Les auteurs prouvent que le durcissement des prompts et la surveillance au runtime sont insuffisants pour éliminer les échecs furtifs. Ils démontent que seul l'exécution (en extrayant directement le verdict mappé $\rho(v)$) peut garantir une correction de bout en bout.
4. Preuve empirique : À travers des expériences étendues sur cinq modèles, l'article montre que même les modèles capables de raisonnement sont susceptibles d'inverser des conclusions vérifiées et que l'ingénierie sociale subtile est aussi efficace que les commandes directes.

5. Signification et affirmations

L'article affirme que l'écart de narration est une propriété fondamentale des pipelines neurosymboliques qui dépendent des LLM pour traduire des résultats formels en langage naturel.

• Le certificat ne suffit pas : Un certificat formel garantit la correction du verdict, mais il ne garantit pas la correction de la réponse utilisateur si cette dernière est générée par un LLM.
• Invisibilité de l'échec : Les échecs les plus dangereux sont les échecs « furtifs », où le système semble fonctionner correctement (restituant le bon verdict) tout en délivrant une conclusion erronée. Ces échecs sont invisibles pour les moniteurs qui n'auditent que le verdict.
• Stratégie d'atténuation : L'article soutient que compter sur le prompt engineering ou des instructions durcies n'est pas une défense fiable contre des adversaires adaptatifs. La seule solution robuste pour les requêtes décidables est de retirer le LLM de l'étape de génération de la conclusion et d'imposer la réponse directement à partir du verdict vérifié.
• Généralisabilité : Bien que testé sur des problèmes SAT, les auteurs affirment que cet écart s'applique à tout pipeline (SMT, prouveurs de théorèmes interactifs) où un résultat vérifié est narré par un LLM.

Les auteurs concluent que pour les applications critiques, la responsabilité du pipeline consiste à s'assurer que la formalisation est fidèle et que la narration est imposée, plutôt que de faire confiance au LLM pour rapporter fidèlement la sortie du solveur.