1.   量子计算与形式化方法的交叉研究：专注于量子系统的模型检测、可信量子机器学习、量子算法以及量子差分隐私等领域的探索。通过引入形式化验证技术，旨在提高量子算法和量子系统的可靠性与安全性。

2.   量子机器学习与算法优化：开发适用于中等规模噪声量子设备的高鲁棒性量子机器学习模型，涉及高维数据分类、量子态判别等应用。研究涵盖了量子电路训练复杂性、非线性表达能力及量子计算加速效应，着力于提升量子机器学习在图像识别和量子纠缠检测等任务中的性能。

3.   量子工具链开发：主导开发了VeriQ可信量子计算工具链，包括量子设计自动化、量子程序验证与分析、以及可信量子机器学习组件，为量子算法和电路的优化和验证提供完整支持。

4.   量子隐私保护与安全：研究量子差分隐私机制，提出最优算法设计，以保障量子数据处理过程中的隐私与安全性，适用于实际量子计算应用场景。

本人长期从事量子计算与形式化方法交叉领域的研究，并主导多个量子计算和量子机器学习的前沿项目，涵盖量子系统的模型检测、可信量子机器学习算法、量子电路优化、以及量子隐私保护等方向。欢迎具有量子计算、形式化方法等背景的同学加入团队，共同探索形式化方法在量子计算中的应用。

我们提供的研究方向包括但不限于：

• 量子系统的模型检测与形式化验证

• 量子隐私保护机制及量子差分隐私

• 量子（机器学习）算法的设计与优化

• 噪声环境下量子计算资源的高效利用

• 可信量子计算工具链开发

本人长期招生研究生、实习生和博士后，研究组经费充足。欢迎有志于在量子计算与形式化方法领域发展的优秀学子与我联系，共同推动该领域的创新与突破。联系邮箱：guanj@ios.ac.cn

081202-计算机软件与理论

量子软件
量子机器学习
形式化方法

2014-08--2018-08   University of Technology Sydney   量子计算/博士
2010-09--2014-07   四川大学   计算数学/本科

   

2022-10~现在, 中国科学院软件研究所, 副研究员
2019-08~2019-10,RWTH Aachen University, Germany, 访问学者
2018-09~2022-09,中国科学院软件研究所, 特别研究助理

• 程序委员会成员（PC Member）：国际顶级会议 Computer Aided Verification (CAV 2025)，International Conference on Quantum Communications, Networking, and Computing  (QCNC 2025)。

• 编委成员：Frontiers in Computer Science 期刊的 Theoretical Computer Science 专栏。

• 开发团队成员：Q|SI⟩ 量子编程环境的开发团队成员，致力于提供高效的量子编程工具。

• 学术审稿人：为多个顶级会议和期刊提供审稿服务，包括 ASPLOS 2025、CDC 2024、QIP 2024、CSL 2024、AQIS 2023、CAV 2021、IEEE QCE 2022-2024、PLanQC 2021、QPL 2020、COCOON 2018-2019、ICFEM 2019 以及 SIAM Journal on Control and Optimization、Science Bulletin、Journal of Computer Science and Technology、Information Processing Letters 和 IEEE Transactions on Emerging Topics in Computational Intelligence 等。

• 学术访问：2019年8月21日至10月16日，受邀在德国亚琛工业大学 Joost-Pieter Katoen 教授的主持下进行学术访问。

1. 2023年中国科学院青年创新促进会会员

2. 2023年北京市高层次留学人才回国资助（每年约30人）

3. 2023年中国科学院软件研究所杰出青年

4. UTS ARC Discovery Scholarship (August 2014 - February 2018)

5. UTS International Research Scholarship (August 2014 - February 2018)

6. UTS FEIT PhD Post-Thesis Publication Scholarship (March 2018 - June 2018)

（ 1 ） 一种可在量子计算机硬件上实现的量子线路重新设计方法, 发明专利, 2024, 第 3 作者, 专利号: CN118070912A

（ 2 ） 量子电路的故障仿真方法、系统、存储介质和电子设备, 发明专利, 2022, 第 1 作者, 专利号: CN114429095A

（ 3 ） 量子电路的故障仿真方法、系统、存储介质和电子设备, 发明专利, 2022, 第 1 作者, 专利号: CN114429096A

