From the 2 of 13 linked papers with an AI index.
13 papers
Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information
Lei Zhang, Yusheng Zhao, Yimeng Cao +10
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.…
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…
Phase-Stable Hologram Updates for Large-Scale Neutral-Atom Array Reconfiguration
Erdong Huang, Jiayi Huang, Hongshun Yao +2
Assembling large-scale, defect-free Rydberg atom arrays is a key technology for neutral-atom quantum computation. Dynamic holographic optical tweezers enable the assembly and recon…
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…
Programmable Open Quantum Systems
Mingrui Jing, Mengbo Guo, Lin Zhu +2
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…