机器学习的形式化方法综述
A Review of Formal Methods applied to Machine Learning
摘要：
我们回顾了应用于机器学习系统验证这一新兴领域的最先进的形式化方法。形式化方法可以对硬件和软件系统提供严格的正确性保证。得益于成熟工具的可用性，它们的使用在行业中得到了很好的认可，特别是在经过严格的认证过程时，用于检查安全关键应用。随着机器学习变得越来越流行，现在考虑将机器学习组件包含在关键系统中。这就提出了核武器的安全和核查问题。然而，已建立的形式化方法仅限于经典的，即非机器学习的软件。应用形式化的方法来验证包括机器学习的系统只是最近才被考虑，并在可靠性，精度和可扩展性方面提出了新的挑战。我们首先回顾建立正式的方法和他们目前使用的一个范例的安全关键领域，航空电子软件，重点是抽象的解释为基础的技术，因为它们提供了一个高层次的可扩展性。这为机器学习验证提供了一个黄金标准并设定了很高的期望。然后，我们提供了一个全面和详细的审查正式的方法，迄今为止开发的机器学习，突出他们的优势和局限性。他们中的大多数验证训练过的神经网络，并采用SMT，优化或抽象解释技术。我们还讨论了支持向量机和决策树集成的方法，以及针对训练和数据准备的方法，这是机器学习的关键但经常被忽视的方面。最后，我们对机器学习系统的形式化验证的未来研究方向提供了展望。
英文摘要：
We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems that include machine learning has only been considered recently and poses novel challenges in soundness, precision, and scalability. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software, with a focus on abstract interpretation based techniques as they provide a high level of scalability. This provides a golden standard and sets high expectations for machine learning verification. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations. The large majority of them verify trained neural networks and employ either SMT, optimization, or abstract interpretation techniques. We also discuss methods for support vector machines and decision tree ensembles, as well as methods targeting training and data preparation, which are critical but often neglected aspects of machine learning. Finally, we offer perspectives for future research directions towards the formal verification of machine learning systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
