圖片來源: 

MIT

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

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

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

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

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

熱門新聞

Advertisement