会议论文

1. Lin, Y., Guan, J.*, Fang, W., Ying, M., Su, Z. (2024). A Robustness Verification Tool for Quantum Machine Learning Models. International Symposium on Formal Methods (FM), pp. 403-421. Springer.     [CCF A]

2. Guan, J., Feng, Y., Turrini, A., Ying, M. (2024). Measurement-based Verification of Quantum Markov Chains. International Conference on Computer Aided Verification (CAV), pp. 533-554. Springer.         [CCF A]

3. Huang, M., Guan, J.*, Fang, W., Ying, M. (2024). Approximation Algorithm for Noisy Quantum Circuit Simulation. Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE.                         [CCF B]

4. Guan, J., Fang, W., Huang, M., Ying, M. (2023). Detecting Violations of Differential Privacy for Quantum Algorithms. ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 2277-2291. ACM.         [CCF A]

5. Guan, J., Fang, W., Ying, M. (2022). Verifying Fairness in Quantum Machine Learning. International Conference on Computer Aided Verification (CAV), pp. 408-429. Springer.      [CCF A]

6. Guan, J., Yu, N. (2022). A Probabilistic Logic for Verifying Continuous-time Markov Chains. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 13244. Springer.           [CCF B]

7. Guan, J., Fang, W., Ying, M. (2021). Robustness Verification of Quantum Classifiers. Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 12759. Springer.       [CCF A]

8. Xu, M., Mei, J., Guan, J.*, Yu, N. (2021). Model Checking Quantum Continuous-Time Markov Chains. Concurrency Theory (CONCUR), Leibniz International Proceedings in Informatics (LIPIcs), vol. 203, pp. 13:1-13:17. Schloss Dagstuhl.        [CCF B]

9. Bei, X., Chen, S., Guan, J., Qiao, Y., Sun, X. (2020). From Independent Sets and Vertex Colorings to Isotropic Spaces and Isotropic Decompositions: Another Bridge Between Graphs and Alternating Matrix Spaces. Innovations in Theoretical Computer Science (ITCS), Schloss Dagstuhl. （字母顺序，同等贡献）

期刊论文

1. Wang, Q., Guan, J., Liu, J., Zhang, Z., Ying, M. (2024). New Quantum Algorithms for Computing Quantum Entropies and Distances. IEEE Transactions on Information Theory, 70(8), pp. 5653-5680.         [CCF A]

2. Wang, Q., Zhang, Z., Chen, K., Guan, J*, Fang, W., Liu, J., Ying, M. (2023). Quantum Algorithm for Fidelity Estimation. IEEE Transactions on Information Theory, 69(1), pp. 273-282.           [CCF A]

3. Bei, X., Chen, S., Guan, J., Qiao, Y., Sun, X. (2021). From Independent Sets and Vertex Colorings to Isotropic Spaces and Isotropic Decompositions: Another Bridge Between Graphs and Alternating Matrix Spaces. SIAM Journal on Computing, 50(3), pp. 924-971.（字母顺序，同等贡献）       [CCF A]

4. Guan, J., Wang, Q., Ying, M. (2021). An HHL-Based Algorithm for Computing Hitting Probabilities of Quantum Random Walks. Quantum Information & Computation, 21(5&6), pp. 395-408.

5. Guan, J., Feng, Y., Ying, M. (2018). Decomposition of Quantum Markov Chains and Its Applications. Journal of Computer and System Sciences, 95, pp. 55-68.       [CCF B]

6. Guan, J., Feng, Y., Ying, M. (2018). Super-activating Quantum Memory with Entanglement. Quantum Information & Computation, 18(13&14), pp. 1115-1124. 

7. Su, Z., Guan, J., Li, L. (2018). Efficient Quantum Repeater with Respect to Both Entanglement-Concentration Rate and Complexity of Local Operations and Classical Communication. Physical Review A, 97(1), p. 012325.

8. Liu, S., Wang, X., Zhou, L., Guan, J., et al. (2018). Q|SI⟩: A Quantum Programming Environment. Symposium on Real-Time and Hybrid Systems, Springer.

9. Liu, S. S., Zhou, L., Guan, J., et al. (2017). Q|SI⟩: A Quantum Programming Environment (in Chinese). Sci Sin Inform, 47, pp. 1300–1315.         [CCF A]

