Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
summary
Implements a sound abstract interpretation of activity analysis inside MLIR, formalizing an MLIR subset amenable to AD and proving correctness; adds a modular function summary scheme that automatically derives summaries and is as precise as whole-program analysis, proving 100% of inactive instructions the whole-program analysis finds. Prototype in Enzyme/MLIR yields up to 3× speedups, geometric-mean 1.24× CPU, 1.7× GPU, and includes evaluated, reproducible artifacts and full proofs.
AI-written summary · about
chapters (11)
- 0:00Automatic differentiation challenges
- 1:04Limitations of traditional AD
- 2:30Activity analysis benefits
- 3:55Soundness and formalization
- 4:39Modularity and function summaries
- 7:50Differential data dependencies
- 8:11Targeting MLIR infrastructure
- 9:13MLIR interfaces for analysis
- 9:54Performance with activity analysis
- 11:57Summary and contributions
- 13:02Q&A on indirect calls
related talks
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
18mFirst-Class Verification Dialects for MLIR
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
11mEnabling Composition of Kernels and Compilers
34mModular Storage Mode Analysis
27mTaming Unsoundness with Gradual Abstract Interpretation
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
11mAbstract Interpretation for Automatic Differentiation