Towards Verified Artificial Intelligence
Sanjit A. Seshia∗, Dorsa Sadigh†, and S. Shankar Sastry∗ ∗University of California, Berkeley † Stanford University
Abstract
Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements. This paper considers Verified AI from a formal methods perspective. We describe five challenges for achieving Verified AI, and five corresponding principles for addressing these challenges.
中文速览
人工智能系统的正确性验证是个棘手难题：如何用严格的数学方法证明一个会"学习"的系统真的按预期工作？这篇文章从形式化方法（formal methods）的视角出发，系统梳理了实现"可验证AI"（Verified AI）面临的五大挑战——环境建模的不确定性、正式规范难以描述模糊任务、学习系统本身难以精确建模、验证算法面对高维空间时的效率瓶颈，以及如何把验证结论转化为可指导设计的保证——并针对每个挑战提出了相应的应对原则，包括学习环境模型、融合数据驱动与形式规范、利用抽象和组合技术缩小搜索空间等。作者以自动紧急制动系统为贯穿全文的具体案例，将理论讨论落地到真实的半自动驾驶场景。这项工作的价值在于为AI安全验证划定了一张清晰的问题地图，指出形式化方法与机器学习需要深度融合，而非各自为战，为后续研究提供了方向性框架。
原文 arXiv:1606.08514;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1606.08514v4