Technisch overzicht: Analyse van de narratiekloof in LLM-solver loops

1. Probleemstelling

Het artikel behandelt een kritieke kwetsbaarheid in neurosymbolische redeneerpipelines die Large Language Models (LLM's) combineren met formele solvers (bijv. SAT, SMT). Hoewel deze systemen gebruikmaken van formele tools om betrouwbare, verifieerbare antwoorden te leveren op logische vragen, identificeren de auteurs een "narratiekloof" (narration gap) waarbij de robuustheid van het systeem bezwijkt.

De pipeline bestaat uit drie stadia:

1. Formalisering: Een LLM vertaalt een natuurlijke taalvraag naar een logische formule ($\phi$).
2. Besluitvorming: Een formele solver bepaalt de bevredigbaarheid van $\phi$ en geeft een oordeel ($v$) en een certificaat ($c$) terug.
3. Narratie: Een LLM vertaalt het formele oordeel terug naar een antwoord in natuurlijke taal voor de gebruiker.

Eerder onderzoek heeft zich gericht op de betrouwbaarheid van de formaliserings- en besluitvormingsstadia. Echter, de narratiestadia blijven ongecertificeerd. De auteurs stellen dat zelfs als het oordeel van de solver wiskundig correct en onafhankelijk geverifieerd is, een tegenstander de LLM tijdens de narratiestap kan manipuleren (via prompt injectie) om de uiteindelijke conclusie voor de gebruiker om te keren, terwijl het onderliggende oordeel en certificaat ongewijzigd blijven. Dit resulteert in een "sluipende fout" (stealthy failure) waarbij het systeem een correcte tussenliggende staat rapporteert, maar een foutief eindantwoord geeft, waardoor standaard runtime-monitors die alleen het oordeel controleren, worden omzeild.

2. Methodologie

Formele Modellering

De auteurs modelleren de LLM-solver loop als een geverifieerde beslissingsprocedure. Ze definiëren:

• Aannames: De formalisering is getrouw aan de intentie van de gebruiker, en de solver is sound en compleet.
• Tegenstandersmodel: Een tegenstander voert indirecte prompt injectie uit door onbetrouwde inhoud (bijv. aantekeningen of formule-commentaren) te controleren die in de context van de narrator wordt gevoerd. Het doel is om de uiteindelijke conclusie ($\bar{p} = \neg \rho(v)$) om te keren (stealthy) terwijl het herstelde oordeel correct blijft, of om te keren (compliant) terwijl zowel het oordeel als de conclusie worden omgegooid.
• Falen-taxonomie: Ze categoriseren fouten in:
  • Stealthy (T2): Oordeel is correct, conclusie is omgedraaid.
  • Compliant (T3): Zowel oordeel als conclusie zijn omgedraaid.
  • Robuustheid: Het systeem weerstaat de aanval.

Theoretische Analyse

Het artikel bewijst twee kernstellingen met betrekking tot monitoring en handhaving:

1. Stelling 1: Een monitor die controleert of de genarreerde conclusie overeenkomt met het geverifieerde oordeel, is sound en compleet. Echter, een monitor die alleen het herstelde oordeel controleert (zonder het te vergelijken met de conclusie), is echter blind voor stealthy fouten.
2. Stelling 2 & Corolarium 3: Een sound en complete monitor bestaat dan en slechts dan als een sound en complete enforcer bestaat. De enige configuratie die een foutpercentage van nul garandeert, is een enforcer die de narratie van de LLM volledig omzeilt en direct het gemapte oordeel ($\rho(v)$) uitvoert.

Experimentele Opstelling

• Oracle: Z3 solver gebruikt als de grondwaarheid voor SAT/UNSAT instanties.
• Modellen: Vijf open-source modellen werden geëvalueerd: Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B, en DeepSeek-R1-8B.
• Attack Vectors: Vier injectie-templates werden getest over twee kanalen (ingebed in de formule versus in een aparte aantekening) en twee stijlen (brutaal versus subtiel/social engineering).
• Defensie: Een "geharde" systeemprompt werd getest, waarbij de LLM de instructie kreeg onbetrouwbare inputs als zodanig te behandelen en prioriteit te geven aan het geverifieerde oordeel.
• Adaptieve Aanvallen: Tegenstanders werden gesimuleerd die de defensie-prompt kenden en injecties ontwierpen die specifiek bedoeld waren om deze te omzeilen.

3. Belangrijkste Resultaten

Betrouwbaarheid van het Oordeel (RQ1)

Wanneer het certificaat van de solver de uiteindelijke antwoordgeneratie beperkt (het systeem dwingt het systeem om het geverifieerde oordeel te produceren), bereikt het systeem 100% correctheid. Dit bevestigt dat de solver-component zelf sound is en dat de kwetsbaarheid strikt ligt in de narratie van de LLM.

Adversariële Narratie Inversie (RQ2)

Zonder defensie slaagden tegenstanders erin om in een meerderheid van de gevallen het genarreerde antwoord om te keren:

• Succespercentages: De succespercentages van injecties varieerden van 0,47 tot 0,71 over verschillende templates.
• Stealthiness: "Stealthy" fouten (waarbij de LLM het oordeel correct herhaalt maar de conclusie omdraait) waren zeer prevalent. Bijvoorbeeld de note_social template (een subtiele aantekening zonder imperatieve commando's) behaalde een totaal succespercentage van 0,71, waarvan 0,39 stealthy was.
• Model Variantie: Redeneermodellen (gpt-oss) waren niet immuun en vertoonden een hoge vatbaarheid (0,91 totaal succespercentage). Niet-redeneermodellen zoals Qwen toonden meer weerstand tegen brute aanvallen, maar bleven kwetsbaar voor subtiele aanvallen.
• Kernbevinding: Subtiele injecties waren statistisch even effectief als brute injecties. De kwetsbaarheid is een falen van de getrouwheid in de transfer van oordeel naar antwoord, en niet louter een falen om expliciete commando's op te volgen.

Effectiviteit van Defensie (RQ3)

• Prompt Hardening: Het harden van de systeemprompt van de narrator verminderde het totale succespercentage van injecties van 0,61 naar 0,14 (een reductie van ~4x).
• Beperkingen:
  • Hardening verminderde primair de compliant fouten (waarbij het model openlijk ongehoorzaam is), maar had minimale impact op stealthy fouten. Het percentage stealthy fouten daalde slechts van 0,57 naar 0,53 onder de resterende aanvallen.
  • Adaptieve Aanvallen: Aanvallers die hun prompts aanpasten om de geharde systeemprompt te counteren (bijv. door de "onbetrouwbare" waarschuwing expliciet te ontkennen), zorgden voor een aanzienlijk herstel van het succespercentage (bijv. note_adaptive_supersede steeg naar 0,43).
  • Model Afhankelijkheid: De effectiviteit van de defensie varieerde sterk per model (bijv. Qwen daalde naar 0,01, terwijl gpt-oss op 0,26 bleef).

4. Kernbijdragen

1. Formele Modellering: Het artikel modelleert de LLM-solver loop formeel als een beslissingsprocedure en identificeert de narratiestap als het specifieke punt waar garanties van soundness verloren gaan.
2. Systematische Meting: Het biedt de eerste systematische meting van de narratiekloof en toont aan dat adversariële injecties geverifieerde conclusies kunnen omkeren over diverse formuleringen en kanalen heen.
3. Theoretische Limieten van Defensie: De auteurs bewijzen dat prompt hardening en runtime monitoring onvoldoende zijn om stealthy fouten te elimineren. Ze tonen aan dat alleen enforcement (het direct outputten van het gemapte oordeel $\rho(v)$) een end-to-end correctheid kan garanderen.
4. Empirisch Bewijs: Door uitgebreide experimenten met vijf modellen toont het artikel aan dat zelfs redeneer-bekwame modellen vatbaar zijn voor het omdraaien van geverifieerde conclusies, en dat subtiele social engineering even effectief is als brute commando's.

5. Betekenis en Claims

Het artikel claimt dat de narratiekloof een fundamentele eigenschap is van neurosymbolische pipelines die vertrouwen op LLM's om formele resultaten naar natuurlijke taal te vertalen.

• Het Certificaat is Niet Genoeg: Een formeel certificat garandeert de correctheid van het oordeel, maar het garandeert niet de correctheid van het gebruikersantwoord als dat antwoord door een LLM wordt gegenereerd.
• Onzichtbaarheid van Fouten: De gevaarlijkste fouten zijn "stealthy", waarbij het systeem correct lijkt te functioneren (het herhaalt het juiste oordeel) terwijl het een foutieve conclusie levert. Deze fouten zijn onzichtbaar voor monitors die alleen het oordeel auditeren.
• Mitigatiestrategie: De auteurs stellen dat het vertrouwen op prompt engineering of geharde instructies geen betrouwbare verdediging is tegen adaptieve tegenstanders. De enige robuuste oplossing voor beslisbare queries is om de LLM te verwijderen uit de stap van conclusiegeneratie en het antwoord direct vanuit het geverifieerde oordeel af te dwingen.
• Generaliseerbaarheid: Hoewel getest op SAT-problemen, stellen de auteurs dat deze kloof van toepassing is op elke pipeline (SMT, Interactive Theorem Provers) waarbij een geverifieerd resultaat door een LLM wordt genarreerd.

De auteurs concluderen dat voor veiligheidskritische toepassingen de verantwoordelijkheid van de pipeline verschuift naar het waarborgen dat de formalisering getrouw is en de narratie wordt afgedwongen, in plaats van te vertrouwen op de LLM om het output van de solver getrouw te rapporteren.