Polar：一个用于（概率）循环的代数分析器
Polar: An Algebraic Analyzer for (Probabilistic) Loops
AI总结：
Polar通过代数推理自动化分析经典和概率循环，能够推导不变量和参数敏感性，适用于包含if语句、多项式运算和概率分布的循环。
摘要：
我们提出了Polar框架，用于使用代数推理完全自动化分析经典和概率循环。Polar的核心主题是处理能够精确捕捉循环语义的代数递归。为此，我们的工作实现了多种技术来计算变量的高阶矩的递归的精确闭合形式，推导不变量，并推导循环对未知参数的敏感性。Polar可以分析包含if语句、多项式运算和常见概率分布的概率循环。通过将循环分析转化为线性递归求解，Polar利用推导出的递归闭合形式来计算最强的多项式不变量或推断参数敏感性。Polar在well-defined编程模型限制内是正确且完整的。解除任何这些限制会导致计算的显著难度限制。为了克服计算负担以提高效率，Polar还提供不完整但正确的技术来计算变量组合的矩。
英文摘要：
We present the Polar framework for fully automating the analysis of classical and probabilistic loops using algebraic reasoning. The central theme in Polar comes with handling algebraic recurrences that precisely capture the loop semantics. To this end, our work implements a variety of techniques to compute exact closed-forms of recurrences over higher-order moments of variables, infer invariants, and derive loop sensitivities with respect to unknown parameters. Polar can analyze probabilistic loops containing if-statements, polynomial arithmetic, and common probability distributions. By translating loop analysis into linear recurrence solving, Polar uses the derived closed-forms of recurrences to compute the strongest polynomial invariant or to infer parameter sensitivity. Polar is both sound and complete within well-defined programming model restrictions. Lifting any of these restrictions results in significant hardness limits of computation. To overcome computational burdens for the sake of efficiency, Polar also provides incomplete but sound techniques to compute moments of combinations of variables.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
