发表机构
Indian Statistical Institute; Ashoka University（印度统计研究所; 阿肖克大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一个统一框架，结合符号与统计方法，对程序在给定输入分布下条件成立频率进行带保证误差界的可靠估计，并支持罕见事件方差缩减。
AI 中文摘要
生产环境中的软件会遇到由其实际使用方式所塑造的输入。我们研究分布感知的可靠性估计：给定一个程序、其运行输入分布以及一个感兴趣的条件，确定该条件成立的频率，并以保证误差界对结果进行认证。符号方法和统计方法提供了回答此问题的两种途径。符号方法推理输入空间的整个区域，并能精确认证比率，但往往难以处理复杂的算术或循环。统计方法则对输入进行采样并应用浓度界。它们具有广泛的适用性，但在故障罕见时可能需要大量样本。我们将这些方法统一到一个框架中，该框架将两者作为特例包含在内。每个估计器有三个组成部分：质量估计器、每叶置信界和符号闭包规则。我们证明，任何满足三个不变量的实例化都会返回包含真实比率的区间，置信度为1-delta，无论其何时停止。认证误差由两部分组成：统计项，通过采样减少；结构项，通过符号闭包减少。纯采样和纯符号执行各自仅减少这两项中的一项。组件的替代选择也使该框架能够支持罕见事件方差缩减方法。
英文摘要
Software in production encounters inputs shaped by how it is used in practice. We study distribution-aware reliability estimation: given a program, its operational input distribution, and a condition of interest, determine how often that condition holds and certify the result with a guaranteed error bound. Symbolic and statistical methods offer two ways to answer this question. Symbolic methods reason about entire regions of the input space and can certify rates exactly, but often struggle with complex arithmetic or loops. Statistical methods instead sample inputs and apply concentration bounds. They are broadly applicable, but can require many samples when failures are rare. We bring these approaches together in a framework that includes both as special cases. Each estimator has three components: a mass estimator, a per-leaf confidence bound, and a symbolic closure rule. We prove that any instantiation satisfying three invariants returns an interval containing the true rate with confidence 1-delta, regardless of when it stops. The certified error has two parts: a statistical term, reduced by sampling, and a structural term, reduced by symbolic closure. Pure sampling and pure symbolic execution each reduce only one of these terms. Alternative choices of the components also allow the framework to support rare-event variance-reduction methods.
