SearcharxivSearch

arXiv subjects

Hongshun Yao

Publications and source records attributed to Hongshun Yao.

At least 19 recordsLinked to original sources

Quantum Compiler Design for Fault-Tolerant Quantum Computing

Scalable quantum computation is expected to rely on fault-tolerant quantum computation (FTQC), in which quantum error correction (QEC) suppresses physical errors sufficiently to support reliable logical operations. This requires quantum compilation to move beyond general-purpose circuit optimization toward encoding-aware and protocol-structured compilation across the full stack of fault-tolerant quantum computers. Beyond circuit synthesis and hardware mapping, an FTQC compiler must lower algorithm-level operations into the logical gate set supported by the chosen code, coordinate encoded data and ancilla resources, realize logical operations together with repeated syndrome extraction under hardware constraints, and provide the resulting measurement stream to real-time decoding. This survey presents a full-stack view of compiler design for QEC-protected quantum computation. We organize existing work into three interacting layers: logical-level QEC compilation, physical-level QEC realization, and decoder runtime integration. At the logical level, we review surface-code lattice-surgery compilers, beyond-surface-code code-surgery frameworks including emerging qLDPC approaches, and compilation support for non-Clifford operations such as magic-state distillation and code switching. At the physical level, we survey hardware-aware QEC realization on superconducting, trapped-ion, and neutral-atom platforms. We further examine decoder models, real-time decoding systems, and frame-management mechanisms that close the feedback loop during fault-tolerant execution. Finally, we identify open challenges in cross-layer optimization, qLDPC compilation, compiler-decoder co-design, runtime adaptivity, and the development of integrated and benchmarkable FTQC compilation stacks. An actively maintained paper list is available at: github.com/chenghongz/QEC-compiler-design.

quant-ph

Phase-Stable Hologram Updates for Large-Scale Neutral-Atom Array Reconfiguration

Dynamic holographic optical tweezers provide a programmable route to array assembly and reconfiguration essential for scalable neutral-atom quantum computation. However, phase mismatch between successive holograms can cause destructive interference during finite spatial light modulator (SLM) refresh. In this work, we analyze finite SLM refresh to establish a phase-stability criterion for prescribed trap amplitudes and develop a weighted-projective Gerchberg-Saxton (WPGS) method that efficiently approximates the corresponding phase-only complex-field optimization. Enforcing this phase constraint also reduces the number of iterations required for each update, achieving convergence within five iterations and enabling hologram generation within a few milliseconds. Numerical simulations of 2D and 3D reconfiguration involving more than $10^3$ traps, together with nonuniform-intensity interlayer transport, show that WPGS preserves endpoint intensity quality while suppressing inter-frame phase mismatch, transient intensity degradation, trap splitting, and motional heating. Similar suppression of phase mismatch and transient-intensity degradation is maintained under Gaussian SLM-plane illumination. These results establish the phase-stability criterion as a practical design principle for dynamic holographic control and scalable neutral-atom array reconfiguration.

quant-ph

An exchange-assisted entangling gate between 87Rb and 171Yb Rydberg atoms

Neutral-atom tweezer arrays support scalable quantum information processing. Dual-species $^{87}\mathrm{Rb}$--$^{171}\mathrm{Yb}$ arrays combine long-lived ytterbium nuclear-spin data qubits with fast, species-selective rubidium ancilla control and readout. However, realizing interspecies gates without inducing destructive Stark mixing in divalent atoms remains an outstanding problem. Here, we identify an optically accessible $S{+}S\leftrightarrow P{+}P$ Förster resonance at zero electric field, providing strong dipole-dipole exchange at array pitch. Using a shaped optical pulse under finite control response, we demonstrate a $0.36\,μ\mathrm{s}$ exchange-assisted controlled-$Z$ gate with an intrinsic fidelity of $99.91\%$, remaining above $99.85\%$ under bounded perturbations. We also identify an auxiliary repulsive van der Waals channel, providing a comprehensive toolbox for hybrid quantum processors.

quant-ph

Exact Virtual Channel Programming with Vanishing Excess Overhead

