麻省理工学院开发的一种新的张量语言，经过正式验证的优化，可能有利于高性能计算。鸣谢:麻省理工学院越来越多的任务需要高性能计算，例如图像处理或神经网络上的各种深度学习应用，在这些任务中，人们必须快速处理大量数据，并以合理的速度完成，否则可能会花费大量时间。人们普遍认为，在执行这类操作时，速度和可靠性之间不可避免地要有所取舍。根据这种观点，如果速度是重中之重，那么可靠性可能会受到影响，反之亦然。然而，一组主要来自麻省理工学院的研究人员对这一观点提出了质疑，他们声称，事实上，一个人可以拥有一切。麻省理工学院计算机科学和人工智能实验室(CSAIL)的二年级博士生刘小源说，有了这种专门为高性能计算编写的新编程语言，“速度和正确性不必竞争。相反，在我们编写的程序中，它们可以携手并进。”
上个月在费城举行的编程语言原理大会上，刘与加州大学伯克利分校博士后吉尔伯特·路易斯·伯恩斯坦、麻省理工学院副教授亚当·奇利帕拉和麻省理工学院助理教授乔纳森·拉冈-凯利一起描述了他们最近开发的发明“张量语言”(ATL)的潜力。
“我们语言中的一切，”刘说，“都是为了产生一个单一的数字或一个张量。”张量又是向量和矩阵的推广。向量是一维对象(通常由单个箭头表示)，矩阵是常见的二维数字数组，而张量是n维数组，例如，可以采用3x3x3数组的形式，或者更高(或更低)维的形式。
计算机算法或程序的全部目的是启动一个特定的计算。但是，可以有许多不同的方式来编写该程序——正如刘和她的合著者在他们即将发表的会议论文中所写的那样，“各种不同的代码实现令人眼花缭乱”——有些方式比其他方式快得多。AT L背后的基本原理是这样的，她解释说:“考虑到高性能计算是如此的资源密集型，为了加快速度，你希望能够修改或重写程序到一个最佳的形式。人们通常从最容易编写的程序开始，但这可能不是运行它的最快方式，因此仍然需要进一步调整。”
例如，假设一个图像由一个100x100的数字数组表示，每个数字对应一个像素，并且您想要获得这些数字的平均值。这可以在两阶段计算中完成，首先确定每行的平均值，然后获得每列的平均值。ATL有一个相关的工具包——计算机科学家称之为“框架”——它可能会显示如何将这个两步过程转换为更快的一步过程。
“我们可以通过使用一种叫做校对助手的东西来保证这种优化是正确的，”刘说。为此，该团队的新语言建立在现有语言Coq的基础上，其中包含一个证明助手。反过来，证明助理具有以数学上严格的方式证明其断言的固有能力。
Coq还有另一个吸引麻省理工学院团队的内在特性:用它编写的程序，或者说它的改编版，总是会终止，并且不能无限循环地运行下去(例如，用Java编写的程序就可能发生这种情况)。“我们运行一个程序来得到一个单一的答案——一个数或一个张量，”刘坚持说。“一个永远不会终止的程序对我们来说是无用的，但终止是我们通过使用Coq免费得到的东西。”
ATL项目结合了拉冈-凯利和奇利帕拉的两个主要研究兴趣。拉冈-凯利长期以来一直关注高性能计算环境中的算法优化。与此同时，Chlipala更关注算法优化的形式(如基于数学的)验证。这是他们的第一次合作。伯恩斯坦和刘是去年被带进企业的，ATL就是其结果。
它现在是第一个，也是迄今为止唯一一个，正式验证优化的张量语言。然而，刘警告说，ATL仍然只是一个原型——尽管是一个很有前途的原型——已经在许多小程序上进行了测试。“展望未来，我们的主要目标之一是提高ATL的可伸缩性，以便它可以用于我们在现实世界中看到的更大的程序，”她说。
在过去，这些程序的优化通常是在更加特别的基础上手工完成的，这通常涉及反复试验，有时还会出现大量错误。刘补充说，有了ATL，“人们将能够遵循一种更有原则的方法来重写这些程序——而且这样做更容易，对正确性的保证也更大。”
这项研究发表在《美国计算机学会编程语言学报》上。
来源：由phyica.com整理转载自PH，转载请保留出处和链接！
