利用 AI 与形式化验证降低量子应用开发信任成本

该研究提出一种结合生成式 AI 与形式化验证的量子应用开发方法，用于降低开发者理解和检查生成线路的“信任成本”。方法将目标数学规格、量子线路及证明二者一致性的对应性定理与证明分开，使规格和定理陈述由人检查、证明交由机械化检查，并以随机粒子系统时间演化的实现作为具体示例。基于论文摘要，摘要未说明证明范围、实验规模或验证基准。