Technische Samenvatting: Agentische Interpretatie voor LLM-gebaseerde Programma-analyse

1. Probleemstelling

Grote Taalmodellen (LLM's) bieden unieke mogelijkheden voor programma-analyse door toegang te krijgen tot informatie buiten de broncode om, zoals documentatie, beveiligingsadviezen, metadata specifiek voor versies en informele API-contracten. Het vertrouwen op LLM's voor "one-shot" analyse van het volledige programma is echter inherent kwetsbaar om drie hoofdzaken:

1. Contextgevoeligheid: Empirische studies wijzen uit dat de prestaties van modellen verslechteren naarmate de contextlengte en taakcomplexiteit toenemen, en dat resultaten sterk afhankelijk zijn van de volgorde van informatie in de prompt. Kritiek bewijsmateriaal (bijvoorbeeld een specifiek beveiligingsadvies) kan worden aangeleverd maar niet betrouwbaar worden benut.
2. Gebrek aan persistente staat: Monolithische LLM-antwoorden missen een persistente staat om bij te houden welke specifieke claims werden ondersteund, weerlegd of open gelaten. Dit maakt het moeilijk om met zelfcontradictief redeneren om te gaan of met redenering die de eigen conclusies niet ondersteunt.
3. Afwezigheid van afhankelijkheidsstructuur: Een single-shot antwoord biedt geen mechanisme voor feedback. Als latere bevindingen onthullen dat een eerdere vraag verkeerd was afgebakend of dat een upstream-component onder een andere hypothese opnieuw moet worden onderzocht, kan een ongestructureerd antwoord deze iteratieve verfijning niet faciliteren.

Gevolg hiervan is dat er behoefte is aan een raamwerk dat de kloof overbrugt tussen ad-hoc LLM-prompting en volledig gespecificeerde statische analyse, specifiek voor evidence-afhankelijke programma-analyses waarbij de relevante feiten niet volledig in de broncode of formele specificaties zijn opgenomen.

2. Methodologie: Agentische Interpretatie

Het artikel stelt Agentische Interpretatie voor, een raamwerk dat de discipline van roostergebaseerde statische analyse toepast op door LLM's gestuurd redeneren. De methodologie decomposeert hoogwaardige analyse-doelen in gelokaliseerde claims die verankerd zijn bij programmapunten en componentgrenzen, en beheert hun evolutie via een rooster met eindige hoogte en een werklijst-algoritme.

2.1 Kerncomponenten

• Evaluatiegraaf ($G^*$): Een uitbreiding van een uit het programma afgeleide graaf ($G_{prog}$) die omvat:
  • Hulpknooppunten: Knooppunten die interacties tussen componenten of doelen vertegenwoordigen die niet corresponderen met een enkel programmapunt.
  • Contextranden: Voorwaarts stromende randen die ervoor zorgen dat wanneer een claim bij knooppunt $n$ wordt geëvalueerd, deze de huidige beoordelingsstatus en het bewijsmateriaal van zijn voorgangers ontvangt.
  • Feedbackranden: Achterwaarts stromende randen die een her-evaluatie van upstream-knooppunten triggeren wanneer een downstream-beoordeling verandert (bijvoorbeeld: een weerlegde compositieclaim triggert een gerichte zoektocht in een ondoorzichtige component).
• Beoordelingsdomein (Rooster): Een join-halfrooster met eindige hoogte ($A$) dat de bewijsstatus van een claim samenvat.
  • Het artikel illustreert dit met het AGraded-rooster: $\{ \perp, w, s \} \times \{ \perp, w, s \}$, waarbij de eerste coördinaat ondersteunend bewijs vertegenwoordigt en de tweede weerleggend bewijs. Waarden variëren van afwezig ($\perp$) tot zwak ($w$) tot sterk ($s$).
  • Het rooster is een epistemisch domein over bewijsstaten, geen abstract domein over concrete programmastaten. Het registreert of een claim is ondersteund of weerlegd en de sterkte van dat bewijs.
• Werklijst-harnas: Een controlelus die de analysestatus beheert.
  • Contextualisatie: Voor een knooppunt $n$ construeert het harnas een prompt-context ($\Gamma_n$) met behulp van broncode, het hoogwaardige doel en de huidige beoordelingen van voorgaande knooppunten.
  • Knooppunt-transformatoren: De LLM-agent voert twee bewerkingen uit:
    1. Evaluatie: Beoordeelt bestaande claims tegen de context en geeft een bijgewerkte beoordeling en bewijsregistraties terug.
    2. Generatie: Stelt nieuwe, relevante claims voor op basis van de context.
  • Propagatie: Als de join van de nieuwe beoordeling met de oude beoordeling resulteert in een strikte toename in de roosterorde, worden de uitgebreide opvolgers van het knooppunt in de wachtrij geplaatst voor her-evaluatie.

2.2 Het Analyseproces

Het proces wordt geïllustreerd aan de hand van een beveiligingsreview van een programma met ondoorzichtige derden-componenten (een JSON-parser en een handtekeningverificatie).

1. Initialisatie: De werklijst wordt gezaaid met alle programma- en hulpknooppunten.
2. Iteratieve Verfijning:
   • Fase I: Initiële onafhankelijke beoordeling van componenten (bijvoorbeeld het reviewen van documentatie voor de parser en verificatie).
   • Fase II: Compositie van bewijs. Het raamwerk evalueert claims tussen componenten (bijvoorbeeld: "Zorgen de componenten gezamenlijk voor veiligheid?"). Als een compositieclaim zwak wordt weerlegd, triggeren feedbackranden een heronderzoek van upstream-componenten.
   • Fase III: Feedback-gedreven verfijning. De context van de weerlegde compositie (bijvoorbeeld: "de processor voert geen validatie uit") leidt de LLM om een gerichte zoektocht te doen naar specifieke kwetsbaarheden (bijvoorbeeld prototype-verontreiniging) in plaats van een brede review.
   • Fase IV: Stabilisatie. De versterkte upstream-bewijzen stromen voorwaarts, wat leidt tot een sterke weerlegging van het globale doel. De werklijst raakt leeg wanneer er geen verdere strikte toename in beoordeling meer optreedt.

3. Belangrijkste Bijdragen

Het artikel levert drie primaire bijdragen:

1. Raamwerkpresentatie: Het introduceert Agentische Interpretatie als een gestructureerde aanpak voor evidence-afhankelijke programma-analyse, en identificeert een geschikt probleemdomein waar LLM's noodzakelijk zijn maar directe prompting ontoereikend is.
2. Formeel Model: Het formaliseert het kernmodel, met definitie van de evaluatiegraaf, het beoordelingsdomein, knooppunt-transformatoren en het werklijst-algoritme.
3. Karakterisering van Ontwerpruimte: Het verkent de ontwerpruimte, inclusief:
   • Beoordelingsroosters: Discussie over afwegingen tussen grove roosters (bijvoorbeeld aanwezigheid/afwezigheid) en fijnmazige roosters (bijvoorbeeld sterkte, basis van vertrouwen). Het introduceert AStratified, een domein dat bewijssterkte en basis van vertrouwen (bijvoorbeeld "alleen model" versus "gecontroleerd") apart bijhoudt.
   • Claimbeheer: Aanpak van claimcanonicalisatie, granulariteit en scope.
   • Query-ontwerp: Differentiatie tussen evaluatiequeries (ondersteuning/weerlegging) en generatieve queries (voorstel van nieuwe claims).
   • Terminatie: Bewijs dat het algoritme terminateert voor roosters met eindige hoogte en beperkte claimgeneratie, zelfs in aanwezigheid van niet-deterministische LLM-antwoorden, mits updates monotoon zijn (via join).

4. Resultaten en Beperkingen

• Resultaten: Het artikel biedt een uitgewerkt voorbeeld (een beveiligingsreview van een handler met ondoorzichtige componenten) dat laat zien hoe het raamwerk een doel decomposeert, feedbacklussen gebruikt om de zoektocht te verfijnen, en stabiliseert op een definitieve beoordeling. Het toont aan hoe het raamwerk kan detecteren dat een globaal beveiligingsdoel wordt geschonden door zwak bewijs uit meerdere bronnen te combineren tot een sterke weerlegging.
• Beperkingen:
  • Het artikel beschrijft werk in uitvoering. Het bevat geen praktische implementatie of experimentele evaluatie.
  • Het raamwerk garandeert terminatie en begrensbaarheid, maar garandeert geen soundness in de traditionele zin (het bewijst namelijk niet dat de conclusies van de LLM correct zijn). Het maakt de evidentiële rol van de LLM expliciet en controleerbaar.
  • Het raamwerk kan een agent die consequent bewijsmateriaal verkeerd inschat, niet corrigeren; het maakt dergelijke fouten alleen zichtbaar.
  • Het bewijs van terminatie rust op de aanname dat claims nooit worden ingetrokken en beoordelingen alleen toenemen via join. Mechanismen voor geloofsrevisionie (verlagen van beoordelingen) worden besproken als toekomstig werk dat beperkte vervanging of epochale herberekening vereist.

5. Betekenis

De betekenis van dit werk ligt in de poging om structurele discipline te brengen in door LLM's gestuurd redeneren binnen programma-analyse. Door weg te bewegen van het "genereren-en-controleren"-paradigma (waarvoor een formele verificateur voor de output van de LLM vereist is) en het "heuristische orakel"-paradigma (waarbij de LLM de soundness niet kan beïnvloeden), richt Agentische Interpretatie zich op een middenweg.

Het is significant voor evidence-afhankelijke analyses waarbij:

• De relevante feiten niet formaliseerbaar zijn (bijvoorbeeld informele API-contracten, beveiligingsadviezen).
• Er geen complete verificateur bestaat.
• De analyse informatie moet synthetiseren uit diverse, niet-code bronnen.

Het raamwerk transformeert de LLM van een black-box generator naar een begrensde, controleerbare component van een groter analysesysteem. Het zorgt ervoor dat de analyse op een gecontroleerde, principiële manier verloopt, waardoor scheiding van belangen mogelijk wordt: de LLM levert bewijs, en het roostergebaseerde harnas zorgt ervoor dat de analyse begrensbaar en traceerbaar is. Deze aanpak beoogt toekomstige discussies te inspireren over het ontwerpen van formeel onderbouwde technieken voor agentische systemen in programma-analyse.