引入純度和類型注釋、捕捉編程錯(cuò)誤，MIT推出低開(kāi)銷量子編程語(yǔ)言Twist

研究者希望 Twist 為創(chuàng)建更多有助于編程人員更易面對(duì)量子計(jì)算挑戰(zhàn)的語(yǔ)言鋪平道路。

與使用比特的傳統(tǒng)計(jì)算機(jī)不同，量子計(jì)算機(jī)使用量子比特（qubit）將信息編碼為 0 或 1，或同時(shí)編碼。再加上量子物理學(xué)的助力，這些冰箱大小的機(jī)器可以處理巨量的信息，但量子計(jì)算機(jī)遠(yuǎn)遠(yuǎn)稱不上完美。就像經(jīng)典計(jì)算機(jī)一樣，我們需要合適的編程語(yǔ)言在量子計(jì)算機(jī)上進(jìn)行計(jì)算。

對(duì)量子計(jì)算機(jī)進(jìn)行編程需要了解糾纏（entanglement），它是用于各種量子比特的計(jì)算乘子，可以轉(zhuǎn)化為強(qiáng)大的能量。當(dāng)兩個(gè)量子比特糾纏時(shí)，一個(gè)量子比特上的行為可以改變另一個(gè)量子比特的值，即使這兩個(gè)量子比特在物理上是分離的，從而引出愛(ài)因斯坦的名言「鬼魅般的超距作用」。

但是，這種能力同樣導(dǎo)致了弱點(diǎn)。在編程時(shí)，如果丟棄一個(gè)量子比特時(shí)沒(méi)有考慮到它與另一個(gè)量子比特的糾纏，則會(huì)破壞另一個(gè)量子比特中存儲(chǔ)的數(shù)據(jù)，進(jìn)而危及程序的正確性。

近日，MIT CSAIL 和 RLE（電子學(xué)研究實(shí)驗(yàn)室）的研究者在論文《Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs》中創(chuàng)建了一種被稱為 Twist 的量子計(jì)算編程語(yǔ)言。Twist 可以通過(guò)一種經(jīng)典計(jì)算機(jī)編程人員理解的語(yǔ)言來(lái)描述和核實(shí)哪些數(shù)據(jù)在量子程序中被糾纏。Twist 語(yǔ)言引入了一種被稱為純度（purity）的概念，這種概念導(dǎo)致糾纏強(qiáng)制缺失，生成了更直觀易懂的程序，并且在理想情況下 bug 更少。

舉例而言，編程人員可以使用 Twist 來(lái)說(shuō)明：一個(gè)程序生成的臨時(shí)垃圾數(shù)據(jù)不與該程序的答案糾纏在一起，因此可以安全地丟棄這些數(shù)據(jù)。

論文地址：https://dl.acm.org/doi/pdf/10.1145/3498691

論文一作、MIT CSAIL 編程系統(tǒng)組（Programming Systems Group）的博士生 Charles Yuan 表示，「通過(guò)顯式地說(shuō)明一個(gè)量子比特何時(shí)不得與另一個(gè)糾纏，Twist 編程語(yǔ)言使得開(kāi)發(fā)人員可以編寫(xiě)更安全的量子程序。并且，因?yàn)槔斫饬孔映绦蛐枰孪攘私饧m纏，我們希望 Twist 為創(chuàng)建更多有助于編程人員更易面對(duì)量子計(jì)算獨(dú)特挑戰(zhàn)的語(yǔ)言鋪平道路?！?/p>

未來(lái)的重要一步是使用 Twist 創(chuàng)建更高級(jí)的量子編程語(yǔ)言。當(dāng)前，大多數(shù)量子編程語(yǔ)言仍然屬于匯編語(yǔ)言，將低級(jí)操作串在一起，沒(méi)有注意到數(shù)據(jù)類型、函數(shù)以及經(jīng)典軟件工程中的典型事物等。

對(duì)于這項(xiàng)工作，芝加哥大學(xué)計(jì)算機(jī)科學(xué)教授、Super.tech 首席科學(xué)家 Fred Chong 說(shuō)道，「量子計(jì)算機(jī)容易出錯(cuò)，并且編程起來(lái)很難。通過(guò)引入程序代碼中的純度并對(duì)它進(jìn)行推理，Twist 語(yǔ)言保證純凈代碼中的量子比特?zé)o法被非代碼中的比特所改變，進(jìn)而朝著更容易的量子編程邁出了一大步?！?/p>

技術(shù)概覽

本文中，研究者將純度形式化為一個(gè)實(shí)現(xiàn)量子程序中糾纏推理的核心工具。就一個(gè)純凈的表達(dá)式而言，它的評(píng)估不受不屬于它的量子比特測(cè)量結(jié)果的影響，這意味著在計(jì)算中不與任何其他表達(dá)式產(chǎn)生糾纏。然后，他們提出了首個(gè)以類型系統(tǒng)為特征的語(yǔ)言 ——Twist，用于對(duì)純度做合理推理。這種類型系統(tǒng)使開(kāi)發(fā)者可以使用類型注釋識(shí)別純凈的表達(dá)式。

Twist 還引入了純度斷言操作符（assertion operator），說(shuō)明量子門(mén)輸出中沒(méi)有糾纏。為了合理地檢查這些斷言，Twist 組合使用了靜態(tài)分析和運(yùn)行時(shí)驗(yàn)證。

研究者使用量子遙傳（quantum teleportation）協(xié)議展示了純度值和 Twist，以及糾纏的力量和門(mén)傳送等技術(shù)的構(gòu)建塊。量子遙傳協(xié)議通過(guò)傳送兩個(gè)經(jīng)典信息比特，將一個(gè)量子比特中存儲(chǔ)的信息傳送到任意距離之外的接收器。下圖 1 展示了一個(gè)用于遙傳延遲測(cè)量變體的量子電路，它將要被傳送的量子比特 q^1 作為輸入。

下圖 2 展示了圖 1 中量子電路的程序，它作為一個(gè)函數(shù)接受量子比特 q^1 并返回傳送的輸出，其中助手（helper）bell_pair 分配了一個(gè)貝爾對(duì)（Bell pair）。

下圖 3 展示了圖 2 中的遙傳程序，使用 Twist 編寫(xiě)，并且純度帶有類型注釋。在 Twist 程序中，每個(gè)量子表達(dá)式都是純凈或混合的類型。其中，純凈表達(dá)式不受其他量子比特測(cè)量影響，而混合表達(dá)式可能受到其他量子比特測(cè)量的影響。

下圖 4 展示了 teleport 函數(shù)的實(shí)現(xiàn)，利用 Twist 的純凈斷言來(lái)可靠地返回一個(gè)純凈輸出。該程序執(zhí)行兩個(gè)步驟以驗(yàn)證 q^3 沒(méi)有與程序中的任何其他量子比特糾纏在一起。

最后，研究者對(duì) Twist 的類型系統(tǒng)進(jìn)行評(píng)估，并在模擬中分析了一組基準(zhǔn)量子程序，證明了 Twist 可以表達(dá)量子算法，捕捉編程錯(cuò)誤，并支持現(xiàn)有量子編程語(yǔ)言不支持的程序，同時(shí)產(chǎn)生的運(yùn)行時(shí)驗(yàn)證開(kāi)銷低于 3.5%

更多細(xì)節(jié)內(nèi)容請(qǐng)參考原論文。

參考鏈接：https://techxplore.com/news/2022-01-language-quantum.html