Neural networks are increasingly becoming integral to safety-critical applications, such as controllers in embedded systems. While formal safety verification focuses on idealized real-valued networks, practical applications require quantization to finite precision, inevitably introducing roundoff errors. Manually optimizing precision, especially for fixed-point implementation, while ensuring safety is complex and time-consuming.

In this talk, I will introduce Aster, the sound, fully automated, mixed-precision, fixed-point quantizer for deep feed-forward neural networks. Aster reduces the quantization problem to a mixed-integer linear programming (MILP) problem, thus efficiently determining minimal precision to guarantee predefined error bounds. Our evaluations show that Aster's optimized code reduces machine cycles when compiled to an FPGA with a commercial HLS compiler compared to (sound) state-of-the-art. Furthermore, Aster handles significantly more benchmarks faster, especially for larger networks with thousands of parameters.

This talk will expose some of the opportunities offered by this freedom, and some of the methodologies and tools that allow a designer to build and compose application-specific operators. It may include some inadvertent advertising for our upcoming 800-page book dedicated to these topics.

Joe is a long-time member on the JDK engineering team, first at Sun and later Oracle. As “Java Floating-Point Czar” he has looked after Java numerics including contributing to the design of strictfp, adding numerous floating-point math library methods, and adding hexadecimal floating-point literals to the Java language and library. Joe was a participant in and interim editor of the 2008 revision to the IEEE 754 floating-point standard. Outside of numerics, Joe has done other foundational work on the Java platform including core libraries development, Java language changes including Project Coin, infrastructure improvements, and reviewing platform interface updates, together with a smattering of project management and release management along the way.

Finch is a domain-specific language for numerically solving differential equations. It employs a variety of numerical techniques, generates code for a number of different target frameworks and languages, and allows almost arbitrary equation input. In addition, it accepts unrestricted modification of the generated code to provide maximal flexibility and hand-optimization. One downside to this (perhaps excessive) flexibility is that numerical instability and the occasional typo can easily turn a solution into a pile of NaNs.

Eric will introduce Finch, and demonstrate some of the features relevant to the numerics. We will look at some examples where things turn out just the way we hoped, and some where they don't.

Allison lead a great discussion of her recent CACM article Keeping Science on Keel When Software Moves.

High performance computing (HPC) is central to solving large problems in science and engineering through the deployment of massive amounts of computational power. The development of important pieces of HPC software spans years or even decades, involving dozens of computer and domain scientists. During this period, the core functionality of the software is made more efficient, new features are added, and the software is ported across multiple platforms. Porting of software in general involves the change of compilers, optimization levels, arithmetic libraries, and many other aspects that determine the machine instructions that actually get executed. Unfortunately, such changes do affect the computed results to a significant (and often worrisome) extent. In a majority of cases, there are not easily definable a priori answers one can check against. A programmer ends up comparing the new answer against a trusted baseline previously established or checks for indirect confirmations such as whether physical properties such as energy are conserved. However, such non-systematic efforts might miss underlying issues, and the code may keep misbehaving until these are fixed.

In this session, Allison presented real-world evidence to show that ignoring numerical result changes can lead to misleading scientific conclusions. She presented techniques and tools that can help computational scientists understand and analyze compiler effects on their scientific code. These techniques are applicable across a wide range of examples to narrow down the root-causes to single files, functions within files, and even computational expressions that affect specific variables. The developer may then rewrite the code selectively and/or suppress the application of certain optimizations to regain more predictable behavior.

Tanmay Tirpankar https://github.com/arnabd88/Satire

Mike Lam https://github.com/crafthpc/floatsmith

Interval arithmetic is a simple way to compute a mathematical expression to an arbitrary accuracy, widely used for verifying floating-point computations. Yet this simplicity belies challenges. Some inputs violate preconditions or cause domain errors. Others cause the algorithm to enter an infinite loop and fail to compute a ground truth. Plus, finding valid inputs is itself a challenge when invalid and unsamplable points make up the vast majority of the input space. These issues can make interval arithmetic brittle and temperamental.

Rival introduces three extensions to interval arithmetic to address these challenges. Error intervals express rich notions of input validity and indicate whether all or some points in an interval violate implicit or explicit preconditions. Movability flags detect futile recomputations and prevent timeouts by indicating whether a higher-precision recomputation will yield a more accurate result. And input search restricts sampling to valid, samplable points, so they are easier to find. We compare these extensions to the state-of-the-art technical computing software Mathematica, and demonstrate that our extensions are able to resolve 60.3% more challenging inputs, return 10.2× fewer completely indeterminate results, and avoid 64 cases of fatal error.