科技日報記者 張佳星

12月20日，《科學》雜志公布十大突破，量子霸權赫然在列。

谷歌的一份論文顯示，面對一個特定的計算任務，量子計算機與第一超級計算機競速結果是200秒：10000年。IBM后來反駁，谷歌沒讓第一超算Summit “好好發揮”，其實差距只是200秒：2.5天。

表面看，似乎是個簡單的問題：量子計算和傳統計算兩個“人”比賽跑，看誰跑得快，就奪得霸權。

事實上，問題復雜得多。一個量子運算是不是正確的？量子程序的正確性如何驗證？千萬行代碼傳遞的指令都正確執行了嗎？這些問題在現行的傳統計算的世界中，很難得到驗證。

同一天，中國科學院軟件研究所及合作團隊正式發布了國內第一個較為完整的量子程序設計平臺isQ，平臺包括量子程序設計、編譯、模擬、分析與驗證等系列工具，擁有編譯器、模擬器、模型檢測工具、定理證明器等功能，正是為量子程序的設計給出一個“指南”，為程序批量的驗證提供平臺。??

從誕生到應用

量子計算需要適宜的新語境

量子計算需要一種適宜的新“語境”，經典編程語境不再適宜。傳統語境只分辨有、無（0與1），量子語境則呈現不同的量子態，并通過疊加和糾纏而以指數級增長的發散式思維解決問題。

“眾所周知, 軟件是計算機的‘靈魂’。一旦量子計算機研制成功, 量子軟件的開發將變成真正發揮量子計算機作用的關鍵。”中科院軟件所學術副所長應明生研究員曾經提到。但由于量子系統與經典世界相比有許多根本不同的特征（如量子信息的不可克隆性、量子糾纏的非局域作用等），經典的軟件理論、方法和技術在很大程度上不能直接適用于量子軟件。

程序調試在軟件開發起到非常重要的作用。在量子計算領域中，一種直接的方法是通過模擬器將經典程序調試的方法嫁接到微型量子程序的調試中去。微軟的一個專利就是這樣做的。這樣的優點是能直接利用已有的手段、方法，缺點是只能針對規模較小的量子程序。

新語言的出現不斷豐富著量子計算的“新語系”。如普林斯頓大學、加州大學圣巴拉拉分校等單位合作的Scaffold等。

量子軟件與經典軟件存在本質不同，相應的量子軟件工具更加復雜而難以研發。為了降低軟件的開發門檻，需要一系列可用性高、功能廣泛而強大，集程序設計、測試、分析、驗證于一體的工具鏈。

在量子程序設計方面，基于對量子語言的充分理解，isQ平臺包含的編譯器能首先將高級語言編寫的量子程序轉化為指令集語言，然后交由后續工具進一步處理。

平臺將幫助程序開發者方便地編寫比較符合程序員思維的高級語言程序，并準確地轉換為量子計算機能理解的指令集語言。未來，平臺可依據不同的硬件，轉換為不同的指令集，實現對多種量子計算機的兼容。?

從表達到有效

程序的驗證之路

量子計算語言所下達的指令是否準確，取決于人類與量子世界的溝通能否達成。?

程序的糾錯與正確性驗證，是量子計算的重要組成部分。目前量子程序規模還比較小，還可以通過人工的方式去完成，比如說寫個兩三百行、上千行的代碼，人工一行一行去檢查錯誤。但如果代碼量到達幾萬行甚至十幾萬行，人工就查不了了。

由于量子程序與傳統計算機程序相比具有很大的不同, 特別是由于量子疊加和糾纏的存在, 量子程序的驗證往往非常困難。

此次發布的國內首個量子程序設計平臺——isQ中包含的定理證明器，是世界上首個能夠對大型量子程序是否正確進行驗證的工具。

“它的實現基于團隊提出的量子Hoare（霍爾）邏輯。” 中科院軟件所量子軟件研究團隊副研究員應圣鋼說，該工具是自主知識產權的成果，可在經典計算機上克服計算時間與存儲空間限制，為較大規模量子程序的設計提供重要幫助。

具體地說，是通過參數化的方式實現邏輯層面的驗證，而不需要真正的在系統中進行數值運算。因此當量子比特數超過目前傳統計算機的模擬運算極限時，這一方法也能夠進行程序的驗證。

利用定理證明器，一臺普通的筆記本電腦也能進行大型量子程序的正確性驗證，而這將是傳統超級計算機無法通過模擬器運算完成的。

據介紹，isQ平臺由中科院軟件所量子軟件研究團隊研發，編譯器和模擬器部分由該團隊與清華大學計算機科學與技術系合作完成。定理證明器將大大提升量子程序的驗證效率，結合前面的程序設計平臺、模擬器、模型檢測工具等，將為量子程序的編寫、糾錯、定型、落地提供系統性的支撐。