MIT研究人員發表高效能運算專用張量語言ATL

MIT研究人員發展專用於高效能運算的程式語言ATL（A Tensor Language），該語言強調能夠兼具效能與可靠性。ATL以程式語言Coq為基礎，並且提供了證明助理，以驗證ATL的最佳化正確無誤。

現在越來越多的應用，像是機器學習與影像處理，皆需仰賴高效能運算，人們普遍認為，在追求速度的同時，可能需要犧牲可靠性，而MIT研究人員則挑戰了此一觀點，研究人員提到，速度和正確性可以不需要競爭，在ATL中可以同時實現。

由於高效能運算非常消耗資源，程式需要以最佳化的形式編寫，來加快執行速度，但是開發人員通常以最容易的方式編寫，因此都需要進一步調整。而ATL便能夠在這種時候幫上忙，針對複雜的運算，ATL提供最佳化程式開發框架，可以將原本多步驟的運算過程，轉換成較少的且較快的運算方法。

ATL建立在現有程式語言Coq之上，並提供了證明助理，該證明助理能以嚴謹的數學方法，證明最佳化的正確性，經證明助理驗證過後的程式，能夠確保最終仍可獲得正確答案。

研究人員提到，過去程式的最佳化不少都要以手動進行，需要經過大量反覆試錯的過程，而ATL提供了更具規則的方式執行程式最佳化。ATL目前是唯一能夠真正驗證其最佳化的張量語言，目前還在初期研究階段，研究人員正提高ATL的可擴展性，以便應用在現實中更大的程式中。