Publications
2026
- CGO 2026Thinking Fast and Correct: Automated Rewriting of Numerical Code through Compiler AugmentationSiyuan Brant Qian, Vimarsh Sathia, Ivan R. Ivanov, Jan Hückelheim, Paul Hovland, and William S. MosesIn 22nd ACM/IEEE International Symposium on Code Generation and Optimization, Jan 2026, Sydney, Australia.
Floating-point numbers are finite-precision approximations to real numbers and are ubiquitous in computer applications in nearly every field. Selecting the right floating-point representation that achieves a good balance of performance and numerical accuracy is a difficult task, which has become even more critical as hardware has trended to high-performance, low-precision operations. Although the common wisdom around changing floating-point precision implies that accuracy and performance are inversely correlated, more advanced techniques can often circumvent this tradeoff. Applying complex numerical optimizations to real-world code, however, is an arduous engineering task that requires expertise in numerical analysis and performance engineering, and the specific computational context. While there is a plethora of existing tools that partially automate this process, they are limited in the scope of optimization techniques or still require substantial human intervention. We present Poseidon, a modular and fully extensible framework that fully automates floating-point analyses and optimizations for real-world applications within a production compiler. Poseidon operates as two-phase compiler. In the first compilation, Poseidon captures computational context through small surrogate profiled executions. In the second compilation, Poseidon consumes profiled data, generates and evaluates candidate rewrites such as precision changes and algebraic rewrites, and solves for optimal performance/accuracy tradeoffs and rewrite sets. Poseidon’s interoperability with standard compiler analyses and optimizations grants it analysis and optimization advantages unavailable to existing source- and binary-level approaches. We evaluate Poseidon on multiple large-scale applications and perform ablations on each component of Poseidon’s design. We find that performing profile-guided algebraic rewrites and precision tuning leads to outsized benefits in performance without substantially changing accuracy, and outsized accuracy benefits without diminishing performance. On a quaternion differentiator, Poseidon enables a 1.46× speedup with a relative error of 1e-7. In DOE’s 64-bit LULESH hydrodynamics application, Poseidon improves program accuracy to exactly match a 512-bit simulation run without substantially reducing runtime performance.
2024
- LAFI 2024Abstract Interpretation for Automatic DifferentiationIn 10th Workshop on Languages for Inference at POPL, Jan 2024, London, UK.
Despite the fact that Automatic Differentiation (AD) underlies much of machine learning, scientific computing and graphics, static analyses of AD code has been limited. In this position paper, we argue why AD code needs precise, general and scalable abstract interpretation and why this abstract interpretation should leverage the specific structure inherent to AD. Lastly, we demonstrate a new use of abstract interpretation of AD to analyze Coordinate MLPs from Graphics, attaining orders of magnitude more precision than prior work.
2023
- OOPSLA 2023Synthesizing Precise Static Analyzers for Automatic DifferentiationIn 38th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications, Oct 2023, Cascais, Portugal.
We present Pasado, a technique for synthesizing precise static analyzers for Automatic Differentiation. Our technique allows one to automatically construct a static analyzer specialized for the Chain Rule, Product Rule, and Quotient Rule computations for Automatic Differentiation in a way that abstracts all of the nonlinear operations of each respective rule simultaneously. By directly synthesizing an abstract transformer for the composite expressions of these 3 most common rules of AD, we are able to obtain significant precision improvement compared to prior works which compose standard abstract transformers together suboptimally. We prove our synthesized static analyzers sound and additionally demonstrate the generality of our approach by instantiating these AD static analyzers with different nonlinear functions, different abstract domains (both intervals and zonotopes) and both forward-mode and reverse-mode AD. We evaluate Pasado on multiple case studies, namely soundly computing bounds on a neural network’s local Lipschitz constant, soundly bounding the sensitivities of financial models, certifying monotonicity, and lastly, bounding sensitivities of the solutions of differential equations from climate science and chemistry for verified ranges of initial conditions and parameters. The local Lipschitz constants computed by Pasado on our largest CNN are up to 2750× more precise compared to the existing state-of-the-art zonotope analysis. The bounds obtained on the sensitivities of the climate, chemical, and financial differential equation solutions are between 1.31 − 2.81× more precise (on average) compared to a state-of-the-art zonotope analysis.