SAIL: Sound Abstract Interpreters with LLMs
summary
Framework uses LLMs to synthesize globally sound abstract transformers by casting synthesis as a constrained optimization problem with a principled cost function that measures degree of unsoundness, enforced by syntactic/semantic checkers and an SMT-backed ProofSound verifier. Generated DSL transformers compile via the Newton compiler to PyTorch. Results: synthesis finishes within ~2 hours, peak memory ≈650 MB, matches handcrafted precision on known operators and produces new high-precision transformers for GELU/ELU and other non-linear operators, with iterative LLM-guided refinement until soundness holds.
AI-written summary · about
chapters (12)
- 0:00SAIL project introduction
- 0:22Motivation for abstract interpreters
- 1:45Challenges in sound transformers
- 3:11Automation efforts and limits
- 3:53Cell framework with LLMs
- 5:18Strict soundness requirements
- 6:21Cost function for unsoundness
- 8:51Cost function design examples
- 13:28Finalized synthesis pipeline
- 14:31Soundness vs precision
- 15:54Experimental metrics
- 18:42Q&A
related talks
28mSynthesizing Abstract Transformers
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
14mSynthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE(…)
20mOptimal Program Synthesis via Abstract Interpretation
19mLLMs reasoning and agentic capabilities over time
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
53mSemantics-based program manipulation in the age of LLMs
29mSynthesizing Axiomatizations using Logic Learning