Hallucination-Resilient LLM-Driven Sound Abstract Interpretation

Prototype abstract interpreter using LLMs to improve precision while maintaining soundness.

Get Started

Install sbt and JVM. Once started with a sbt session, you can compile code using command compile, run a main function using run, execute all test cases using test. You can also run a specific test given the package path, e.g. testOnly llmaam.aam.TestAAM.

Currently, the code base supports Google Gemini and OpenAI API. You need to put a Google Gemini API key in file GEMINI_AI_KEY or OpenAI API in file OPENAI_API_KEY.

Examples

See some visualized analysis results of using different allocation strategies in examples folder.

An example is the stack2 program to demonstrate spurious binding and return flow:

let id = λz. z in
let idid = λw. id(w) in
let x = idid(1) in
let y = idid(2) in
x

Neither 0CFA, 1CFA, or the combination of 0CFA and P4F yields a precision abstract state graph. Using the combination of 1CFA and P4F can achieve the optimal precision (i.e., no spurious state transition, being identical to concrete execution).

This project demonstrates that using LLM as abstract address allocator can achieve the optimal precision too. The allocation strategy is neither fixed k-CFA nor P4F, but entirely adaptive to the program and "runtime" abstract state (while still remain sound). See the system prompt and conversion with LLM here.

TODO

• tweak prompt so that the response can be reified back to Scala code
• OpenAI support
• support conditionals and boolean
• support loops
• support mutable states
• make use of ErrState (eg. adding a function with a number produce ErrState)
• a Scheme parser (to handle some benchmarks)
• Refactor desugaring from Scheme to core syntax
• Deepseek, QWen API support
• Give better prompt (eg existing strategy etc) to guide LLM make better decisions
• support call/cc