Synthesizing Backward Error Bounds, Backward

TL;DR

This paper introduces a formal framework and a tool for automated backward error analysis of numerical programs, broadening the scope of backward stability verification.

Contribution

It generalizes backward stability, develops a categorical model, and implements a tool that automates backward error bounds synthesis for complex programs.

Findings

Successfully analyzes programs with variable reuse

Proves soundness of the backward stability algorithm

Synthesizes bounds for previously intractable programs

Abstract

Backward stability is a desirable property for a well-designed numerical algorithm: given an input, a backward stable floating-point program produces the exact output for a nearby input. While automated tools for bounding the forward error of a numerical program are well-established, few existing tools target backward error analysis. We present a formal framework that enables sound, automated backward error analysis for a broad class of numerical programs. First, we propose a novel generalization of the definition of backward stability that is both compositional and flexible, satisfied by a wide range of floating-point operations. Second, based on this generalization, we develop the category Shel where morphisms model stable numerical programs, and show that structures in Shel support a rich variety of backward error analyses. Third, we implement a tool, eggshel, that automatically searches within a syntactic subcategory of Shel to prove backward stability for a given program. Our algorithm handles many programs with variable reuse, a known challenge in backward error analysis. We prove soundness of our algorithm and use our tool to synthesize backward error bounds for a suite of programs that were previously beyond the reach of automated analysis.