Certified roundoff error bounds using semidefinite programming
From MaRDI portal
Abstract: Roundoff errors cannot be avoided when implementing numerical programs with finite precision. The ability to reason about rounding is especially important if one wants to explore a range of potential representations, for instance for FPGAs or custom hardware implementations. This problem becomes challenging when the program does not employ solely linear operations, and non-linearities are inherent to many interesting computational problems in real-world applications. Existing solutions to reasoning possibly lead to either inaccurate bounds or high analysis time in the presence of nonlinear correlations between variables. Furthermore, while it is easy to implement a straightforward method such as interval arithmetic, sophisticated techniques are less straightforward to implement in a formal setting. Thus there is a need for methods which output certificates that can be formally validated inside a proof assistant. We present a framework to provide upper bounds on absolute roundoff errors of floating-point nonlinear programs. This framework is based on optimization techniques employing semidefinite programming and sums of squares certificates, which can be checked inside the Coq theorem prover to provide formal roundoff error bounds for polynomial programs. Our tool covers a wide range of nonlinear programs, including polynomials and transcendental operations as well as conditional statements. We illustrate the efficiency and precision of this tool on non-trivial programs coming from biology, optimization and space control. Our tool produces more accurate error bounds for 23% of all programs and yields better performance in 66% of all programs.
Recommendations
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Rigorous roundoff error analysis of probabilistic floating-point computations
Cited in
(30)- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Combining tools for optimization and analysis of floating-point computations
- A sublevel moment-SOS hierarchy for polynomial optimization
- Exploiting sparsity in complex polynomial optimization
- Sparse noncommutative polynomial optimization
- Exploiting term sparsity in noncommutative polynomial optimization
- A two-phase approach for conditional floating-point verification
- Deductive verification of floating-point Java programs in KeY
- Runtime abstract interpretation for numerical accuracy and robustness
- SONC optimization and exact nonnegativity certificates via second-order cone programming
- Certification of bounds on expressions involving rounded operators
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- Rigorous Error Bounds for the Optimal Value in Semidefinite Programming
- Optimal bounds for round-off errors in the cyclic peaceman-rachford iteration
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- TSSOS: A Moment-SOS Hierarchy That Exploits Term Sparsity
- Chordal-TSSOS: a moment-SOS hierarchy that exploits term sparsity with chordal extension
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Roundoff-Error-Free Basis Updates of LU Factorizations for the Efficient Validation of Optimality Certificates
- The RPR2 rounding technique for semidefinite programs
- A unified framework of SAGE and SONC polynomials and its duality theory
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- The smallest mono-unstable convex polyhedron with point masses has 8 faces and 11 vertices
- Formally verified roundoff errors using SMT-based certificates and subdivisions
- CS-TSSOS: correlative and term sparsity for large-scale polynomial optimization
- Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
- A real moment-HSOS hierarchy for complex polynomial optimization with real coefficients
- Reachability in dynamical systems with rounding
- Formally verified roundoff error bounds on LogSumExp-based computations
- Rigorous roundoff error analysis of probabilistic floating-point computations
Describes a project that uses
Uses Software
This page was built for publication: Certified roundoff error bounds using semidefinite programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3133585)
