2026-03-05
邓东灵、李婷婷团队提出了一种在形式化正确性约束下进行成本优化的统一框架。该方法引入轻量级中间表示 QCore，并定义关系型操作语义，使全态等价、测量分布保持、部分迹一致与近似正确性等不同层次的正确性契约，能够在同一语义体系中统一表达、组合与验证。基于此，优化过程被建模为满足用户指定关系契约 ( Φ , Ψ ) 的约束综合问题，并引入可调的多目标成本模型，联合度量门数、线路深度及纠错相关开销，以指导优化搜索。
本论文共同通讯作者为研究院高级研究员李婷婷。
图. RelOpt 架构与组件交互关系
论文信息：
Relational Verification for Cost-Aware Quantum Program Optimization, Ziming Zhao, Tingting Li†, Zhaoxuan Li, Jianwei Yin†，AAAI 2026.