A finite-dimensional physical processor cannot exactly program a continuous family of distinct unitary channels. We show that this obstruction becomes quantitative when the target channel is stored in a normalized Choi state and its output observables are reconstructed by sampling physical channels and classically post-processing their measurement outcomes. For arbitrary $d$-dimensional channels, we construct a target-independent exact reconstruction protocol and prove the optimal one-copy sampling overhead, which grows quadratically with system dimension. We further prove the sharp fixed-$d$ law that the excess overhead vanishes inversely with the number of identical Choi programs. The upper bound combines deterministic port-based teleportation with a quasi-decomposition that corrects its depolarizing distortion. The converse maps any low-overhead reconstruction protocol to a physical learner of unknown unitaries and uses local quantum estimation to recover the same leading coefficient. These results recast the universal no-programming obstruction as a quantitative trade-off between quantum program memory and classical sampling, with a leading cost that reflects the locally learnable unitary degrees of freedom.

quant-ph

Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information

Formal verification is becoming increasingly practical for quantum computing, yet the ability of AI agents to construct machine-checkable proofs in this domain remains unmeasured. We introduce Lean-QuantumAlg-Bench and Lean-QIT-Bench, two Lean 4 benchmarks containing 36 and 40 theorem-completion tasks for quantum algorithms and quantum information theory, respectively. Every task compiles in a fixed environment and is evaluated by deterministic proof checking and targeted semantic review, with difficulty weights assigned before model execution. We evaluate four models-GPT-5.5, Kimi K3, DeepSeek V4-Pro, and MiniMax M3-within a common theorem-proving framework under two settings: a task-only baseline and library-augmented deduction (LAD), which additionally provides access to a verified domain library. The highest difficulty-weighted scores are 60.4 out of 100 on the quantum-algorithm benchmark and 59.6 out of 100 on the quantum-information benchmark. LAD improves both score and completion rate in all eight model-benchmark comparisons, with gains of up to 15.9 points, providing evidence that verified libraries can strengthen domain-specific proof agents. The results reveal recurring weaknesses of agentic proving in areas such as quantum simulation, quantum learning, quantum information measures, and entanglement theory. Monetary and wall-clock costs per score point also vary substantially across models, highlighting important capability-efficiency trade-offs. We expect these benchmarks to establish a reproducible baseline for developing more capable and reliable proof agents, and to pave the way toward self-evolving AI scientists for advancing quantum information science.

quant-ph

Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256

Large language models are increasingly assisting with demanding formal theorem-proving tasks, particularly when grounded in machine-checked libraries such as Lean. Agentic systems further amplify this process by searching, reusing, and extending existing formal developments to uncover new discoveries. In quantum computing, Shor's algorithm and its variants present such a demanding case for Lean formalization. In this work, we formalize this algorithm family in Lean through agentic formalization: software agents analyze sources, write Lean code and repair proofs, with human review of the scientific claims and machine checking of the resulting formal proofs. Our formalization develops the mathematical foundations for analyzing quantum attacks in two cryptographic settings: a 2048-bit modulus in the RSA-2048 and the standardized elliptic curve over a 256-bit prime field (P-256). To support these analyses, the formalization ranges from quantum algorithms for order finding to reversible quantum circuits for modular and elliptic-curve arithmetic. Based on [Quantum 5, 433] and [ASIACRYPT 2017, 241--270], we formalize the logical resource estimates for RSA-2048 and P-256, respectively, and provide additional estimates of classical operations. We expect the results pave the way for broader machine-checked quantum cryptanalysis and represent a step toward AI-assisted design and verification of quantum algorithms.

quant-ph

An Agentic Formalization for Certified Quantum Neural Network Design

A central model in quantum machine learning is the quantum neural network (QNN), whose design requires balancing expressivity and trainability. Technically, expressivity is studied through circuit-function analysis, such as quantum signal processing, while trainability is analyzed using dynamical-Lie-algebra (DLA) methods. To support certified QNN design, we formalize these major components of QNN theory in a connected lean 4 development checked by a proof kernel, where every analytic input is either proved or exposed as a named hypothesis. On the expressivity side, we prove exact if-and-only-if characterizations of single-qubit QNNs, a resource-counted quantum phase processing theorem, and an overparameterization ceiling that bounds the quantum Fisher information rank by the DLA dimension. On the trainability side, we derive the direct-sum loss-variance law through a de-circularized second-moment interface. A parameterized Casimir-uniqueness engine discharges the required inputs for fully controllable, orthogonal, and matchgate circuit families, while single-qubit and product-Clifford ensembles close the two-design assumptions directly. A capstone theorem pairs the conditional variance law with exact loss reconstruction in DLA coordinates. The development record identifies eight corrections and clarifications that were not explicit in the informal arguments. We expect this work to provide a machine-checkable foundation for QNN theory and a step toward AI-assisted or automated design of quantum machine learning algorithms.

