Ji Guan

Ji Guan

官极

Research

Research Focus

My research develops formal methods for trustworthy quantum computing, with a focus on the correctness, security, privacy, and reliability of quantum systems, algorithms, programs, and hardware-facing applications. The long-term goal is to make quantum systems not only powerful, but also verifiable, robust, privacy-preserving, and deployable.

The work connects formal verification, quantum information, quantum programming, quantum machine learning, and NISQ-era algorithm design. It also feeds into VeriQ, our trustworthy quantum computing toolchain.

Core themes: quantum model checking; verification of quantum programs and circuits; robustness, fairness, and privacy in quantum machine learning; quantum algorithms for verification-relevant primitives; NISQ-oriented simulation, synthesis, and chemistry applications.

Publication map: this page highlights representative work by research direction. The full chronological list is available on the Publications page.

Research Modules

Theme 1

Correctness of Quantum Systems

Quantum systems are difficult to verify because their states are continuous, high-dimensional, and measurement-dependent. I study mathematical models, temporal logics, and model-checking algorithms for reasoning about quantum system behavior.

Representative contributions

  • Formal models for quantum Markov chains and quantum continuous-time Markov chains.
  • Decomposition and reachability analysis for long-run quantum system behavior.
  • Temporal/logical specifications for dynamic correctness properties.
  • Verification of emerging quantum programming patterns, including ancilla safety and tensor-network-style state representations.

Related publications

  • Li, J., Mei, J., Fang, W., and Guan, J.*. Formal Verification of Quantum Ancilla Safety. CAV 2026. Accepted · Paper by request
  • Xu, M., Chen, Y., and Guan, J.*. Model Checking Matrix Product States Against Linear Chain Logic. CAV 2026. Accepted · Paper by request
  • Guan, J.*, Feng, Y., Turrini, A., and Ying, M. Measurement-based Verification of Quantum Markov Chains. CAV 2024. Paper · DOI · arXiv
  • Mei, J., Xu, M., Guan, J., Deng, Y., and Yu, N. Checking Continuous Stochastic Logic Against Quantum Continuous-time Markov Chains. LMCS 2025. Paper · DOI · arXiv
  • Guan, J. and Yu, N. A Probabilistic Logic for Verifying Continuous-time Markov Chains. TACAS 2022. Paper · DOI · arXiv
  • Xu, M., Mei, J., Guan, J.*, and Yu, N. Model Checking Quantum Continuous-Time Markov Chains. CONCUR 2021. Paper · DOI · arXiv
  • Guan, J.*, Feng, Y., and Ying, M. Decomposition of Quantum Markov Chains and Its Applications. JCSS 2018. Paper · DOI · arXiv

These results connect with the monograph Model Checking Quantum Systems: Principles and Algorithms by Ying, Feng, Yu, and Duan.

Theme 2

Robust, Fair, and Privacy-Preserving Quantum Algorithms

Quantum machine learning and quantum data-processing pipelines can be vulnerable to noise, adversarial perturbations, and privacy leakage. I develop formal definitions, verification algorithms, and mechanisms for trustworthy quantum learning and privacy.

Representative contributions

  • Formal verification of local/global robustness for quantum classifiers.
  • Fairness verification for quantum machine learning.
  • Differential privacy analysis for quantum algorithms and quantum local privacy mechanisms.
  • Hardware-facing robustness benchmarking and validation on superconducting quantum processors.

Related publications

  • Guan, J.*. Optimal Mechanisms for Quantum Local Differential Privacy. ACM CCS 2025. Paper · DOI · arXiv
  • Guan, J.*, Fang, W., Huang, M., and Ying, M. Detecting Violations of Differential Privacy for Quantum Algorithms. ACM CCS 2023. Paper · DOI · arXiv
  • Guan, J.*, Fang, W., and Ying, M. Verifying Fairness in Quantum Machine Learning. CAV 2022. Paper · DOI · arXiv
  • Guan, J.*, Fang, W., and Ying, M. Robustness Verification of Quantum Classifiers. CAV 2021. Paper · DOI · arXiv
  • Zhang, H. F., Chen, Z. Y., Wang, P., Guo, L. L., Wang, T. L., Yang, X. Y., Zhao, R. Z., Zhao, Z. A., Zhang, S., Du, L., Tao, H. R., …, Guan, J.*, Duan, P., and Guo, G. Experimental Robustness Benchmark of Quantum Neural Network on a Superconducting Quantum Processor. SCIENCE CHINA Physics, Mechanics & Astronomy, 2025. arXiv
  • Guan, J. and Ying, M. Verifying Adversarial Robustness in Quantum Machine Learning: From Theory to Physical Validation via a Software Tool. In Quantum Robustness in Artificial Intelligence. Springer. Chapter · DOI · Chapter PDF
  • Li, C., Ying, M., and Guan, J.*. Differential Privacy of Quantum and Quantum-Inspired-Classical Recommendation Algorithms. arXiv
Theme 3

Quantum Program Analysis, Simulation, and Design Automation

Trustworthy quantum computing needs tools that can analyze quantum programs, optimize circuits, simulate noisy behavior, and check equivalence. I work on formal and algorithmic foundations for quantum design automation and quantum software analysis.

Representative contributions

  • Symbolic simulation and analysis for quantum programs with loops and sequential quantum circuits.
  • Robustness verification tools for quantum machine learning models.
  • Simulation and equivalence checking of noisy quantum circuits.
  • Exact and approximate synthesis/optimization for quantum circuits.

