通过重新参数化验证ML系统
Verification of ML Systems via Reparameterization
摘要：
随着机器学习越来越多地用于基本系统，减少或消除严重错误的发生率非常重要。越来越多的研究已经开发出机器学习算法，这些算法具有关于性能、鲁棒性或公平性的正式保证。然而，这些算法的分析通常是复杂的，并且在实践中实现这样的系统引入了错误的空间。证明助手可以用于通过构造排除此类错误的机器检查的正确性证明来正式验证机器学习系统。然而，在证明助手内部关于概率性声明的推理仍然具有挑战性。我们展示了如何一个概率程序可以自动表示在一个定理证明使用的概念\emph{reparameterization}，以及如何一些繁琐的证明可测性可以自动生成的概率程序。为了证明这种方法足够广泛，可以处理不同类型的机器学习系统，我们验证了统计学习理论的经典结果（决策树桩的PAC可学习性），并证明贝叶斯假设检验中使用的零模型满足称为人口统计学平价的公平性标准。
英文摘要：
As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machine learning algorithms with formal guarantees about performance, robustness, or fairness. Yet, the analysis of these algorithms is often complex, and implementing such systems in practice introduces room for error. Proof assistants can be used to formally verify machine learning systems by constructing machine checked proofs of correctness that rule out such bugs. However, reasoning about probabilistic claims inside of a proof assistant remains challenging. We show how a probabilistic program can be automatically represented in a theorem prover using the concept of \emph{reparameterization}, and how some of the tedious proofs of measurability can be generated automatically from the probabilistic program. To demonstrate that this approach is broad enough to handle rather different types of machine learning systems, we verify both a classic result from statistical learning theory (PAC-learnability of decision stumps) and prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