quant-ph

Block Coordinate Descent for Dynamic Portfolio Optimization on Finite-Precision Coherent Ising Machines

Coherent Ising machines (CIMs) have emerged as specialized quantum hardware for large-scale combinatorial optimization. However, for large instances that remain challenging for classical methods, some platforms support only finite-precision inputs, and the required scaling and quantization can degrade solution quality. Dynamic portfolio optimization (DPO) can be formulated as a quadratic unconstrained binary optimization (QUBO) problem, but large instances are especially vulnerable to precision loss under global scaling. We propose a block coordinate descent method that decomposes the DPO model along the time dimension and iteratively solves compact time-block subproblems on the device. Experiments on finite-precision CIM hardware show that the method enables these instances to be solved under hardware precision limits, yields portfolios competitive with classical benchmark solvers, and reduces runtime through fast CIM solution of the resulting subproblems. These results demonstrate the promise of finite-precision CIMs as a practical and scalable approach to structured large-scale combinatorial optimization.

quant-ph

Programmable Open Quantum Systems

Programmability is a unifying paradigm for enacting families of quantum transformations via fixed processors and program states, with a fundamental role and broad impact in quantum computation and control. While there has been a shift from viewing open systems solely as a source of error to treating them as a computational resource, their programmability remains largely unexplored. In this work, we develop a framework that characterizes and quantifies the programmability of Lindbladian semigroups by combining physically implementable retrieval maps with time varying program states. Within this framework, we identify quantum programmable classes enabled by symmetry and stochastic structure, including covariant semigroups and fully dissipative Pauli Lindbladians with finite program dimension. We further provide a necessary condition for physical programmability that rules out coherent generators and typical dissipators generating amplitude damping. For such nonphysically programmable cases, we construct explicit protocols with finite resources. Finally, we introduce an operational programming cost, defined via the number of samples required to program the Lindbladian, and establish its core structural properties, such as continuity and faithfulness. These results provide a notion of programming cost for Lindbladians, bridge programmable channel theory and open system dynamics, and yield symmetry driven compression schemes and actionable resource estimates for semigroup simulation and control in noisy quantum technologies.

quant-ph

Quantifying Unextendibility via Virtual State Extension

Monogamy of entanglement, which limits how entanglement can be shared among multiple parties, is a fundamental feature underpinning the privacy of quantum communication. In this work, we introduce a novel operational framework to quantify the unshareability or unextendibility of entanglement via a virtual state-extension task. The virtual extension cost is defined as the minimum simulation cost of a randomized protocol that reproduces the marginals of a $k$-extension. For the important family of isotropic states, we derive an exact closed-form expression for this cost. Our central result establishes a tight connection: the virtual extension cost of a maximally entangled state equals the optimal simulation cost of universal virtual quantum broadcasting. Using the algebra of partially transposed permutation matrices, we obtain an analytical formula and construct an explicit quantum circuit for the optimal broadcasting protocol, thereby resolving an open question in quantum broadcasting. We further relate the virtual extension cost to the absolute robustness of unextendibility, providing it with a clear operational meaning, and show that the virtual extension cost is an entanglement measure that bounds distillable entanglement and connects to logarithmic negativity.

quant-ph

Conclusive exclusion of quantum states with group action

Retrieving classical information from quantum systems is central to quantum information processing. As a more general task than quantum state discrimination, which focuses on identifying the exact state, quantum state exclusion only requires ruling out options, revealing fundamental limits of information extraction from quantum systems. In this work, we study the conclusive exclusion of quantum states generated by group actions, establishing explicit criteria for when such exclusion is possible. For systems with complex symmetries, including finite and compact Lie groups, we derive a sufficient condition for conclusive exclusion based on the initial state's amplitudes and the group's structure. As applications to special groups such as Abelian groups, we establish necessary and sufficient conditions for conclusive state exclusion and generalize the Pusey-Barrett-Rudolph result to a wider range of scenarios. Finally, we explore zero-error communication via conclusive exclusion of quantum states and derive a lower bound on the feedback-assisted and non-signalling-assisted zero-error capacity of classical-quantum channels generated by group actions.

