SHF: Small: Reasoning Rigorously About Probabilistic Programs

随着社会越来越依赖软件系统来帮助计划医疗、预测未来气候、指导金融市场投资，以及挖掘嘈杂的数据来推断科学事实，输入数据中的不确定性和软件中的缺陷可能会产生虚假警报或虚假安全感的风险很大。这个项目将帮助解决高度复杂的概率程序和有关它们的推理工具之间的差距。概率程序出现在重要的日常应用中，包括医疗、工程和金融风险分析/决策系统、大规模模拟、数据挖掘、用于网络物理系统的传感器噪声过滤算法和随机算法。程序行为中内置的输入不确定性和随机性的存在可能会导致不良行为和可变的性能。因此，准确地预测此类不良行为的概率以及重要性能度量的期望值是很重要的。本项目研究了用于概率程序的自动程序分析工具，该工具将对不确定性的来源进行适当的建模，并推断断言的概率和性能度量的期望的界限。目前正在研究两种类型的推理程序：符号程序--将决策程序与鞅理论相结合--以及使用统计假设检验方法来推断具有统计保证的概率注释的统计程序。

As society becomes increasingly reliant on software systems to helpplan medical treatments, predict the future climate, guide investmentsin financial markets, and mine noisy data to infer scientific facts,the risk that uncertainties in the input data and defects in thesoftware can create false alarms, or a false sense of security, ishigh. This project will help address the gap between highly complexprobabilistic programs and tools for reasoning about them.Probabilistic programs arise in important everyday applications thatinclude medical, engineering and financial risk analysis/decisionmaking systems, large-scale simulations, data mining, sensor noisefiltering algorithms for cyber-physical systems, and randomizedalgorithms. The presence of input uncertainties and randomness builtinto the behavior of the programs can cause undesirable behaviors andvariable performance. Therefore, it is important to accuratelypredict the probabilities of such undesirable behaviors, and expectedvalues for important performance measures.This project investigates automatic program analysis tools forprobabilistic programs that will model the sources of uncertaintyappropriately, and infer bounds on the probabilities of assertions andexpectations of performance measures. Two flavors of inferenceprocedures are being investigated: symbolic procedurescombining decision procedures with the theory of martingales andstatistical procedures using statistical hypothesis testingmethods to infer probabilistic annotations with statisticalguarantees.