在《科學》雜志公布的十大科學突破中，量子霸權赫然在列。但公眾想要真正用上量子計算機，還需要有實際功能的程序落地，需要觸手可及的量子APP。
“眾所周知, 軟件是計算機的‘靈魂’。一旦量子計算機研制成功, 量子軟件的開發(fā)將變成真正發(fā)揮量子計算機作用的關鍵。”中科院軟件所學術副所長應明生表示。
近日，中國科學院軟件研究所及合作團隊正式發(fā)布了國內(nèi)首個量子程序設計平臺——isQ，為量子程序的設計給出“指南”，為程序批量驗證提供平臺。
量子計算需要一種適宜的新語境，經(jīng)典編程語境不再適宜。由于量子系統(tǒng)與經(jīng)典世界相比有許多完全不同的特征，如量子信息的不可克隆性、量子糾纏的非局域作用等。經(jīng)典的軟件理論、方法和技術在很大程度上不能直接適用于量子軟件。
微軟的一個專利是通過模擬器將經(jīng)典程序調(diào)試的方法“嫁接”到微型量子程序的調(diào)試，其優(yōu)點是能直接利用已有的手段、方法，缺點是只能針對規(guī)模較小的量子程序。
基于對量子語言的充分理解，isQ平臺包含的編譯器能首先將高級語言編寫的量子程序轉(zhuǎn)化為指令集語言，然后交由后續(xù)工具進一步處理。平臺將幫助程序開發(fā)者方便地編寫比較符合程序員思維的高級語言程序，并準確地轉(zhuǎn)換為量子計算機能理解的指令集語言。相關研究人員表示，平臺未來可依據(jù)不同的硬件，轉(zhuǎn)換為不同的指令集，實現(xiàn)對多種量子計算機的兼容。
量子計算語言所下達的指令是否準確，取決于人類與量子世界的“溝通”程度。
程序的糾錯與正確性驗證，是量子計算的重要組成部分。目前量子程序規(guī)模還比較小，還可以通過人工的方式去完成，比如說寫個兩三百行、上千行的代碼，人工一行一行去檢查錯誤。但如果代碼量達到幾萬行甚至十幾萬行，人工驗證就失效了。
由于量子程序與傳統(tǒng)計算機程序相比具有很大的不同, 特別是由于量子疊加和糾纏的存在, 量子程序的驗證往往非常困難。
isQ中包含的定理證明器，是世界上首個能夠?qū)Υ笮土孔映绦蚴欠裾_進行驗證的工具。
“它的實現(xiàn)基于團隊提出的量子霍爾邏輯。” 中科院軟件所量子軟件研究團隊副研究員應圣鋼說，該工具是自主知識產(chǎn)權的成果，可在經(jīng)典計算機上克服計算時間與存儲空間的限制，為較大規(guī)模量子程序的設計提供重要幫助。
具體地說，是通過參數(shù)化的方式實現(xiàn)邏輯層面的驗證，而不需要真正地在系統(tǒng)中進行數(shù)值運算。因此當量子比特數(shù)超過目前傳統(tǒng)計算機的模擬運算極限時，這一方法也能夠進行程序的驗證。利用定理證明器，一臺普通的筆記本電腦也能進行大型量子程序的正確性驗證，這是傳統(tǒng)超級計算機通過模擬器運算無法完成的。