利用形式化验证结果收紧 PAC 界的评估
Tightening the Evaluation of PAC Bounds Using Formal Verification Results
AI总结：
本文提出利用神经系统的形式化验证结果来评估 PAC 界，通过使用围绕测试点区域的验证结果代替逐点测试信息，证明了在验证结果上条件化现有界能实现与已验证区域概率质量成正比的收紧效果。
摘要：
可能近似正确（PAC）界被广泛用于推导机器学习模型泛化能力的概率保证。它们突出了模型中对其泛化能力有贡献的组成部分。然而，当前最先进的结果在近似已部署机器学习模型的泛化能力时较为宽松。因此，尽管 PAC 界在理论上很有用，但它们在评估模型在给定操作设计域内的泛化特性的适用性是有限的。其底层的经典理论基于这样一个观点：当用户可用于评估模型的测试点数量增加时，可以收紧界。然而，在神经网络的情况下，即使对于小问题，获得感兴趣的界所需的测试点数量通常是不切实际的。在本文中，我们采用了一种新颖的方法，利用神经系统的形式化验证来为 PAC 界的评估提供信息。我们不再使用从重复测试中获得的逐点信息，而是使用围绕测试点区域的验证结果。我们证明了在验证结果上对现有界进行条件化处理，会导致与已验证区域的底层概率质量成正比的收紧。
英文摘要：
Probably Approximately Correct (PAC) bounds are widely used to derive probabilistic guarantees for the generalisation of machine learning models. They highlight the components of the model which contribute to its generalisation capacity. However, current state-of-the-art results are loose in approximating the generalisation capacity of deployed machine learning models. Consequently, while PAC bounds are theoretically useful, their applicability for evaluating a model's generalisation property in a given operational design domain is limited. The underlying classical theory is supported by the idea that bounds can be tightened when the number of test points available to the user to evaluate the model increases. Yet, in the case of neural networks, the number of test points required to obtain bounds of interest is often impractical even for small problems. In this paper, we take the novel approach of using the formal verification of neural systems to inform the evaluation of PAC bounds. Rather than using pointwise information obtained from repeated tests, we use verification results on regions around test points. We show that conditioning existing bounds on verification results leads to a tightening proportional to the underlying probability mass of the verified region.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
