10 papers
Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256
Lei Zhang, Yusheng Zhao, Hongshun Yao +1
The paper uses AI‑driven agents together with the Lean theorem prover to formally verify Shor's algorithm and its quantum attacks on RSA‑2048 and the P‑256 elliptic curve, providin…
An Agentic Formalization for Certified Quantum Neural Network Design
Mingrui Jing, Lei Zhang, Yusheng Zhao +2
The paper formalizes the theory of quantum neural networks (QNNs) using a machine-checked Lean 4 development, providing exact characterizations of expressivity and trainability and…
A Nonstabilizerness Resource Law for Universal Quantum State Purification
Keming He, Enji Xiong, Xin Wang
Quantum state purification aims to recover higher-fidelity quantum states from multiple noisy copies and is a fundamental primitive for quantum information processing. Magic resour…
Universal Robust Quantum Gates via Doubly Geometric Control
Hai Xu, Tao Chen, Junkai Zeng +5
Geometric quantum computation offers a potential route to fault-tolerant quantum information processing by exploiting the global nature of geometric phases. However, achieving cont…
Block Coordinate Descent for Dynamic Portfolio Optimization on Finite-Precision Coherent Ising Machines
Keming He, Yuehan Zhang, Hongshun Yao +2
Coherent Ising machines (CIMs) have emerged as specialized quantum hardware for large-scale combinatorial optimization. However, for large instances that remain challenging for cla…
Evidential Quantum Vertical Federated Learning
Hao Luo, Zhiyuan Zhai, Qianli Zhou +3
Quantum federated learning (QFL) has recently emerged as a promising paradigm for privacy-preserving collaborative learning, yet most existing studies focus on horizontal federated…