Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
summary
Automates generation of MLIR integer abstract transformers by synthesizing small SSA programs (cut-style MCMC search) and composing them with meet-of-components synthesis plus conditional abduction to make partial rules globally sound. Candidates lower to an SMT MLIR dialect for verification and to C++ for execution; the system runs hundreds of parallel MCMC chains to explore programs, produces provably sound transformers, usually assembles 1–10 components per operator, and yields 17% more precise than LLVM on some operators while matching LLVM on many others.
AI-written summary · about
chapters (20)
- 0:00MLIR abstract transformers intro
- 1:05Why abstract transformers matter
- 3:12Manual transformer challenges
- 4:59Nice to Meet You results preview
- 6:02Formal problem definition
- 7:49Key insights behind approach
- 8:54Precision measurement objective
- 10:00Stochastic synthesis via MCMC
- 11:05Meet operators for scalability
- 12:53Abduction to refine transformers
- 13:34End-to-end workflow
- 14:59Evaluation on IR operators
- 16:05Precision in real projects
- 17:08Composite operator synthesis
- 18:35Future work and economics
- 19:41Related work context
- 20:25Q&A: Input requirements
- 21:27Q&A: Meet transformer count
- 22:30Q&A: Relational domain support
- 23:56Q&A: Starting from existing code
related talks
28mSynthesizing Abstract Transformers
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
30mAnalyzing Programs with SMT Solvers
22mSAIL: Sound Abstract Interpreters with LLMs
20mMimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
18mCompiling with Abstract Interpretation
14mSound and Modular Activity Analysis for Automatic Differentiation in MLIR