Résumé Technique : Interprétation Agentique pour l'Analyse de Programmes Basée sur les LLM

1. Énoncé du Problème

Les Modèles de Langage (LLM) offrent des capacités uniques pour l'analyse de programmes en accédant à des informations au-delà du code source, telles que la documentation, les avis de sécurité, les métadonnées spécifiques aux versions et les contrats d'API informels. Cependant, s'appuyer sur les LLM pour une analyse de programme complète en « un seul coup » est intrinsèquement fragile pour trois raisons principales :

1. Sensibilité au Contexte : Des études empiriques indiquent que les performances des modèles se dégradent à mesure que la longueur du contexte et la complexité de la tâche augmentent, et que les résultats dépendent fortement de l'ordre des informations dans l'invite. Des preuves critiques (par exemple, un avis de sécurité spécifique) peuvent être fournies mais non utilisées de manière fiable.
2. Absence d'État Persistant : Les réponses monolithiques des LLM manquent d'un état persistant pour suivre quelles affirmations spécifiques ont été étayées, réfutées ou laissées en suspens. Cela rend difficile la gestion des raisonnements auto-contradictoires ou des raisonnements qui échouent à soutenir leurs propres conclusions.
3. Absence de Structure de Dépendance : Une réponse en un seul coup ne fournit aucun mécanisme de rétroaction. Si des découvertes ultérieures révèlent qu'une question antérieure était mal délimitée ou qu'un composant en amont doit être réexaminé sous une hypothèse différente, une réponse non structurée ne peut pas faciliter cette raffinement itératif.

Par conséquent, il existe un besoin d'un cadre qui comble le fossé entre l'invite aléatoire de LLM et l'analyse statique entièrement spécifiée, spécifiquement pour les analyses de programmes dépendantes des preuves, où les faits pertinents ne sont pas entièrement contenus dans le code source ou les spécifications formelles.

2. Méthodologie : Interprétation Agentique

L'article propose l'Interprétation Agentique, un cadre qui applique la discipline de l'analyse statique basée sur les treillis au raisonnement piloté par les LLM. La méthodologie décompose les objectifs d'analyse de haut niveau en affirmations localisées ancrées aux points du programme et aux limites des composants, en gérant leur évolution à travers un treillis de hauteur finie et un algorithme de liste de travail.

2.1 Composants Principaux

• Graphe d'Évaluation ($G^*$) : Une extension d'un graphe dérivé du programme ($G_{prog}$) qui inclut :
  • Nœuds Auxiliaires : Des nœuds représentant des interactions inter-composants ou des objectifs qui ne correspondent pas à un seul point du programme.
  • Arêtes de Contexte : Des arêtes à flux direct assurant que lorsqu'une affirmation au nœud $n$ est évaluée, elle reçoit l'état d'évaluation actuel et les preuves de ses prédécesseurs.
  • Arêtes de Rétroaction : Des arêtes à flux inverse qui déclenchent la réévaluation des nœuds en amont lorsque l'évaluation en aval change (par exemple, une affirmation de composition réfutée déclenche une recherche ciblée dans un composant opaque).
• Domaine d'Évaluation (Treillis) : Un semi-treillis de jonction de hauteur finie ($A$) qui résume le statut probatoire d'une affirmation.
  • L'article illustre cela avec le treillis AGraded : $\{ \perp, w, s \} \times \{ \perp, w, s \}$, où la première coordonnée représente les preuves à l'appui et la seconde les preuves réfutatoires. Les valeurs vont de l'absence ($\perp$) à faible ($w$) jusqu'à fort ($s$).
  • Le treillis est un domaine épistémique sur les états de preuve, et non un domaine abstrait sur les états concrets du programme. Il enregistre si une affirmation a été étayée ou réfutée et la force de cette preuve.
• Harnais de Liste de Travail : Une boucle de contrôle qui gère l'état de l'analyse.
  • Contextualisation : Pour un nœud $n$, le harnais construit un contexte d'invite ($\Gamma_n$) en utilisant le code source, l'objectif de haut niveau et les évaluations actuelles des nœuds prédécesseurs.
  • Transformateurs de Nœuds : L'agent LLM effectue deux opérations :
    1. Évaluation : Évalue les affirmations existantes par rapport au contexte, renvoyant une évaluation mise à jour et des enregistrements de preuves.
    2. Génération : Propose de nouvelles affirmations pertinentes basées sur le contexte.
  • Propagation : Si la jonction de la nouvelle évaluation avec l'ancienne évaluation entraîne une augmentation stricte dans l'ordre du treillis, les successeurs étendus du nœud sont mis en file d'attente pour réévaluation.

2.2 Le Processus d'Analyse

Le processus est illustré par une revue de sécurité d'un programme comportant des composants tiers opaques (un analyseur JSON et un vérificateur de signature).

