Correctness Meets Performance: From Agda to Futhark
summary
Derives a reverse-mode automatic-differentiation pipeline in Agda for index-safe tensors, proves semantic preservation for AD and optimizer passes, and extracts a deeply-embedded tensor DSL to Futhark. Implements a canonical convolutional neural network, computes training derivatives, and generates GPU code; microbenchmarks show generated kernels beat TensorFlow on small shapes and fall behind at large sizes but otherwise approach TensorFlow performance, demonstrating correctness with practical speed.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 2:10Proof assistants vs performance
- 3:17Array theory with combinators
- 5:25CNNs in array expressions
- 6:50Arrays as dependent functions
- 10:07Convolution combinators
- 13:23Index-safe neural networks
- 14:51DSL for numerical apps
- 16:17Reverse autodiff in DSL
- 19:04Optimization proofs
- 19:27Performance vs TensorFlow
- 20:33Conclusion
- 20:53Q&A
related talks
39mDifferentiable Functional Programming
29mStaging Automatic Differentiation with Fusion
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
29mReverse Automatic Differentiation for Accelerate (Extended Abstract)
30mGenerating High Performance Code for Irregular Data Structures using Dependent Types
45mAPLicative Programming with Naperian Functors
30mData-Parallel Flattening by Expansion
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...