特斯拉跑车2022：价格、发布窗口、续航里程等

越来越多的任务需要高性能计算——例如图像处理或神经网络上的各种深度学习应用程序——在这些任务中，人们必须处理大量数据，并且速度相当快，否则可能会很荒谬时间。人们普遍认为，在执行此类操作时，在速度和可靠性之间存在不可避免的权衡。根据这种观点，如果速度是重中之重，那么可靠性可能会受到影响，反之亦然。

然而，主要位于麻省理工学院的一组研究人员对这一概念提出了质疑，声称事实上，一个人可以拥有一切。麻省理工学院计算机科学与人工智能实验室 (CSAIL) 的二年级博士生 Amanda Liu 说，使用他们专门为高性能计算编写的新编程语言，“速度和正确性不必竞争. 相反，他们可以在我们编写的程序中携手并进。”

Liu 与加州大学伯克利分校博士后 Gilbert Louis Bernstein、麻省理工学院副教授 Adam Chlipala 和麻省理工学院助理教授 Jonathan Ragan-Kelley 一起描述了他们最近开发的“张量语言”（ATL）的潜力，上个月在费城编程语言原则会议。

“我们语言中的一切，”刘说，“都是为了产生一个数字或一个张量。” 反过来，张量是向量和矩阵的泛化。向量是一维对象（通常由单独的箭头表示），矩阵是熟悉的二维数字数组，而张量是n维数组，例如可以采用 3x3x3 数组的形式，或者更高的形式（或更低）尺寸。

计算机算法或程序的全部意义在于启动特定的计算。但是可以有许多不同的方式来编写这个程序——正如 Liu 和她的合著者在他们即将发表的会议论文中所写的那样，“各种不同的代码实现令人眼花缭乱”——有些方式比其他方式快得多。她解释说，ATL 背后的主要理由是：“鉴于高性能计算非常耗费资源，您希望能够将程序修改或重写为最佳形式以加快速度。人们通常从最容易编写的程序开始，但这可能不是运行它的最快方式，因此仍需要进一步调整。”

例如，假设图像由 100×100 的数字数组表示，每个数字对应一个像素，并且您希望获得这些数字的平均值。这可以在两阶段计算中完成，首先确定每行的平均值，然后获取每列的平均值。ATL 有一个相关的工具包——计算机科学家称之为“框架”——它可以展示如何将这个两步过程转换为更快的一步过程。

“我们可以通过使用一种叫做证明助手的东西来保证这种优化是正确的，”刘说。为此，团队的新语言建立在现有语言 Coq 的基础上，其中包含一个证明助手。反过来，证明助手具有以数学严谨的方式证明其断言的内在能力。

Coq 有另一个内在特性使其对基于 MIT 的团队具有吸引力：用它编写的程序或其改编版总是终止并且不能在无限循环中永远运行（例如，用 Java 编写的程序可能会发生这种情况）。“我们运行一个程序来得到一个单一的答案——一个数字或一个张量，”刘坚持说。“一个永不终止的程序对我们来说毫无用处，但终止是我们通过使用 Coq 免费获得的东西。”

ATL 项目结合了 Ragan-Kelley 和 Chlipala 的两个主要研究兴趣。Ragan-Kelley 长期以来一直关注高性能计算背景下的算法优化。与此同时，Chlipala 更关注算法优化的形式化（如基于数学的）验证。这代表了他们的第一次合作。Bernstein 和 Liu 去年被引入企业，ATL 就是结果。

它现在是第一个，也是迄今为止唯一一个具有正式验证优化的张量语言。然而，Liu 告诫说，ATL 仍然只是一个原型——尽管它很有希望——它已经在许多小程序上进行了测试。“展望未来，我们的主要目标之一是提高 ATL 的可扩展性，以便它可以用于我们在现实世界中看到的更大的程序，”她说。

过去，这些程序的优化通常是手工完成的，而且更加临时，这通常涉及反复试验，有时还会出现大量错误。使用 ATL，Liu 补充说，“人们将能够遵循一种更有原则的方法来重写这些程序——而且这样做更容易，也更能保证正确性。”