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