quant-ph

Near-Optimal Simultaneous Estimation of Quantum State Moments

Estimating nonlinear properties such as Rényi entropies and observable-weighted moments serves as a central strategy for spectrum spectroscopy, which is fundamental to property prediction and analysis in quantum information science, statistical mechanics, and many-body physics. However, existing approaches are susceptible to noise and require significant resources, making them challenging for near-term quantum hardware. In this work, we introduce a framework for resource-efficient simultaneous estimation of quantum state moments via qubit reuse. For an $m$-qubit quantum state $ρ$, our method achieves the simultaneous estimation of the full hierarchy of moments $\text{Tr}(ρ^2), \dots, \text{Tr}(ρ^k)$, as well as arbitrary polynomial functionals and their observable-weighted counterparts. By leveraging qubit reset operations, our core circuit for simultaneous moment estimation requires only $2m+1$ physical qubits and $\mathcal{O}(k)$ CSWAP gates, achieving a near-optimal sample complexity of $\mathcal{O}(k \log k / \varepsilon^2)$. We demonstrate this protocol's utility by showing that the estimated moments yield tight bounds on a state's maximum eigenvalue and present applications in quantum virtual cooling to access low-energy states of the Heisenberg model. Furthermore, we show the protocol's viability on near-term quantum hardware by experimentally measuring higher-order Rényi entropy on a superconducting quantum processor. Our method provides a scalable and resource-efficient route to quantum system characterization and spectroscopy on near-term quantum hardware.

quant-ph

No-Go Theorems for Universal Quantum State Purification via Classically Simulable Operations

Quantum state purification, a process that aims to recover a state closer to a system's principal eigenstate from multiple copies of an unknown noisy quantum state, is crucial for restoring noisy states to a more useful form in quantum information processing. Fault-tolerant quantum computation relies on stabilizer operations, which are classically simulable protocols critical for error correction but inherently limited in computational power. In this work, we investigate the limitations of classically simulable operations for quantum state purification. We demonstrate that while certain classically simulable operations can enhance fidelity for specific noisy state ensembles, they cannot achieve universal purification. We prove that neither deterministic nor probabilistic protocols using only classically simulable operations can achieve universal purification of two-copy noisy states for qubit systems and all odd dimensions. We further extend this no-go result of state purification using three and four copies via numerical solutions of semidefinite programs. Our findings highlight the indispensable role of non-stabilizer resources and the inherent limitations of classically simulable operations in quantum state purification, emphasizing the necessity of harnessing the full power of quantum operations for more robust quantum information processing.

quant-ph

LCQNN: Linear Combination of Quantum Neural Networks

Quantum neural networks combine quantum computing with advanced data-driven methods, offering promising applications in quantum machine learning. However, the optimal paradigm for balancing trainability and expressivity in QNNs remains an open question. To address this, we introduce the Linear Combination of Quantum Neural Networks (LCQNN) framework, which uses the linear combination of unitaries concept to create a tunable design that mitigates vanishing gradients without incurring excessive classical simulability. We show how specific structural choices, such as adopting $k$-local control unitaries or restricting the model to certain group-theoretic subspaces, prevent gradients from collapsing while maintaining sufficient expressivity for complex tasks. We further employ the LCQNN model to handle supervised learning tasks, demonstrating its effectiveness on real datasets. In group action scenarios, we show that by exploiting symmetry and excluding exponentially large irreducible subspaces, the model circumvents barren plateaus. Overall, LCQNN provides a novel framework for focusing quantum resources into architectures that are practically trainable yet expressive enough to tackle challenging machine learning applications.

quant-ph

Sample-Efficient Estimation of Nonlinear Quantum State Functions

