4月13日，第六届云安全联盟大中华区大会（The 6th CSA GCR Congress）在上海成功举办！！

美国哥伦比亚大学常务副校长、美国艺术与科学院院士、IEEE & ACM Fellow 周以真 (Jeannette M. Wing) 通过视频连线，为与会者带来了关于可信AI的精彩演讲。她强调，AI系统在某些任务上已经取得了优异的表现，但也可能产生不公平和残酷的结果。为实现可信AI，我们需要从可信计算的基础上添加一系列属性，包括准确性、健壮性、公平性、问责制、透明度、可解释性和道德性。周以真校长提出了一种实现可信AI的方法，即将正式的数学社区、可信计算社区和人工智能社区结合在一起，采用验证和测试的常用方法来确保AI系统的正确性和满足特定属性。

我想谈谈可信计算中的可信AI。几十年来，计算机科学界在可信计算领域取得了一定进展，其中可信意味着一系列属性，包括可靠性，它做了正确的事吗？安全性，它无害吗？ 防护性，面对攻击，它有多脆弱？隐私性，它是否保护了个人的身份和数据？可用性，当需要访问系统时，它是否可用？易用性，人类可以轻松地使用吗？计算就是硬件和软件的结合，当然还包括使用系统的人。

从可信计算到可信AI，我们正在不断提升。我们不仅需要可信计算的属性，同时还需要新的属性。我们期望这些计算系统具有准确性、稳健性、公平性、问责制、透明度、可解释性，甚至解决AI系统存在的道德问题。

所以从传统的应用形式看，我们有以下公式证明一个程序是正确的，或者表明系统满足一个特定的属性，这个公式有三个部分，M代表程序或协议，或者可以是一个循环分布式系统的数学模型。双转风格代表逻辑和嵌入该逻辑的工具，如模型检测器、定理证明器和可满足性模理论 (smt) 求解器。我们可以用它推理程序，P代表我们在传统形式验证中关心的透明度属性。我们试图证明一段代码的属性。我们使用布尔逻辑和离散逻辑。我们在这个领域取得了很大的进步，实际上已经将这些属性正式描述为安全属性和活跃属性。我们通常通过传统形式验证中的某种时序逻辑正式编写这些属性，有时会要求显式模型程序运行的系统环境，例如，e 可以是操作系统，也可以是特定网络物理系统的物理环境。

请记住验证计算系统的传统方法在可信度方面的两个主要区别，分别是概率推理的需要，以及数据的作用。在本次演讲中，针对数据作用，我们只讨论两个关于未见数据的问题，以及我们要量化什么，因为这些是采用正式方法的社区以前不必解决的新问题。

因此，首先我们必须看看有关数据收集和分区的问题。我们如何将可用的给定数据集划分为训练集和测试集？在构建模型 M 时，我们可以针对所需属性 P 对这个分区做出什么保证？对于给定的属性P，多少数据足以构建模型M？添加更多的数据训练或测试 M 是否使其更健壮、更公平等。或者它对属性 P 没有影响。如果不具备所需的属性，那需要收集什么样的新数据？

如何标记未知的数据是一个很大的难题。我们如何标明数据或表征数据的属性？根据定义，它是未知的。那么我们怎么知道我们还没有看到？正如我之前提到的，我们可以通过它的参数将想法指定为随机过程或数据分布。我们可以使用概率编程语言，例如 stan，它用于指定统计模型。但是那些不适合常见统计模型（如正态分布或猜测分布）的大型现实世界数据集，或者具有数千个参数的大型数据集，更像是我们今天所看到的。我们收集大量数据并使用这些数据构建这些现代机器学习模型。还有一个关于标明未知的数据的问题，这打破了循环推理。为了标明未知的数据，我们需要做出某些假设并对未知数据运用这些假设，而这些假设与那些首先建立模型的假设不同。也就是说，我们如何才能相信 D 的规范？因此，为了打破这种循环推理，我们可能会采用几种方法。一个是统计工具的全部内容，我将在后面的胶片中具体介绍。另一个是从一个更小、足够简单的初始规范开始，可以通过手动检查。然后我们使用这个规范引导一个迭代的细化过程。这个过程很像正式方法中的反例引导抽象和细化。最后，未知数据的规范与训练和测试的数据规范有何关系？

尝试验证可信AI系统的第二个大的新问题是我们要量化什么？在传统的正式方法中，我们努力为所有 x.p(x) 证明这一点。 例如，对于一个特定变量的所有值，一些属性会得以实现。并且如果我们可以为相当多的变量的所有值证明它，那么对于实际使用的任何变量 P 肯定成立。但是对于AI系统，我们并不期望 M 对所有输入数据或所有数据集 D 都有效。

那我们可以量化什么？对于给定的 M，我们如何指定 P 应该具有的分布类别？它可能取决于属性。对于健壮性，在对抗性机器学习系统设置中，我们可能希望证明 M 对所有范数有界扰动 D 是健壮的。更有趣的是，我们可能希望证明 M 对于所有“语义”或“结构”的扰动是健壮的。例如，计算机视觉。在这里，我们知道给熊猫的图片添加一点噪音，在pandas可以看到、完整分类器，所以这个分类器对特定的扰动并不具备健壮性。

那对于像公平这样的不同属性应该怎么实现？为了公平起见，我们可能希望表明机器学习模型在给定数据集和所有未见过的数据集上是公平的，这些数据集对于某种正式的相似概念是相似的。例如，著名的 COMPAS 数据表明，对于累犯风险，该模型可能存在偏差。因此，在我与同事一起完成的去年在欧洲出版的一些工作中，我们展示了采用一个模型是多么容易，该模型在给定的数据分布上具有公平性，并且数据分布非常轻微，以使分类器公平。所以在这种情况下，这个公平模型不是很健壮，在我们发表的报纸上，我们展示了如何建立一个健壮的公平模型。