1. Initialisation : La liste de travail est amorcée avec tous les nœuds du programme et les nœuds auxiliaires.
2. Raffinement Itératif :
   • Phase I : Évaluation indépendante initiale des composants (par exemple, examen de la documentation pour l'analyseur et le vérificateur).
   • Phase II : Composition des preuves. Le cadre évalue les affirmations inter-composants (par exemple, « Les composants garantissent-ils conjointement la sécurité ? »). Si une affirmation de composition est faiblement réfutée, les arêtes de rétroaction déclenchent une réinvestigation des composants en amont.
   • Phase III : Raffinement piloté par la rétroaction. Le contexte de la composition réfutée (par exemple, « le processeur n'effectue aucune validation ») guide le LLM pour effectuer une recherche ciblée de vulnérabilités spécifiques (par exemple, pollution du prototype) plutôt qu'une revue large.
   • Phase IV : Stabilisation. Les preuves en amont renforcées se propagent vers l'avant, conduisant à une réfutation forte de l'objectif global. La liste de travail se vide lorsqu'aucune augmentation stricte supplémentaire de l'évaluation ne se produit.

3. Contributions Clés

L'article fait trois contributions principales :

1. Proposition de Cadre : Il introduit l'Interprétation Agentique comme une approche structurée pour l'analyse de programmes dépendante des preuves, identifiant un domaine de problème approprié où les LLM sont nécessaires mais où l'invite directe est insuffisante.
2. Modèle Formel : Il formalise le modèle de base, définissant le graphe d'évaluation, le domaine d'évaluation, les transformateurs de nœuds et l'algorithme de liste de travail.
3. Caractérisation de l'Espace de Conception : Il explore l'espace de conception, notamment :
   • Treillis d'Évaluation : Discutant des compromis entre les treillis grossiers (par exemple, présence/absence) et les treillis fins (par exemple, force, base de confiance). Il introduit AStratified, un domaine qui suit la force de la preuve et la base de confiance (par exemple, « uniquement modèle » vs « vérifié ») séparément.
   • Gestion des Affirmations : Abordant la canonicalisation des affirmations, la granularité et la portée.
   • Conception des Requêtes : Différenciant les requêtes d'évaluation (appui/réfutation) et les requêtes génératives (proposition de nouvelles affirmations).
   • Terminaison : Prouvant que l'algorithme termine pour les treillis de hauteur finie avec une génération d'affirmations bornée, même en présence de réponses non déterministes des LLM, à condition que les mises à jour soient monotones (via la jonction).

4. Résultats et Limites

• Résultats : L'article fournit un exemple travaillé (une revue de sécurité d'un gestionnaire avec des composants opaques) démontrant comment le cadre décompose un objectif, utilise des boucles de rétroaction pour affiner la recherche et se stabilise sur une évaluation finale. Il montre comment le cadre peut détecter qu'un objectif de sécurité global est violé en combinant des preuves faibles de plusieurs sources en une réfutation forte.
• Limites :
  • L'article décrit un travail en cours. Il n'inclut pas une implémentation pratique ni une évaluation expérimentale.
  • Le cadre garantit la terminaison et la bornitude, mais il ne garantit pas la correction au sens traditionnel (c'est-à-dire qu'il ne prouve pas que les conclusions du LLM sont correctes). Il rend le rôle probatoire du LLM explicite et auditable.
  • Le cadre ne peut pas corriger un agent qui juge constamment mal les preuves ; il rend simplement ces erreurs visibles.
  • La preuve de terminaison repose sur l'hypothèse que les affirmations ne sont jamais révoquées et que les évaluations n'augmentent que via la jonction. Des mécanismes pour la révision des croyances (abaissement des évaluations) sont discutés comme un travail futur nécessitant un remplacement borné ou une recomputation par époques.

5. Signification

La signification de ce travail réside dans sa tentative d'apporter une discipline structurelle au raisonnement basé sur les LLM dans l'analyse de programmes. En s'éloignant du paradigme « générer-et-vérifier » (qui nécessite un vérificateur formel pour la sortie du LLM) et du paradigme « oracle heuristique » (où le LLM ne peut pas affecter la correction), l'Interprétation Agentique vise un juste milieu.

Elle est significative pour les analyses dépendantes des preuves où :

• Les faits pertinents ne sont pas formalisables (par exemple, contrats d'API informels, avis de sécurité).
• Un vérificateur complet n'existe pas.
• L'analyse nécessite de synthétiser des informations provenant de sources diverses et non liées au code.

Le cadre transforme le LLM d'un générateur boîte noire en un composant borné et auditable d'un système d'analyse plus vaste. Il garantit que l'analyse progresse de manière contrôlée et raisonnée, permettant la séparation des préoccupations : le LLM fournit des preuves, et le harnais basé sur les treillis garantit que l'analyse est bornée et traçable. Cette approche vise à inspirer de futures discussions sur la conception de techniques fondées formellement pour les systèmes agentiques dans l'analyse de programmes.