林海onrush (2023-01-27 01:30):
#paper, Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs,DOI: 10.48550/arXiv.2205.02287,作者引入了纯度表达式的概念,以在量子程序中对纠缠状态进行推理判断。类似于经典内存的指针,并通过执行被称为门的操作来对它们进行评估。由于纠缠的特殊形式存在,导致量子比特的测量结果是相关的现象,而纠缠可以决定算法的正确性和编程模式的适用性。将纯度表达形式化,可以作为自动推理量子程序中纠缠的核心工具,是指其评价不受量子比特的测量结果影响的表达式。本文主要贡献在于提出了Twist,这是第一种具有类型系统的语言,用于对纯度进行合理推理,使开发者能够使用类型注解来识别纯度表达式。最后证明了Twist可以表达量子算法,捕捉其中的编程错误,并支持一些其他语言不允许的程序。同时产生的运行时验证开销小于3.5%。整体而言,是一项基础且有意义的工作。
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
翻译
Abstract:
Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement, the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns. In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation. We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification. We evaluate Twist's type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that several languages disallow, while incurring runtime verification overhead of less than 3.5%.
翻译
回到顶部