A Dual Number Abstraction for Static Analysis of Clarke Jacobians
summary
Paper presents a dual-interval abstract domain that lifts dual-number forward-mode differentiation to interval arithmetic and proves the transformer semantics sound interval over-approximation of the Clarke Jacobian. Implementation DeepJ computes interval Clarke Jacobians for compositions of neural nets with non-differentiable perturbations (rotation, contrast, haze), scales to networks of roughly 62,000 neurons and ≈2.5 million parameters, runs in seconds per analysis, and yields much tighter local Lipschitz bounds than the global-baseline.
AI-written summary · about
chapters (25)
- 0:00Intro
- 0:51Machine Learning Revolution
- 1:13Gradients
- 1:58Neural Network
- 2:30Local Lipschitz Robustness - Intuition
- 3:24Example: Lipschitz Robustness Problem
- 6:08DeepJ Language
- 6:30Semantics
- 7:07Reminder: Standard Jacobian
- 7:18Clarke Generalized Jacobian
- 8:21Forward or Reverse?
- 8:45Dual Numbers
- 9:04First Order Taylor Series
- 10:04Our Analysis: Dual Intervals
- 10:17Dual Interval Arithmetic
- 10:36Dual Interval Abstract Domain: ID
- 11:06Dual Interval Abstract Evaluation
- 13:00Dual Interval Abstract Branching
- 13:42Dual Interval Branching Examples (ReLU and Max)
- 15:58Theoretical Results
- 17:00Applications
- 17:36Experimental Methodology - DeepJ
- 18:31Haze - Paterson et al. [2021]
- 21:09Analysis Execution Time per Image (62K neurons)
- 21:41Takeaways
related talks
11mAbstract Interpretation for Automatic Differentiation
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
01h 03mInside Every Calculus Is A Little Algebra Waiting To Get Out
16mThe Continuous Tensor Abstraction: Where Indices are Real
17mSynthesizing Precise Static Analyzers for Automatic Differentiation
31mAbstract Neural Networks
29mParallelism-preserving automatic differentiation for second-order array languages
32mData-Driven Inverse Modeling with Incomplete Observations