More Like this

1. Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

   https://doi.org/10.1145/3674635  

   Aguirre, Alejandro; Haselwarter, Philipp G; de_Medeiros, Markus; Li, Kwing Hei; Gregersen, Simon Oddershede; Tassarotti, Joseph; Birkedal, Lars (August 2024, Proceedings of the ACM on Programming Languages)

   Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the probability of these errors, but existing verification approaches have limitations that lead to error probability bounds that are excessively coarse, or only apply to first-order programs. In this paper we present Eris, a higher-order separation logic for proving error probability bounds for probabilistic programs written in an expressive higher-order language. Our key novelty is the introduction of error credits, a separation logic resource that tracks an upper bound on the probability that a program returns an erroneous result. By representing error bounds as a resource, we recover the benefits of separation logic, including compositionality, modularity, and dependency between errors and program terms, allowing for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and error induction. We illustrate the advantages of our approach by proving amortized error bounds on a range of examples, including collision probabilities in hash functions, which allow us to write more modular specifications for data structures that use them as clients. We also use our logic to prove correctness and almost-sure termination of rejection sampling algorithms. All of our results have been mechanized in the Coq proof assistant using the Iris separation logic framework and the Coquelicot real analysis library. 

   more » « less
2. Identifying and bounding the probability of necessity for causes of effects with ordinal outcomes

   https://doi.org/10.1093/biomet/asaf049  

   Zhang, Chao; Geng, Zhi; Li, Wei; Ding, Peng (July 2025, Biometrika)

   Abstract Although the existing causal inference literature focuses on the forward-looking perspective by estimating effects of causes, the backward-looking perspective can provide insights into causes of effects. In backward-looking causal inference, the probability of necessity measures the probability that a certain event is caused by the treatment given the observed treatment and outcome. Most existing results focus on binary outcomes. Motivated by applications with ordinal outcomes, we propose a general definition of the probability of necessity. However, identifying the probability of necessity is challenging because it involves the joint distribution of the potential outcomes. We propose a novel assumption of monotonic incremental treatment effect to identify the probability of necessity with ordinal outcomes. We also discuss the testable implications of this key identification assumption. When it fails, we derive explicit formulas of the sharp large-sample bounds on the probability of necessity. 

   more » « less
3. Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms

   Sankaranarayanan, Sriram; Chou, Yi; Goubault, Eric; and Putot, Sylvie (December 2020, Advances in Neural Information Processing System (NeurIPS))

   null (Ed.)

   In this paper, we propose polynomial forms to represent distributions of state variables over time for discrete-time stochastic dynamical systems. This problem arises in a variety of applications in areas ranging from biology to robotics. Our approach allows us to rigorously represent the probability distribution of state variables over time, and provide guaranteed bounds on the expectations, moments and probabilities of tail events involving the state variables. First we recall ideas from interval arithmetic, and use them to rigorously represent the state variables at time t as a function of the initial state variables and noise symbols that model the random exogenous inputs encountered before time t. Next we show how concentration of measure inequalities can be employed to prove rigorous bounds on the tail probabilities of these state variables. We demonstrate interesting applications that demonstrate how our approach can be useful in some situations to establish mathematically guaranteed bounds that are of a different nature from those obtained through simulations with pseudo-random numbers. 

   more » « less
4. Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms.

   Sankaranarayanan, Sriram; Chou, Yi; Goubault, Eric; Putot, Sylvie (December 2020, Part of Advances in Neural Information Processing Systems 33 (NeurIPS 2020))

   In this paper, we propose polynomial forms to represent distributions of state variables over time for discrete-time stochastic dynamical systems. This problem arises in a variety of applications in areas ranging from biology to robotics. Our approach allows us to rigorously represent the probability distribution of state variables over time, and provide guaranteed bounds on the expectations, moments and probabilities of tail events involving the state variables. First, we recall ideas from interval arithmetic, and use them to rigorously represent the state variables at time t as a function of the initial state variables and noise symbols that model the random exogenous inputs encountered before time t. Next, we show how concentration of measure inequalities can be employed to prove rigorous bounds on the tail probabilities of these state variables. We demonstrate interesting applications that demonstrate how our approach can be useful in some situations to establish mathematically guaranteed bounds that are of a different nature from those obtained through simulations with pseudo-random numbers. 

   more » « less
5. Exponential Tail Bounds on Queues: A Confluence of Non- Asymptotic Heavy Traffic and Large Deviations

   https://doi.org/10.1145/3649477.3649488  

   Raj_Jhunjhunwala, Prakirt; Hurtado-Lange, Daniela; Theja_Maguluri, Siva (February 2024, ACM SIGMETRICS Performance Evaluation Review)

   In general, obtaining the exact steady-state distribution of queue lengths is not feasible. Therefore, we focus on establishing bounds for the tail probabilities of queue lengths. We examine queueing systems under Heavy Traffic (HT) conditions and provide exponentially decaying bounds for the probability P(∈q > x), where ∈ is the HT parameter denoting how far the load is from the maximum allowed load. Our bounds are not limited to asymptotic cases and are applicable even for finite values of ∈, and they get sharper as ∈ - 0. Consequently, we derive non-asymptotic convergence rates for the tail probabilities. Furthermore, our results offer bounds on the exponential rate of decay of the tail, given by -1/2 log P(∈q > x) for any finite value of x. These can be interpreted as non-asymptotic versions of Large Deviation (LD) results. To obtain our results, we use an exponential Lyapunov function to bind the moment-generating function of queue lengths and apply Markov's inequality. We demonstrate our approach by presenting tail bounds for a continuous time Join-the-shortest queue (JSQ) system. 

   more » « less