量智信息中心_量科网

在量子信息与计算研究中，符号化方法已被广泛用于对量子态与量子操作的人工规范描述和推理验证。同时，这些方法对于保障量子算法与程序自动化验证工具的可扩展性和效率至关重要。然而，当前仍缺乏关于量子数据与操作符号化规范及推理的形式化理论，这极大限制了自动化验证技术在量子计算中的实际应用。 该研究团队提出了一种名为符号化算子逻辑（𝐒𝐎𝐋）的通用逻辑框架，用于实现量子数据与操作的符号化规范及推理。该框架将经典一阶逻辑语言嵌入到形式化算子语言中，用以描述包括递归定义在内的量子数据与操作规范。这种嵌入方式使得研究人员能够在选定底层经典数据理论（如布尔代数或群论）的前提下推理相关性质，从而充分利用现有面向经典计算开发的自动化验证工具。需要特别强调的是，正是这种将经典一阶逻辑嵌入𝐒𝐎𝐒的设计，才使得符号化方法成为可能。 该工作预期该框架能为量子计算与信息的形式化验证及自动化定理证明提供理论基础，适用于Lean、Coq等证明辅助系统及相关平台。