Satire: Computing Rigorous Bounds for Floating-Point Rounding Error in Mixed-Precision Loop-Free Programs

• URL: http://arxiv.org/abs/2503.05924v1
• Date: Fri, 07 Mar 2025 20:46:38 GMT
• Title: Satire: Computing Rigorous Bounds for Floating-Point Rounding Error in Mixed-Precision Loop-Free Programs
• Abstract summary: Satire is a tool that allows designers to trade error-bound tightness for gains in analysis time.<n>satire can be used during the design of numerical routines to effect design tradeoffs guided by rigorous empirical error guarantees.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Techniques that rigorously bound the overall rounding error exhibited by a numerical program are of significant interest for communities developing numerical software. However, there are few available tools today that can be used to rigorously bound errors in programs that employ conditional statements (a basic need) as well as mixed-precision arithmetic (a direction of significant future interest) employing global optimization in error analysis. In this paper, we present a new tool that fills this void while also employing an abstraction-guided optimization approach to allow designers to trade error-bound tightness for gains in analysis time -- useful when searching for design alternatives. We first present the basic rigorous analysis framework of Satire and then show how to extend it to incorporate abstractions, conditionals, and mixed-precision arithmetic. We begin by describing Satire's design and its performance on a collection of benchmark examples. We then describe these aspects of Satire: (1) how the error-bound and tool execution time vary with the abstraction level; (2) the additional machinery to handle conditional expression branches, including defining the concepts of instability jumps and instability window widths and measuring these quantities; and (3) how the error changes when a mix of precision values are used. To showcase how \satire can add value during design, we start with a Conjugate Gradient solver and demonstrate how its step size and search direction are affected by different precision settings. Satire is freely available for evaluation, and can be used during the design of numerical routines to effect design tradeoffs guided by rigorous empirical error guarantees.

Related papers

• FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection [0.0]
  FPScan is a novel tool to formally define and detect catastrophic cancellation and absorption in floating-point programs.<n>Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables.<n>Off-the-shelf SMT solver is used to determine whether the program exhibits any of these critical numerical pitfalls.
  arXiv  Detail & Related papers  (2026-09-07T13:41:01Z)
• NL2Scratch: An Executable Benchmark and Evaluation for Block-Based Programming [62.89531126732269]
  We introduce NL2Scratch, an executable benchmark for natural-language-to-Scratch generation.<n>We construct a semantically validated pool of 23,594 examples, and a slot-balanced 800 diagnostic benchmark.<n>Experiments across instruction-tuned and fine-tuned LLMs reveal a notable gap between lexical similarity and semantic alignment.
  arXiv  Detail & Related papers  (2026-06-20T14:22:59Z)
• Evaluating Numerical Accuracy in Mixed-Precision Computing by Dual-Delta Testing [0.7106986689736828]
  When implementing custom mixed-precision functions, it is critical to verify their numerical accuracy.<n>Traditional approaches typically compare the custom implementation against a reference using a single error metric.<n>This paper introduces textitDual-Delta Testing, a systematic methodology that evaluates two error distributions against a high-precision oracle.
  arXiv  Detail & Related papers  (2026-02-11T07:54:04Z)
• EmbedGrad: Gradient-Based Prompt Optimization in Embedding Space for Large Language Models [45.78656491861157]
  We propose EmbedGrad, a framework that optimize text prompt embeddings through gradient-based refinement.<n>Our approach uniquely decouples training from deployment.<n> Comprehensive evaluations across mathematical reasoning, sentiment analysis, and causal judgment tasks demonstrate EmbedGrad's effectiveness.
  arXiv  Detail & Related papers  (2025-08-05T15:03:10Z)
• Employing Continuous Integration inspired workflows for benchmarking of scientific software -- a use case on numerical cut cell quadrature [0.3387808070669509]
  This paper presents a proven approach that utilizes established Continuous Integration tools and practices to achieve high automation of benchmark execution and reporting. Our use case is the numerical integration (quadrature) on arbitrary domains, which are bounded by implicitly or parametrically defined curves or surfaces in 2D or 3D.
  arXiv  Detail & Related papers  (2025-03-21T14:42:24Z)
• Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
  We present a novel gradient-free algorithm to solve convex optimization problems. Such problems are encountered in medicine, physics, and machine learning. We provide convergence guarantees for the proposed algorithm under both types of noise.
  arXiv  Detail & Related papers  (2024-11-21T10:26:17Z)
• Probably Approximately Precision and Recall Learning [62.912015491907994]
  Precision and Recall are foundational metrics in machine learning. One-sided feedback--where only positive examples are observed during training--is inherent in many practical problems. We introduce a PAC learning framework where each hypothesis is represented by a graph, with edges indicating positive interactions.
  arXiv  Detail & Related papers  (2024-11-20T04:21:07Z)
• Uncertainty Quantification for Neurosymbolic Programs via Compositional Conformal Prediction [36.88661670156255]
  Conformal prediction has emerged as a promising strategy for quantifying uncertainty in machine learning. We propose a novel framework for adapting conformal prediction to neurosymbolic programs. We evaluate our approach on programs that take MNIST and MS-COCO images as input.
  arXiv  Detail & Related papers  (2024-05-24T20:15:53Z)
• SimGrade: Using Code Similarity Measures for More Accurate Human Grading [5.797317782326566]
  We show that inaccurate and inconsistent grading of free-response programming problems is widespread in CS1 courses. We propose several algorithms for assigning student submissions to graders, and (2) ordering submissions to maximize the probability that a grader has previously seen a similar solution.
  arXiv  Detail & Related papers  (2024-02-19T23:06:23Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing [0.0]
  We study the foundations of variational inference, which frames posterior inference as an optimisation problem. We endow our language with both a measurable and a smoothed (approximate) value semantics. We show that our approach has a similar convergence as a key competitor, but is simpler, faster, and attains orders of magnitude reduction in work-normalised variance.
  arXiv  Detail & Related papers  (2023-01-09T15:12:45Z)
• Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference [13.836565669337057]
  We present a static analysis for discovering differentiable or more generally smooth parts of a given probabilistic program. We show how the analysis can be used to improve the pathwise gradient estimator.
  arXiv  Detail & Related papers  (2022-08-22T18:18:32Z)
• A Universal Error Measure for Input Predictions Applied to Online Graph Problems [57.58926849872494]
  We introduce a novel measure for quantifying the error in input predictions. The measure captures errors due to absent predicted requests as well as unpredicted actual requests.
  arXiv  Detail & Related papers  (2022-05-25T15:24:03Z)
• Non-Clairvoyant Scheduling with Predictions Revisited [77.86290991564829]
  In non-clairvoyant scheduling, the task is to find an online strategy for scheduling jobs with a priori unknown processing requirements. We revisit this well-studied problem in a recently popular learning-augmented setting that integrates (untrusted) predictions in algorithm design. We show that these predictions have desired properties, admit a natural error measure as well as algorithms with strong performance guarantees.
  arXiv  Detail & Related papers  (2022-02-21T13:18:11Z)
• ML Supported Predictions for SAT Solvers Performance [0.0]
  Internal solver runtime parameters have been collected and analyzed. A machine learning model has been created for the binary classification of the solver's termination behavior.
  arXiv  Detail & Related papers  (2021-12-17T11:17:29Z)
• Error Estimation for Sketched SVD via the Bootstrap [60.67199274260768]
  This paper develops a fully data-driven bootstrap method that numerically estimates the actual error of sketched singular vectors/values. The method is computationally inexpensive, because it operates only on sketched objects, and it requires no passes over the full matrix being factored.
  arXiv  Detail & Related papers  (2020-03-10T19:14:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.