Related publications

  • Li, Z., Guan, J.*, and Ying, M. QSeqSim: A Symbolic Simulator for Qiskit While Loops Using Sequential Quantum Circuits. FM 2026. Paper · DOI · arXiv · PDF · GitHub
  • Li, C., Zhou, X., Guan, J.*, Meng, F., Zhu, P., and Luo, Y. Lin-search: Scaling Exact Synthesis of CNOT Circuits via Hybrid Iterative Deepening Search. DAC 2026. Program · Paper by request
  • Huang, M., Guan, J.*, Fang, W., and Ying, M. Approximation Methods for Simulation and Equivalence Checking of Noisy Quantum Circuits. IEEE TCAD 2025. Paper · DOI · arXiv
  • Lin, Y., Guan, J.*, Fang, W., Ying, M., and Su, Z. A Robustness Verification Tool for Quantum Machine Learning Models. FM 2024. Paper · DOI · arXiv · GitHub
  • Huang, M., Guan, J.*, Fang, W., and Ying, M. Approximation Algorithm for Noisy Quantum Circuit Simulation. DATE 2024. Paper · DOI · arXiv
  • He, R., Guan, J., Hong, X., Cui, G., Wang, S., and Ying, S. RH: An Architecture for Redesigning Quantum Circuits on Quantum Hardware Devices. arXiv
  • Chen, K., Fang, W., Guan, J.*, Hong, X., Huang, M., Liu, J., Wang, Q., and Ying, M. VeriQBench: A Benchmark for Multiple Types of Quantum Circuits. arXiv · GitHub
Theme 4

Quantum Algorithms, NISQ Applications, and Verification Primitives

I also study quantum algorithms and NISQ applications that interact with verification, simulation, and trustworthy computing, including quantum information metrics, quantum games, and chemistry-oriented variational algorithms.

Representative contributions

  • Quantum algorithms for fidelity estimation, entropy, trace distance, and hitting probabilities.
  • VQE ansatz design for chemistry simulations with symmetry and compactness considerations.
  • Quantum game and property-partitioning experiments on superconducting processors.
  • NISQ-oriented methods that connect algorithm design with verification and reliability.

Related publications

  • He, R., Ablimit, A., Hong, X., Chai, Q., Zhou, J., Guan, J., Cui, G., and Ying, S. Hamiltonian-Informed Point Group Symmetry-Respecting Ansätze for the Variational Quantum Eigensolver. Journal of Chemical Theory and Computation, 2026. Paper · DOI · arXiv
  • He, R., Hong, X., Chai, Q., Guan, J., Zhou, J., Ablimit, A., Cui, G., and Ying, S. Constructing Compact ADAPT Unitary Coupled-Cluster Ansatz with Parameter-Based Criterion. Journal of Chemical Theory and Computation, 2026. Paper · DOI · arXiv
  • Jiang, H., Fu, J., Xu, M., Guan, J., and Ying, S. A Quantum Game Designed for Property Partitioning with Implementation on Superconducting Quantum Processors. Theoretical Computer Science, 2026. Paper · DOI
  • Wang, Q., Guan, J., Liu, J., Zhang, Z., and Ying, M. New Quantum Algorithms for Computing Quantum Entropies and Distances. IEEE Transactions on Information Theory, 2024. Paper · DOI · arXiv
  • Wang, Q., Zhang, Z., Chen, K., Guan, J.*, Fang, W., Liu, J., and Ying, M. Quantum Algorithm for Fidelity Estimation. IEEE Transactions on Information Theory, 2022. Paper · DOI · arXiv
  • Guan, J.*, Wang, Q., and Ying, M. An HHL-Based Algorithm for Computing Hitting Probabilities of Quantum Random Walks. Quantum Information & Computation, 2021. Paper · DOI · arXiv

VeriQ Toolchain

VeriQ is our toolchain for trustworthy quantum computing, spanning:

  • Verification and model checking: correctness of quantum systems, Markovian models, and program-level properties.
  • Robustness and privacy: formal verification of quantum machine learning robustness, fairness, and differential privacy.
  • Simulation and equivalence checking: scalable analysis for noisy quantum circuits and dynamic quantum programs.
  • Design automation: circuit synthesis, optimization, benchmarking, and hardware-aware redesign.

Representative tools and artifacts include VeriQR, QSeqSim, VeriQBench, noisy-circuit simulation/equivalence-checking methods, and hardware-facing robustness benchmarks.

Visit VeriQ · View full publication list

Future Research Directions

  1. End-to-end trustworthy quantum software. Develop verification, testing, and certification methods for dynamic quantum circuits, quantum programs with control flow, and hybrid quantum-classical workflows.
  2. Trustworthy quantum machine learning. Build robust, fair, and privacy-preserving quantum learning systems, with both formal guarantees and hardware validation.
  3. Scalable NISQ algorithms and design automation. Improve simulation, synthesis, optimization, and ansatz design for practical NISQ applications, especially when correctness and reliability matter.
  4. Quantum acceleration for formal verification. Explore quantum algorithms for verification-relevant primitives such as fidelity, distance, entropy, and reachability.

These directions continue the central theme of my work: bringing the rigor of formal methods into quantum computing so that future quantum systems can be trusted in practice.