Preprint upozorňuje na naratívnu medzeru v slučkách medzi LLM a formálnym solverom

Formálne nástroje, ako sú SAT a SMT solvery, sa čoraz častejšie objavujú v reťazcoch s veľkými jazykovými modelmi. Dôvod je zrejmý: pri bezpečnostne alebo technicky kritickej otázke môže solver poskytnúť odpoveď, ktorá nie je iba pravdepodobným textom, ale výsledkom overiteľného rozhodovacieho postupu. Nový preprint Analyzing the Narration Gap in LLM-Solver Loops však upozorňuje, že záruka solvera sa môže oslabiť v poslednom kroku – keď model výsledok vysvetľuje človeku. Autori túto slabinu nazývajú naratívna medzera.

Typická hybridná slučka má tri časti. Najprv sa prirodzená otázka preloží do formálneho zadania, napríklad logickej formule alebo obmedzení. Potom solver rozhodne, či je zadanie splniteľné, nájde príklad alebo potvrdí nesplniteľnosť. Nakoniec sa výsledok preloží späť do ľudskej odpovede. Výskum sa doteraz často sústredil na prvé dve fázy: či model správne formalizuje úlohu a či solver správne počíta. Preprint tvrdí, že rovnako dôležitá je tretia fáza, pretože používateľ zvyčajne nečíta surový dôkaz alebo model solvera, ale naratívnu odpoveď vytvorenú LLM.

Problém je nenápadný. Solver môže vyprodukovať správny a nezávisle overiteľný výsledok, no jazykový model ho môže pri vysvetlení zjednodušiť, obrátiť význam, doplniť nepodložený dôsledok alebo nejasne opísať hranice platnosti. Používateľ potom dostane text, ktorý pôsobí sebavedomo a odvoláva sa na formálny nástroj, ale v skutočnosti už nezodpovedá presne tomu, čo solver dokázal. V bezpečnostných workflowoch je to mimoriadne rizikové: tím môže veriť, že odpoveď je formálne garantovaná, hoci garantovaná bola iba jedna vnútorná časť procesu.

Téma je dôležitá pre všetky systémy, ktoré kombinujú LLM s externými verifikátormi. Patrí sem generovanie kódu s testami, automatizovaná kontrola konfigurácií, formálne dôkazy, hľadanie zraniteľností aj rozhodovanie o prístupových pravidlách. V každom prípade môže vzniknúť lákavá skratka: ak solver niečo potvrdil, model to „pekne vysvetlí“ a človek nemusí čítať technický výstup. Preprint pripomína, že práve tento preklad je súčasťou bezpečnostnej hranice, nie iba kozmetický krok.

Naratívna medzera súvisí aj s tým, ako hodnotíme agentické systémy. Ak benchmark meria iba to, či sa agent dopracoval k správnemu rozhodnutiu solvera, môže prehliadnuť, že finálna odpoveď používateľovi je zavádzajúca. Pri reálnom nasadení však rozhoduje finálny text, nie interný log. Autori preto smerujú pozornosť k potrebe kontrolovať konzistenciu medzi formálnym výstupom a naratívom. Prakticky to môže znamenať šablónované odpovede, povinné citovanie presného solver výstupu, automatickú kontrolu tvrdení v závere alebo oddelenie vysvetľujúcej vrstvy od rozhodovacej vrstvy.

Pre vývojárov AI nástrojov je najdôležitejšie nepreceňovať slovo „overené“. Ak agent povie, že odpoveď overil solverom, treba vedieť, čo presne bolo overené: pôvodná otázka, jej formalizácia, konkrétny model, alebo iba jedna redukovaná verzia problému. Rovnako treba vidieť, či finálne odporúčanie obsahuje dodatočné tvrdenia, ktoré solver nikdy neposudzoval. Táto disciplína je podobná práci s citáciami pri vyhľadávaní: zdroj môže byť pravý, no odpoveď ho môže interpretovať nesprávne.

Preprint má širší význam aj pre regulované aplikácie. V zdravotníctve, kyberbezpečnosti, financiách alebo pri právnych rozhodnutiach sa bude čoraz častejšie používať argument, že AI systém má oporu vo formálnej kontrole alebo externom nástroji. Ak však audit sleduje len to, že nástroj bol zavolaný, a nie to, či výsledná komunikácia presne odráža jeho výstup, vznikne falošný pocit bezpečia. Naratívna medzera je preto auditný problém: treba logovať nielen vstup a výstup solvera, ale aj transformáciu do odpovede a jej súlad s formálnym výsledkom.

Zaujímavé je, že tento problém sa nedá vyriešiť len silnejším jazykovým modelom. Lepší model môže menej často zle vysvetľovať, no stále pracuje pravdepodobnostne a môže dopĺňať implicitné súvislosti. Robustnejší prístup bude pravdepodobne kombinovať obmedzený jazyk pre finálne tvrdenia, mechanické overovanie konzistencie a používateľské rozhranie, ktoré zobrazí aj pôvodný formálny výsledok. Inak sa solver stane skôr reputačnou pečaťou než skutočnou zárukou správnosti.

Pre slovenské tímy, ktoré budujú agentov nad internými pravidlami, databázami alebo bezpečnostnými kontrolami, je poučenie praktické. Nestačí pridať solver, test runner alebo policy engine a predpokladať, že systém je tým pádom dôveryhodný. Treba navrhnúť aj posledný meter komunikácie: ako agent vysvetlí, čo bolo dokázané, čo zostáva neisté a čo je len odporúčanie. Ak sa tento krok zanedbá, hybridné LLM-solver slučky môžu byť zradné práve preto, že spájajú objektívne vyzerajúci formálny nástroj s presvedčivým, ale nie vždy presným jazykom.