Nengkun Yu

Kean Chen, Filippo Girardi, Aadil Oufkir et al.

How many black-box queries to a quantum channel are needed to learn its full classical description? This question lies at the heart of quantum channel tomography (also known as quantum process tomography), a fundamental task in the characterization and validation of quantum hardware. Despite extensive prior work, the optimal query complexity for quantum channel tomography is far from fully understood. In this paper, we study tomography of an unknown quantum channel with input dimension $d_1$, output dimension $d_2$, and Kraus rank at most $r$, to within error $\varepsilon$. We identify the dilation rate $τ= r d_2 / d_1$ (which always satisfies $τ\geq 1$ due to the trace preservation of quantum channels) as a key parameter, and establish that the optimal query complexity of channel tomography exhibits distinct scaling laws across three regimes of $τ$. - In the boundary regime ($τ= 1$): we show that the query complexity is $Θ(r d_1 d_2/\varepsilon)$ for Choi trace norm error $\varepsilon$, and is upper bounded by $O(\min\{r d_1^{1.5} d_2/\varepsilon, r d_1 d_2/\varepsilon^2\})$ and lower bounded by $Ω(r d_1 d_2/\varepsilon)$ for diamond norm error $\varepsilon$. - In the away-from-boundary regime ($τ\geq 1+Ω(1)$): we show that the query complexity is $Θ(r d_1 d_2/\varepsilon^2)$ for both Choi trace norm and diamond norm errors $\varepsilon$. Our results uncover a sharp Heisenberg-to-classical phase transition in the query complexity of quantum channel tomography: at $τ=1$, the optimal query complexity exhibits Heisenberg scaling $1/\varepsilon$, whereas for $τ\geq 1+Ω(1)$, it exhibits classical scaling $1/\varepsilon^2$. In addition, we show that in the near-boundary regime ($1< τ< 1+o(1)$), the query complexity exhibits a mixture of Heisenberg and classical scaling behaviors.

Nengkun Yu, Jens Palsberg, Thomas Reps

Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification techniques are insufficient -- even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents a logic for reasoning in such settings, called SAQR-QC. The logic supports {S}calable but {A}pproximate {Q}uantitative {R}easoning about {Q}uantum {C}ircuits, whence the name. SAQR-QC has three characteristics: (i) some (deliberate) loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) most importantly, to make reasoning scalable, every reasoning step is local -- i.e., it involves just a small number of qubits. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation -- a core subroutine in Shor's factoring algorithm.

Tianrun Zhao, Nengkun Yu

Violation of the Clauser-Horne-Shimony-Holt (CHSH) inequality certifies genuine quantum correlations. In this work, we formalize in Lean 4 the rigidity theorem -- any strategy achieving near-optimal CHSH value must be locally isometric to the canonical qubit strategy. In the course of formalization, we identified a gap in the argument of McKague, Yang, and Scarani (arXiv:1203.2976).

Peng Yan, Nengkun Yu

Quantum key distribution, initialized in 1984, is a commercialized secure communication method which enables two parties to produce shared random secret key by the nature of quantum mechanics. We propose QQUIC (Quantum assisted Quick UDP Internet Connections) transport protocol, which modifies the famous QUIC transport protocol by employing the quantum key distribution instead of the original classical algorithms in the key exchanging stage. Thanks to the provable security of quantum key distribution, the security of QQUIC key does not depend on computational assumptions. Maybe surprisingly, QQUIC can reduce the network latency in some circumstance even comparing with QUIC. To achieve this, the attached quantum connections are used as the dedicated lines for key generation.

Gushu Li, Li Zhou, Nengkun Yu et al.

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two ingenious quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor's algorithm.

Mingsheng Ying, Yuang Feng, Nengkun Yu

Quantum cryptography has been extensively studied in the last twenty years, but information-flow security of quantum computing and communication systems has been almost untouched in the previous research. Duo to the essential difference between classical and quantum systems, formal methods developed for classical systems, including probabilistic systems, cannot be directly applied to quantum systems. This paper defines an automata model in which we can rigorously reason about information-flow security of quantum systems. The model is a quantum generalisation of Goguen and Meseguer's noninterference. The unwinding proof technique for quantum noninterference is developed, and a certain compositionality of security for quantum systems is established. The proposed formalism is then used to prove security of access control in quantum systems.