软件、网络攻击和人工智能系统安全。4 因此,人工智能系统的验证和确认问题,以及更广泛地说,实现值得信赖的人工智能的问题,39 已开始引起研究界的关注。我们将“经过验证的人工智能”定义为设计具有强大、理想情况下可证明的正确性保证的人工智能系统的目标,这些保证对于数学指定的要求是正确的。我们如何实现这一目标?在本文中,我们从形式化方法的角度考虑经过验证的人工智能的挑战,形式化方法是一个计算机科学和工程领域,涉及系统的严格数学规范、设计和验证。38 形式化方法的核心在于证明:制定形成证明义务的规范;设计系统以满足这些义务;并通过算法证明搜索验证系统确实符合其规范。从规范驱动的测试和仿真到模型检查和定理证明,一系列形式化方法通常用于集成电路 (IC) 的计算机辅助设计,并已广泛应用于查找软件中的错误、分析信息物理系统 (CPS) 和查找安全漏洞。我们回顾了