Numerical Abstract Domains for Trustworthy Code Transpilation (Keynote)

Abstract

LLMs are making code modernization, translation, and rewriting easier and more scalable, enabling software to be transpiled across programming languages and compilers, and optimized for specific hardware platforms. For numerical software relying on finite-precision arithmetic, however, these transformations may introduce numerical deviations that are difficult to predict. Changing the programming language, compiler, execution model, or hardware platform can alter floating-point behavior through differences in precision, rounding, overflow, and the handling of exceptional values. These differences can accumulate into observable changes in program behavior, even when the transformed program produces results equivalent to those of the initial program under real-number semantics. Ensuring trustworthy code transpilation therefore requires reasoning about the finite-precision behavior of the transformed program, taking into account its execution environment and target hardware. This talk presents a retrospective on numerical abstract domains developed to soundly reason about floating-point semantics. It traces the evolution from interval abstractions to richer domains, such as zonotopes and floating-point polyhedra. It then examines how these abstractions have been used to build static analyses for verifying numerical properties of real-world software. This retrospective highlights the trade-offs between the precision, computational cost, and scalability of different abstract domains. The talk then explores how these static analyses can be incorporated into LLM-based code transpilation pipelines. These analyses can assess and guide LLM-based code transformations, allowing the transpilation process to detect changes in finite-precision behavior and determine whether the resulting deviations from ideal real-number semantics are acceptable for the target application. This approach can support a range of requirements, from guaranteeing that numerical error remains within a specified tolerance to enabling performance-driven transformations such as reduced-precision implementations, while providing evidence that the resulting code meets the required accuracy.