Efficient estimation of nonlinear functions of quantum states is crucial for various key tasks in quantum computing, such as entanglement spectroscopy, fidelity estimation, and feature analysis of quantum data. Conventional methods using state tomography and estimating numerous terms of the series expansion are computationally expensive, while alternative approaches based on a purified query oracle impose practical constraints. In this paper, we introduce the quantum state function (QSF) framework by extending the SWAP test via linear combination of unitaries and parameterized quantum circuits. Our framework enables the implementation of arbitrarily normalized degree-$n$ polynomial functions of quantum states with precision $\varepsilon$ using $\mathcal{O}(n/\varepsilon^2)$ copies. We further apply QSF for developing quantum algorithms for fundamental tasks, including entropy, fidelity, and eigenvalue estimations. Specifically, for estimating von Neumann entropy, quantum relative entropy, and quantum state fidelity, where $κ$ and $γ$ represent the minimal nonzero eigenvalue and normalized factor, respectively, we achieve a sample complexity of $\tilde{\mathcal{O}}(γ^2/(\varepsilon^2κ))$. Our work establishes a concise and unified paradigm for estimating and realizing nonlinear functions of quantum states, paving the way for the practical processing and analysis of quantum data.

quant-ph

Optimizer-Dependent Generalization Bound for Quantum Neural Networks

Quantum neural networks (QNNs) play a pivotal role in addressing complex tasks within quantum machine learning, analogous to classical neural networks in deep learning. Ensuring consistent performance across diverse datasets is crucial for understanding and optimizing QNNs in both classical and quantum machine learning tasks, but remains a challenge as QNN's generalization properties have not been fully explored. In this paper, we investigate the generalization properties of QNNs through the lens of learning algorithm stability, circumventing the need to explore the entire hypothesis space and providing insights into how classical optimizers influence QNN performance. By establishing a connection between QNNs and quantum combs, we examine the general behaviors of QNN models from a quantum information theory perspective. Leveraging the uniform stability of the stochastic gradient descent algorithm, we propose a generalization error bound determined by the number of trainable parameters, data uploading times, dataset dimension, and classical optimizer hyperparameters. Numerical experiments validate this comprehensive understanding of QNNs and align with our theoretical conclusions. As the first exploration into understanding the generalization capability of QNNs from a unified perspective of design and training, our work offers practical insights for applying QNNs in quantum machine learning.

quant-ph

Protocols and Trade-Offs of Quantum State Purification

Quantum state purification is crucial in quantum communication and computation, aiming to recover a purified state from multiple copies of an unknown noisy state. This work introduces a general state purification framework designed to achieve the highest fidelity with a specified probability and characterize the associated trade-offs. For i.i.d. quantum states under depolarizing noise, our framework can replicate the purification protocol proposed by [Barenco et al., SIAM Journal on Computing, 26(5), 1997] and further provide exact formulas for the purification fidelity and probability with explicit trade-offs. We prove the protocols' optimality for two copies of noisy states with any dimension and confirm its optimality for higher numbers of copies and dimensions through numerical analysis. Our methodological approach paves the way for proving the protocol's optimality in more general scenarios and leads to optimal protocols for other noise models. Furthermore, we present a systematic implementation method via block encoding and parameterized quantum circuits, providing explicit circuits for purifying three-copy and four-copy states under depolarizing noise. Finally, we estimate the sample complexity and generalize the protocol to a recursive form, demonstrating its practicality for quantum computers with limited memory.

quant-ph

Optimal unilocal virtual quantum broadcasting

Quantum broadcasting is central to quantum information processing and characterizes the correlations within quantum states. Nonetheless, traditional quantum broadcasting encounters inherent limitations dictated by the principles of quantum mechanics. In a previous study, Parzygnat et al. [Phys. Rev. Lett. 132, 110203 (2024)] introduced a canonical broadcasting quantum map that goes beyond the quantum no-broadcasting theorem through a virtual process. In this work, we generalize the concept of virtual broadcasting to unilocal broadcasting by incorporating a reference system and introduce protocols that can be approximated using physical operations with minimal cost. First, we propose a universal unilocal protocol enabling multiple parties to share the correlations of a target bipartite state, which is encoded in the expectation value for any observable. Second, we formalize the simulation cost of a virtual quantum broadcasting protocol into a semidefinite programming problem. Notably, we propose a specific protocol with optimal simulation cost for the 2-broadcasting scenario, revealing an explicit relationship between simulation cost and the quantum system's dimension. Moreover, we establish upper and lower bounds on the simulation cost of the virtual $n$-broadcasting protocol and demonstrate the convergence of the lower bound to the upper bound as the quantum system's dimension increases.

quant-ph