arXiv subjects

Jingu Xie

Publications and source records attributed to Jingu Xie.

4 recordsLinked to original sources

arXiv2026

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↗

arXiv2025

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↗

arXiv2025

Structure, Optimality, and Symmetry in Shadow Unitary Inversion

Reversing unitary operations is a key task in quantum computing and quantum control. In this work, we introduce and develop the framework of shadow unitary inversion, a relaxed variant of unitary inversion in which the goal is to reproduce the action of the inverse unitary only at the level of the expectation value of a fixed observable. This task captures an operational setting in which only shadow information is required and allows query complexities significantly below those of full unitary inversion. We establish a dimension-dependent lower bound showing that any $t$-query scheme requires $t$ to scale at least linearly with the system dimension, with the constant determined by the spectral properties of the target observable. In the qubit case, we construct a deterministic three-query sequential protocol that achieves exact shadow inversion, and we provide a complete characterization of all admissible qubit channels satisfying the shadow constraint. Numerical evidence suggests that three queries are optimal. For higher-dimensional systems, we develop a semidefinite-programming formulation for optimizing shadow-inversion combs and introduce a representation-theoretic symmetry reduction that decomposes the problem into invariant blocks, substantially reducing the problem size. These results provide the first systematic study for shadow unitary inversion and establish its resource requirements and symmetry structure across dimensions.

quant-ph↗

arXiv2025

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↗