量子科技中心_量科网

哈密顿量模拟是量子计算的核心应用之一，在物理系统建模和复杂优化问题求解方面具有重大潜力。现有的此类模拟编译器通常局限于基于泡利算符的低级表示，这限制了程序可编程性，且无法为整个编译流程提供正确性的形式化保证。该研究团队提出了QBlue——一个用于哈密顿量模拟编译的高级形式化验证框架。该框架基于二次量子化形式体系，通过产生和湮灭算符为量子粒子系统提供了自然且富有表现力的描述方式。为确保安全性和正确性，QBlue内置了能追踪粒子类型并强制保持厄米特结构的类型系统。该框架支持将模拟编译为数字和模拟量子电路，并捕捉从静态约束到动态演化的多层语义。QBlue的所有组件（包括语言设计、类型系统和编译正确性）均在Rocq证明框架中实现了完全机械化验证，使其成为首个实现二次量子化哈密顿量模拟端到端验证的编译器。