光明網訊（記者肖春芳）12月20日，中國科學院軟件研究所在北京正式發布國內第一個較為完整的量子程序設計平臺，包括量子程序設計、編譯、模擬、分析與驗證等系列工具。

中國科學院軟件研究所所長趙琛

　　最新發布的量子程序設計平臺名稱為“isQ”，“is”代表軟件研究所Institute of Software，“Q”代表量子Quantum。“2016年，軟件所在國內率先部署量子軟件研究方向，成立了量子軟件研究研究室，重點開展量子軟件理論研究和工程實現兩部分工作。今天發布的量子程序設計平臺，就是基于研究團隊多年來，在量子程序設計模型、量子程序邏輯、量子程序分析算法等方面所取得的系統性理論成果基礎上實現的，其中驗證工具是國際首創。”中國科學院軟件研究所所長趙琛說。

　　當前，量子軟件大致可以分為兩類，一類是面向量子算法，其目的是保證量子算法能夠準確地轉化為量子計算機可以執行的量子機器語言；一類是為量子硬件服務，其目的是保障量子芯片能夠有效地設計、運行。現階段，這兩大類軟件均運行于經典計算設備上，是量子計算機開發、運行不可或缺的部分。 “一套可用性高、功能廣泛而強大，集程序設計、測試、分析、驗證于一體的工具鏈對量子軟件開發十分重要。”中國科學院軟件研究所計算機科學國家重點實驗室量子軟件研究團隊副研究員應圣鋼表示，隨著量子芯片規模和電路層數深度的提升，經典計算機上用模擬器運行、調試量子程序所需的時間、空間將成指數增長，最終將無法完成。

國內第一個較為完整的量子程序設計平臺——isQ

　　“我們開發isQ平臺，主要目的就是為了保證量子程序開發的正確性及糾錯的便利性。現在isQ平臺已上線的功能主要分編譯器、模擬器、模型檢測工具、定理證明器四大部分。”應圣鋼介紹說，在量子程序設計方面，編譯器能首先將高級語言編寫的量子程序轉化為指令集語言，然后交由后續工具進一步處理。已上線的模擬器和模型檢測工具就是兩款后續工具。其中，模擬器可在經典計算機上模擬運行量子程序，查看運行結果，對現階段量子程序的設計、測試有重要作用；模型檢測工具可用于檢驗量子系統的各種性質。而定理證明器實現了研究團隊提出的量子霍爾（Hoare）邏輯，是目前已知的世界上唯一能夠對大型量子程序是否正確進行驗證的途徑，可在經典計算機上克服計算時間與存儲空間限制，為較大規模量子程序的設計提供重要幫助。

　　據悉，接下來，研究團隊將在現有理論研究成果及工程化實現的基礎上，進一步完善平臺功能,包括定理證明器與編譯器的對接等；同時，團隊也期望與國內量子硬件團隊緊密合作，盡快將這一平臺配置在中國自主研制的量子計算機上。

[ 責編：宋雅娟 ]