1. 针对NISQ时代噪声影响，形式化（在严格数学证明基础上）验证和设计高鲁棒（抗噪声）和高隐私量子机器学习算法：定义了一个用于量子机器学习算法的局部鲁棒性、全局鲁棒性和差分隐私性等可信性质验证和分析的形式化框架：开发算法来形式化验证这些可信性质并通过验证信息来设计高鲁棒性（抗噪声）和具有隐私保护的量子机器学习算法，保障量子机器学习算法（在NISQ时代）的安全可靠运行。这系列工作作为量子计算领域仅有的两篇被接受的工作已经发表在国际计算机辅助验证最好的（中国计算机协会CCF A类）会议CAV 2021和2022 上，以及安全领域国际四大会议（CCF A类）之一的ACM CCS 2023上，相关工具发表在软件工程旗舰会议（CCF A类）FM 2024上。这系列工作获得审稿人高度评价“It is an important first step on the field.” “In any case, this is the first published algorithm for solving the given problem.”开创了一个新的研究方向并取得突破。

2. ​估计保真度的量子（指数）加速算法：与合作者利用量子奇异值变换和量子幅度估计等算法，设计出了首个针对低秩混合量子态的计算量子保真度的多项式算法，相比于已知的最好算法有指数级加速。我们技术上的贡献是，将酉算子的块编码推广至量子态的块编码，并将块编码的技术推广至在某些条件下不依赖于其条件数。此外该算法被进一步扩展去计算迹距离和熵等一些列重要的量子信息量。相关工作发表在国际信息论方向最好的期刊（CCF A类）IEEE TIT 2023 和2024上。此外，因为量子算法的鲁棒性和隐私性主要依靠保真度及迹距离等度量来定义，所以这一系列量子（指数）加速算法可以在容错量子计算时代用于在量子计算机上验证量子算法的鲁棒性和隐私性。

3. 模型检测量子系统，用于形式化验证系统设计的正确性：提出多种量子时序逻辑用于表示量子系统的演化性质并开发模型检测算法来自动化检测量子系统（包括量子通讯协议、算法、程序等）的正确性，保证系统按照预期设计运行。这系列相关成果发表在形式化方法国际顶级或知名会议和期刊上，包括CCF A类：CAV 2024，CCF B类：JCSS 2018、CONCUR 2021、TACAS 2022等。

4. 可信量子计算工具链VeriQ：与应明生教授联合领导一个名为 VeriQ 的可信量子计算工具链的开发项目，其中包括 (1) QDA（量子芯片设计自动化）、(2) 量子程序验证和分析以及 (3) 可信量子机器学习。目前已经上线10个相关工具。VeriQ也是国际上第一个较为完整的可信量子计算工具链，为开发安全可靠的量子系统打下理论和工程基础。查看网站https://www.veri-q.com。

5. 量子噪声模拟器：基于张量网络，通过奇异值分解方法，提出高效含噪量子电路的模拟方法，能支持上百含噪量子比特电路近似模拟。相关成果发表在国际芯片设计自动化的三大会议之一DATE 2024 上，并且相关技术已经获批国家发明专利。

6. 硬件对接：本人所开发的QDA工具和模型检测工具已经成功嵌入到所在团队开发的量子程序设计语言isQ中，用于量子电路的编译优化并保证其正确性，并对接国际领先的超导量子芯片“祖冲之二号”，促进软硬件融合，帮助量子芯片高效可靠运行。

（ 1 ） 量子机器学习鲁棒性的形式化验证与训练, 负责人, 国家任务, 2025-01--2027-12
（ 2 ） 北京市高层次留学人才回国资助---可信量子机器学习平台, 负责人, 地方任务, 2023-06--2024-05
（ 3 ） 中国科学院青年创新促进会, 负责人, 中国科学院计划, 2023-01--2026-12
（ 4 ） 量子马尔可夫链可达性的定量分析:量子算法与工具, 负责人, 境内委托项目, 2022-05--2023-04
（ 5 ） 量子程序设计的理论基础, 参与, 国家任务, 2019-05--2023-12
（ 6 ） 量子程序设计理论,方法与工具, 参与, 国家任务, 2018-05--2023-04

现指导学生

周正扬  硕士研究生  081200-计算机科学与技术