Certified roundoff error bounds using semidefinite programming
From MaRDI portal
Publication:3133585
DOI10.1145/3015465zbMATH Open1380.65084OpenAlexW2227234579WikidataQ113310145 ScholiaQ113310145MaRDI QIDQ3133585FDOQ3133585
Authors:
Publication date: 5 February 2018
Published in: ACM Transactions on Mathematical Software (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1507.03331
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
polynomial optimizationsemidefinite programmingformal verificationproof assistantfloating-point arithmetictranscendental functionsroundoff errorcorrelation sparsity pattern
Cited In (28)
- 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
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- 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
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- TSSOS: A Moment-SOS Hierarchy That Exploits Term Sparsity
- Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
- Optimal bounds for round-off errors in the cyclic peaceman-rachford iteration
- 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
- The RPR2 rounding technique for semidefinite programs
- A sublevel moment-SOS hierarchy for polynomial optimization
- The smallest mono-unstable convex polyhedron with point masses has 8 faces and 11 vertices
- Sparse noncommutative polynomial optimization
- Rigorous Error Bounds for the Optimal Value in Semidefinite Programming
- Exploiting term sparsity in noncommutative polynomial optimization
- 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
- A unified framework of SAGE and SONC polynomials and its duality theory
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)
