5 papers
Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
Austin Shen, Yunong Shi
Automated theorem proving systems built on Lean 4 increasingly rely on parallel tactic search over partially specified proofs, such as those generated by Draft-Sketch-Prove (DSP) p…
ConiQ: Enabling Concatenated Quantum Error Correction on Neutral Atom Arrays
Pengyu Liu, Mingkuan Xu, Hengyun Zhou +3
Recent progress on concatenated codes, especially many-hypercube codes, achieves unprecedented space efficiency. Yet two critical challenges persist in practice. First, these codes…
CaliScalpel: In-Situ and Fine-Grained Qubit Calibration Integrated with Surface Code Quantum Error Correction
Xiang Fang, Keyi Yin, Yuchen Zhu +8
Quantum Error Correction (QEC) is a cornerstone of fault-tolerant, large-scale quantum computing. However, qubit error drift significantly degrades QEC performance over time, neces…
QECC-Synth: A Layout Synthesizer for Quantum Error Correction Codes on Sparse Hardware Architectures
Keyi Yin, Hezi Zhang, Xiang Fang +4
Quantum Error Correction (QEC) codes are essential for achieving fault-tolerant quantum computing (FTQC). However, their implementation faces significant challenges due to disparit…
AlphaRouter: Quantum Circuit Routing with Reinforcement Learning and Tree Search
Wei Tang, Yiheng Duan, Yaroslav Kharkov +3
Quantum computers have the potential to outperform classical computers in important tasks such as optimization and number factoring. They are characterized by limited connectivity,…