, стверджує, що розробляє прототип нової мови програмування.){kind=link}
需要高性能計算來解決越來越多的任務——例如圖像處理或神經網絡上的各種深度學習應用程序——在這些任務中，您需要處理大量數據，並且處理得足夠快，否則可能需要大量的時間。 人們普遍認為，在執行此類操作時，速度和可靠性之間的折衷是不可避免的。 根據這種想法，如果速度是優先考慮的因素，那麼可靠性可能會受到影響，反之亦然。
然而，主要位於麻省理工學院 (MIT) 的一組研究人員正在挑戰這一概念，他們認為您實際上可以擁有一切。 麻省理工學院計算機科學與人工智能實驗室 (CSAIL) 的二年級研究生 Amanda Liu 表示，使用他們專門為高性能計算編寫的新編程語言，“速度和正確性不必競爭。 相反，在我們編寫的程序中，它們可以一起並肩而行。” Liu 和她的團隊上個月在費城舉行的編程語言原則會議上談到了他們新創建的張量語言 (ATL) 的潛力。
“我們語言中的一切，”劉說，“都是為了獲得一個數字或一個張量。” 反過來，張量是向量和矩陣的泛化。 向量是一維對象（通常由單個箭頭表示），矩陣是熟悉的二維數字數組，而張量是 n 維數組，可以採用例如 3×3×3 數組的形式，甚至更高（或更低）維度。
計算機算法或程序的本質是啟動某種計算。 但是可以有許多不同的方法來編寫這個程序——正如 Liu 和她的合著者在他們的論文中所寫的那樣，“令人驚訝的各種不同的代碼實現”——其中一些方法明顯快於其他方法。 她解釋說，ATL 背後的主要理由是：“鑑於高性能計算非常耗費資源，您希望能夠以最佳形式修改或重寫程序以加快速度。 通常你從最容易編寫的程序開始，但這可能不是運行它的最快方式，所以你仍然需要做進一步的調整。”
新的命令語言基於現有的 Coq 語言，其中包括一個證明助手。 反過來，證明助手有能力在數學上精確地證明其陳述。 Coq 有另一個特性使它對 MIT 團隊很有吸引力：用該語言編寫的程序，或者它的改編版，總是終止並且不能無限循環地運行。
現在它是第一個也是迄今為止唯一一個經過正式驗證優化的張量語言。 然而，麻省理工學院的團隊警告說，ATL 仍然只是一個原型——儘管它很有希望——已經在許多小程序上進行了測試。
另請閱讀：