Technical Summary: Agentic Interpretation for LLM-Based Program Analysis

1. Problem Statement

Large Language Models (LLMs) offer unique capabilities for program analysis by accessing information beyond source code, such as documentation, security advisories, version-specific metadata, and informal API contracts. However, relying on LLMs for "one-shot" whole-program analysis is inherently brittle for three primary reasons:

1. Context Sensitivity: Empirical studies indicate that model performance degrades as context length and task complexity increase, and results depend heavily on the ordering of information in the prompt. Critical evidence (e.g., a specific security advisory) may be supplied but not utilized reliably.
2. Lack of Persistent State: Monolithic LLM responses lack a persistent state to track which specific claims were supported, refuted, or left open. This makes it difficult to handle self-contradictory reasoning or reasoning that fails to support its own conclusions.
3. Absence of Dependency Structure: A single-shot answer provides no mechanism for feedback. If later findings reveal that an earlier question was scoped incorrectly or that an upstream component requires re-examination under a different hypothesis, an unstructured answer cannot facilitate this iterative refinement.

Consequently, there is a need for a framework that bridges the gap between ad-hoc LLM prompting and fully specified static analysis, specifically for evidence-dependent program analyses where the relevant facts are not fully contained in the source code or formal specifications.

2. Methodology: Agentic Interpretation

The paper proposes Agentic Interpretation, a framework that applies the discipline of lattice-based static analysis to LLM-driven reasoning. The methodology decomposes high-level analysis goals into localized claims anchored to program points and component boundaries, managing their evolution through a finite-height lattice and a worklist algorithm.

2.1 Core Components

• Evaluation Graph ($G^*$): An extension of a program-derived graph ($G_{prog}$) that includes:
  • Auxiliary Nodes: Nodes representing cross-component interactions or goals that do not map to a single program point.
  • Context Edges: Forward-flowing edges ensuring that when a claim at node $n$ is evaluated, it receives the current assessment state and evidence from its predecessors.
  • Feedback Edges: Reverse-flowing edges that trigger re-evaluation of upstream nodes when a downstream assessment changes (e.g., a refuted composition claim triggers a targeted search in an opaque component).
• Assessment Domain (Lattice): A finite-height join-semilattice ($A$) that summarizes the evidential status of a claim.
  • The paper illustrates this with the AGraded lattice: $\{ \perp, w, s \} \times \{ \perp, w, s \}$, where the first coordinate represents supporting evidence and the second represents refuting evidence. Values range from absent ($\perp$) to weak ($w$) to strong ($s$).
  • The lattice is an epistemic domain over evidence states, not an abstract domain over concrete program states. It records whether a claim has been supported or refuted and the strength of that evidence.
• Worklist Harness: A control loop that manages the analysis state.
  • Contextualization: For a node $n$, the harness constructs a prompt context ($\Gamma_n$) using source code, the high-level goal, and the current assessments of predecessor nodes.
  • Node Transformers: The LLM agent performs two operations:
    1. Evaluation: Assesses existing claims against the context, returning an updated assessment and evidence records.
    2. Generation: Proposes new, relevant claims based on the context.
  • Propagation: If the join of the new assessment with the old assessment results in a strict increase in the lattice order, the node's extended successors are enqueued for re-evaluation.

2.2 The Analysis Process

The process is illustrated through a security review of a program with opaque third-party components (a JSON parser and a signature verifier).

1. Initialization: The worklist is seeded with all program and auxiliary nodes.
2. Iterative Refinement:
   • Phase I: Initial independent assessment of components (e.g., reviewing documentation for the parser and verifier).
   • Phase II: Composition of evidence. The framework evaluates cross-component claims (e.g., "Do the components jointly ensure safety?"). If a composition claim is weakly refuted, feedback edges trigger a re-investigation of upstream components.
   • Phase III: Feedback-driven refinement. The context from the refuted composition (e.g., "the processor performs no validation") guides the LLM to perform a targeted search for specific vulnerabilities (e.g., prototype pollution) rather than a broad review.
   • Phase IV: Stabilization. The strengthened upstream evidence propagates forward, leading to a strong refutation of the global goal. The worklist empties when no further strict increases in assessment occur.

3. Key Contributions

The paper makes three primary contributions:

1. Framework Proposal: It introduces Agentic Interpretation as a structured approach for evidence-dependent program analysis, identifying a suitable problem domain where LLMs are necessary but direct prompting is insufficient.
2. Formal Model: It formalizes the core model, defining the evaluation graph, the assessment domain, node transformers, and the worklist algorithm.
3. Design Space Characterization: It explores the design space, including:
   • Assessment Lattices: Discussing trade-offs between coarse lattices (e.g., presence/absence) and fine-grained lattices (e.g., strength, confidence basis). It introduces AStratified, a domain that tracks evidence strength and confidence basis (e.g., "model-only" vs. "checked") separately.
   • Claim Management: Addressing claim canonicalization, granularity, and scope.
   • Query Design: Differentiating between evaluation queries (support/refutation) and generative queries (proposing new claims).
   • Termination: Proving that the algorithm terminates for finite-height lattices with bounded claim generation, even in the presence of non-deterministic LLM responses, provided that updates are monotonic (via join).

4. Results and Limitations

• Results: The paper provides a worked example (a security review of a handler with opaque components) demonstrating how the framework decomposes a goal, utilizes feedback loops to refine the search, and stabilizes on a final assessment. It shows how the framework can detect that a global security goal is violated by combining weak evidence from multiple sources into a strong refutation.
• Limitations:
  • The paper describes work in progress. It does not include a practical implementation or experimental evaluation.
  • The framework guarantees termination and boundedness, but it does not guarantee soundness in the traditional sense (i.e., it does not prove the LLM's conclusions are correct). It makes the LLM's evidential role explicit and auditable.
  • The framework cannot correct an agent that consistently misjudges evidence; it only makes such errors visible.
  • The termination proof relies on the assumption that claims are never revoked and assessments only increase via join. Mechanisms for belief revision (lowering assessments) are discussed as future work requiring bounded replacement or epochal recomputation.

5. Significance

The significance of this work lies in its attempt to bring structural discipline to LLM-based reasoning in program analysis. By moving away from the "generate-and-check" paradigm (which requires a formal verifier for the LLM's output) and the "heuristic oracle" paradigm (where the LLM cannot affect soundness), Agentic Interpretation targets a middle ground.

It is significant for evidence-dependent analyses where:

• The relevant facts are not formalizable (e.g., informal API contracts, security advisories).
• A complete verifier does not exist.
• The analysis requires synthesizing information from diverse, non-code sources.

The framework transforms the LLM from a black-box generator into a bounded, auditable component of a larger analysis system. It ensures that the analysis proceeds in a controlled, principled manner, allowing for the separation of concerns: the LLM provides evidence, and the lattice-based harness ensures the analysis is bounded and traceable. This approach aims to inspire future discussions on designing formally-grounded techniques for agentic systems in program analysis.