量子霸权登顶《科学》“十大”，同日中国首个量子程序设计平台发布

12月20日，《科学》杂志公布十大突破，量子霸权赫然在列。

谷歌的一份论文显示，面对一个特定的计算任务，量子计算机与第一超级计算机竞速结果是200秒：10000年。IBM后来反驳，谷歌没让第一超算Summit “好好发挥”，其实差距只是200秒：2.5天。

表面看，似乎是个简单的问题：量子计算和传统计算两个“人”比赛跑，看谁跑得快，就夺得霸权。

事实上，问题复杂得多。一个量子运算是不是正确的？量子程序的正确性如何验证？千万行代码传递的指令都正确执行了吗？这些问题在现行的传统计算的世界中，很难得到验证。

同一天，中国科学院软件研究所及合作团队正式发布了国内第一个较为完整的量子程序设计平台isQ，平台包括量子程序设计、编译、模拟、分析与验证等系列工具，拥有编译器、模拟器、模型检测工具、定理证明器等功能，正是为量子程序的设计给出一个“指南”，为程序批量的验证提供平台。  

从诞生到应用

量子计算需要适宜的新语境

量子计算需要一种适宜的新“语境”，经典编程语境不再适宜。传统语境只分辨有、无（0与1），量子语境则呈现不同的量子态，并通过叠加和纠缠而以指数级增长的发散式思维解决问题。

“众所周知, 软件是计算机的‘灵魂’。一旦量子计算机研制成功, 量子软件的开发将变成真正发挥量子计算机作用的关键。”中科院软件所学术副所长应明生研究员曾经提到。但由于量子系统与经典世界相比有许多根本不同的特征（如量子信息的不可克隆性、量子纠缠的非局域作用等），经典的软件理论、方法和技术在很大程度上不能直接适用于量子软件。

程序调试在软件开发起到非常重要的作用。在量子计算领域中，一种直接的方法是通过模拟器将经典程序调试的方法嫁接到微型量子程序的调试中去。微软的一个专利就是这样做的。这样的优点是能直接利用已有的手段、方法，缺点是只能针对规模较小的量子程序。

新语言的出现不断丰富着量子计算的“新语系”。如普林斯顿大学、加州大学圣巴拉拉分校等单位合作的Scaffold等。

量子软件与经典软件存在本质不同，相应的量子软件工具更加复杂而难以研发。为了降低软件的开发门槛，需要一系列可用性高、功能广泛而强大，集程序设计、测试、分析、验证于一体的工具链。

在量子程序设计方面，基于对量子语言的充分理解，isQ平台包含的编译器能首先将高级语言编写的量子程序转化为指令集语言，然后交由后续工具进一步处理。

平台将帮助程序开发者方便地编写比较符合程序员思维的高级语言程序，并准确地转换为量子计算机能理解的指令集语言。未来，平台可依据不同的硬件，转换为不同的指令集，实现对多种量子计算机的兼容。 

从表达到有效

程序的验证之路

量子计算语言所下达的指令是否准确，取决于人类与量子世界的沟通能否达成。 

程序的纠错与正确性验证，是量子计算的重要组成部分。目前量子程序规模还比较小，还可以通过人工的方式去完成，比如说写个两三百行、上千行的代码，人工一行一行去检查错误。但如果代码量到达几万行甚至十几万行，人工就查不了了。

由于量子程序与传统计算机程序相比具有很大的不同, 特别是由于量子叠加和纠缠的存在, 量子程序的验证往往非常困难。

此次发布的国内首个量子程序设计平台——isQ中包含的定理证明器，是世界上首个能够对大型量子程序是否正确进行验证的工具。

“它的实现基于团队提出的量子Hoare（霍尔）逻辑。” 中科院软件所量子软件研究团队副研究员应圣钢说，该工具是自主知识产权的成果，可在经典计算机上克服计算时间与存储空间限制，为较大规模量子程序的设计提供重要帮助。

具体地说，是通过参数化的方式实现逻辑层面的验证，而不需要真正的在系统中进行数值运算。因此当量子比特数超过目前传统计算机的模拟运算极限时，这一方法也能够进行程序的验证。

利用定理证明器，一台普通的笔记本电脑也能进行大型量子程序的正确性验证，而这将是传统超级计算机无法通过模拟器运算完成的。

据介绍，isQ平台由中科院软件所量子软件研究团队研发，编译器和模拟器部分由该团队与清华大学计算机科学与技术系合作完成。定理证明器将大大提升量子程序的验证效率，结合前面的程序设计平台、模拟器、模型检测工具等，将为量子程序的编写、纠错、定型、落地提供系统性的支撑。