光明网讯（记者肖春芳）12月20日，中国科学院软件研究所在北京正式发布国内第一个较为完整的量子程序设计平台，包括量子程序设计、编译、模拟、分析与验证等系列工具。
中国科学院软件研究所所长赵琛
最新发布的量子程序设计平台名称为“isQ”，“is”代表软件研究所Institute of Software，“Q”代表量子Quantum。“2016年，软件所在国内率先部署量子软件研究方向，成立了量子软件研究研究室，重点开展量子软件理论研究和工程实现两部分工作。今天发布的量子程序设计平台，就是基于研究团队多年来，在量子程序设计模型、量子程序逻辑、量子程序分析算法等方面所取得的系统性理论成果基础上实现的，其中验证工具是国际首创。”中国科学院软件研究所所长赵琛说。
当前，量子软件大致可以分为两类，一类是面向量子算法，其目的是保证量子算法能够准确地转化为量子计算机可以执行的量子机器语言；一类是为量子硬件服务，其目的是保障量子芯片能够有效地设计、运行。现阶段，这两大类软件均运行于经典计算设备上，是量子计算机开发、运行不可或缺的部分。
“一套可用性高、功能广泛而强大，集程序设计、测试、分析、验证于一体的工具链对量子软件开发十分重要。”中国科学院软件研究所计算机科学国家重点实验室量子软件研究团队副研究员应圣钢表示，随着量子芯片规模和电路层数深度的提升，经典计算机上用模拟器运行、调试量子程序所需的时间、空间将成指数增长，最终将无法完成。
国内第一个较为完整的量子程序设计平台——isQ
“我们开发isQ平台，主要目的就是为了保证量子程序开发的正确性及纠错的便利性。现在isQ平台已上线的功能主要分编译器、模拟器、模型检测工具、定理证明器四大部分。”应圣钢介绍说，在量子程序设计方面，编译器能首先将高级语言编写的量子程序转化为指令集语言，然后交由后续工具进一步处理。已上线的模拟器和模型检测工具就是两款后续工具。其中，模拟器可在经典计算机上模拟运行量子程序，查看运行结果，对现阶段量子程序的设计、测试有重要作用；模型检测工具可用于检验量子系统的各种性质。而定理证明器实现了研究团队提出的量子霍尔（Hoare）逻辑，是目前已知的世界上唯一能够对大型量子程序是否正确进行验证的途径，可在经典计算机上克服计算时间与存储空间限制，为较大规模量子程序的设计提供重要帮助。
据悉，接下来，研究团队将在现有理论研究成果及工程化实现的基础上，进一步完善平台功能,包括定理证明器与编译器的对接等；同时，团队也期望与国内量子硬件团队紧密合作，尽快将这一平台配置在中国自主研制的量子计算机上。
[ 责编：宋雅娟 ]