Certified roundoff error bounds using semidefinite programming
From MaRDI portal
Publication:3133585
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
(28)- A unified framework of SAGE and SONC polynomials and its duality theory
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- CS-TSSOS: correlative and term sparsity for large-scale polynomial optimization
- Runtime abstract interpretation for numerical accuracy and robustness
- Certification of bounds on expressions involving rounded operators
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- A two-phase approach for conditional floating-point verification
- Deductive verification of floating-point Java programs in KeY
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- TSSOS: A Moment-SOS Hierarchy That Exploits Term Sparsity
- Optimal bounds for round-off errors in the cyclic peaceman-rachford iteration
- Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
- Combining tools for optimization and analysis of floating-point computations
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- Roundoff-Error-Free Basis Updates of LU Factorizations for the Efficient Validation of Optimality Certificates
- Rigorous roundoff error analysis of probabilistic floating-point computations
- SONC optimization and exact nonnegativity certificates via second-order cone programming
- Chordal-TSSOS: a moment-SOS hierarchy that exploits term sparsity with chordal extension
- A sublevel moment-SOS hierarchy for polynomial optimization
- The RPR2 rounding technique for semidefinite programs
- Sparse noncommutative polynomial optimization
- The smallest mono-unstable convex polyhedron with point masses has 8 faces and 11 vertices
- Exploiting term sparsity in noncommutative polynomial optimization
- Rigorous Error Bounds for the Optimal Value in Semidefinite Programming
- Exploiting sparsity in complex polynomial optimization
- A real moment-HSOS hierarchy for complex polynomial optimization with real coefficients
- Formally verified roundoff errors using SMT-based certificates and subdivisions
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)
