周以真(英文名Jeannette M. Wing),美国计算机科学家,曾任卡内基-梅隆大学教授。美国国家自然基金会计算与信息科学工程部助理部长。ACM和IEEE会士。她的主要研究领域是形式方法、可信计算、分布式系统、编程语言等。现为哥伦比亚大学数据科学研究院主任、计算机科学教授,其长期研究兴趣主要集中于网络安全、数据隐私以及人工智能。
具有里程碑意义的1999年国家科学院网络空间信任(Trust in Cyberspace 1999 National Academies)报告奠定了可信计算的基础,此后,可信计算持续成为一个活跃的研究领域。
大约在同一时期,美国国家科学基金会(National Science Foundation)启动了一系列关于信任的项目。从始于2001年的可信计算(Trusted Computing)为起点,到2004年的网络信任(Cyber Trust),再到2007年的可信赖计算(Trustworthy Computing),以及2011年的安全可信的网络空间(Secure and Trustworthy Cyberspace),计算机和信息科学与工程理事会(Computer and Information Science and Engineering Directorate)已经发展成可信计算的学术研究社区。虽然它源于计算机科学社区,但现在支持可信计算的研究已跨越了美国国家科学基金会的多个部门,并涉及许多其他资助组织,包括通过网络和信息技术研究与发展(NITRD)计划和20个联邦机构。
M是要验证的对象,它可以是一个程序,也可以是一个复杂系统的抽象模型,例如,并发的、分布式的或反应性的系统。P是用某种离散逻辑表示的正确性属性。例如,M可能是使用锁进行同步的并发程序,而P可能是“无死锁”的。M 是无死锁的证明意味着 M 的任何用户都确信 M 永远不会达到死锁状态。为了证明M满足P,我们使用了形式化的数学逻辑,这是当今可扩展和实用的验证工具的基础,如模型检验器、定理证明器和可满足模理论(SMT)求解器。
特别是当M是一个并发的、分布式或反应式的系统时,在传统的形式方法中,我们经常在验证任务的制定中明确添加系统环境 E 的规范:
M和P的固有的概率性质,因此需要概率推理。ML模型M本身在语义和结构上都不同于典型的计算机程序。如前所述,它具有内在的概率性,从现实世界中获取输入,这些输入可能被数学建模为随机过程,并产生与概率相关的输出。在内部,模型本身是基于概率的;例如,在深度神经网络中,边缘上的标签是概率,节点根据这些概率计算函数。从结构上讲,因为机器生成了 ML 模型,所以 M 本身不一定是人类可读或可理解的;粗略地说,DNN是由if-then-else语句组成的复杂结构,人类不太可能编写这种语句。这种“中间代码”表示在程序分析中开辟了新的研究方向。
属性P本身可以在连续域而非(仅)离散域上表述,和/或使用来自概率和统计的表达式。深度神经网络的稳健性被描述为对连续变量的预测,而公平性的特征是关于相对于实数的损失函数的期望(具体参见Dwork等人的研究)。差分隐私是根据相对于(小)真实值的概率差异来定义的。请注意,就像可信计算的实用性等属性一样,可信 AI 系统的一些所需属性,例如透明度或道德感,尚未形式化或可能无法形式化。对于这些属性,一个考虑法律、政策、行为和社会规则和规范的框架可以提供一个环境,在这个环境中可以回答一个可形式化的问题。简而言之,人工智能系统的验证将仅限于可以形式化的内容。
根据定义,在指定不可见的数据时,我们需要对不可见数据做出某些假设。这些假设会不会和我们一开始建立模型M时所做的假设一样呢?更重要的是:我们如何信任D的规范?这种看似逻辑的僵局类似于传统验证中的问题,给定一个M,我们需要假设元素的规范E和MP中元素E和P的规范是“正确的”。那么在验证过程中,我们可能需要修改E和/或P(甚至M)。为了打破现有的循环推理,一种方法是使用不同的验证方法来检查 D 的规范;这种方法可以借鉴一系列统计工具。另一种方法是假设初始规范足够小或足够简单,可以通过(例如,手动)检查进行检查;然后我们使用这个规范引导一个迭代的细化过程。(我们从形式方法的反例引导抽象和细化方法中获得灵感。)这种细化过程可能需要修改D、M和/或P。
相关工作。形式方法社区最近一直在探索人工智能系统的稳健性,特别是用于自动驾驶汽车的图像处理系统。最先进的VerifAI系统探索了自动驾驶汽车稳健性的验证,依靠模拟来识别执行轨迹,其中网络物理系统(例如,自动驾驶汽车)的控制依赖于嵌入式 ML 模型可能出错。ReluVal和Neurify等工具研究了DNN的稳健性,特别是应用于自动驾驶汽车的安全性,包括自动驾驶汽车和飞机防撞系统。这些工具依靠区间分析来减少状态探索,同时仍然提供强有力的保证。在F1/10赛车平台上,使用Verisig验证基于DNN的控制器的安全性的案例研究为比较不同的DNN配置和输入数据的大小提供了基准,并识别了模拟和验证之间的当前差距。
之前,我们主要关注形式方法中的验证任务。但形式方法的机制最近也成功地用于程序合成。与其对模型 M 进行事后验证,我们能否首先开发一种“构建正确”的方法来构建 M?例如,我们是否可以在训练和测试M时添加所需的可信属性P作为约束,以保证P在部署时成立(可能适用于给定的数据集或一类分布)?这种方法的一种变体是通过在每个步骤检查算法不会不满足不希望行为来指导 ML 算法设计过程。类似地,安全强化学习解决决策过程中的学习策略,其中安全性作为优化的一个因素或探索的外部约束。
2019年10月30日至11月1日,哥伦比亚大学数据科学研究所主办了由 DSI 行业附属机构 Capital One 赞助的关于可信AI的首届研讨会。它汇集了来自形式方法、安全和隐私、公平和机器学习的研究人员。来自业界的发言者对学术界正在追求的各种问题和方法进行了现实检验。与会者确定了研究面临的挑战领域,包括:
通过安全可信的网络空间计划(Secure and Trustworthy Cyberspace Program),国家科学基金会资助了一个由宾夕法尼亚州立大学领导的可信赖机器学习中心,来自斯坦福大学、加州大学伯克利分校、加州大学圣地亚哥分校、弗吉尼亚大学和威斯康星大学的研究人员也参与其中。他们的主要重点是解决对抗性机器学习,补充之前概述的形式方法。(为了充分披露,本文作者是该中心顾问委员会成员。)2019年10月,美国国家科学基金会宣布了一项资助国家人工智能研究所的新计划。它命名的六个主题之一是“可信AI”,强调可靠性、可解释性、隐私性和公平性等属性。