論文の概要: VyZX : A Vision for Verifying the ZX Calculus

• arxiv url: http://arxiv.org/abs/2205.05781v2
• Date: Wed, 18 May 2022 22:28:53 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-13 12:11:53.704366
• Title: VyZX : A Vision for Verifying the ZX Calculus
• Title（参考訳）: VyZX : ZX計算の検証のためのビジョン
• Authors: Adrian Lehmann, Ben Caldwell and Robert Rand
• Abstract要約: VyZXは、Coq証明アシスタントにおける検証済みのZX計算である。 本稿では,VyZXの基礎となる証明と設計の選択肢とその応用について考察する。
• 参考スコア（独自算出の注目度）: 0.5735035463793007
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Optimizing quantum circuits is a key challenge for quantum computing. The PyZX compiler broke new ground by optimizing circuits via the ZX calculus, a powerful graphical alternative to the quantum circuit model. Still, it carries no guarantee of its correctness. To address this, we developed VyZX, a verified ZX-calculus in the Coq proof assistant. VyZX provides two distinct representations of ZX diagrams for ease of programming and proof: A graph-based representation for writing high-level functions on diagrams and a block-based representation for proving ZX diagrams equivalent. Through these two different views, VyZX provides the tools necessary to verify properties and transformations of ZX diagrams. This paper explores the proofs and design choices underlying VyZX and its application and the challenges of verifying a graphical programming language.
• Abstract（参考訳）: 量子回路の最適化は量子コンピューティングの重要な課題である。 PyZXコンパイラは、量子回路モデルの強力なグラフィカルな代替品であるZX計算を通じて回路を最適化することで、新しい基盤を壊した。 しかし、その正しさは保証されていない。 そこで我々は,coq証明アシスタントで検証されたzx計算系vyzxを開発した。 VyZXは、プログラミングと証明の容易性のために、ZXダイアグラムの2つの異なる表現を提供する: ダイアグラムに高階関数を記述するグラフベースの表現と、ZXダイアグラムを同等に証明するためのブロックベースの表現。 これら2つの異なるビューを通じて、VyZXはZXダイアグラムの特性と変換を検証するために必要なツールを提供する。 本稿では、VyZXの基盤となる証明と設計の選択肢とその応用とグラフィカルプログラミング言語の検証の課題について述べる。

関連論文リスト

• Equivalence Classes of Quantum Error-Correcting Codes [49.436750507696225]
  量子過程に影響を与える固有のノイズに対処するために、量子誤り訂正符号(QECC)が必要である。 我々は、テンソルネットワークからなるZXダイアグラムと呼ばれる形式でQECCを表す。
  論文  参考訳（メタデータ） (2024-06-17T20:48:43Z)
• VyZX: Formal Verification of a Graphical Quantum Language [0.17476232824732776]
  帰納的表現は形式的推論の意味論を定義する。 VyZXは、帰納的に定義されたグラフィカル言語を推論するためのライブラリである。 VyZX における帰納グラフは、ZX-計算の書き直し規則の正しさを証明するためにどのように用いられるかを示す。
  論文  参考訳（メタデータ） (2023-11-20T07:12:22Z)
• Simple qudit ZX and ZH calculi, via integrals [0.0]
  ZX計算とZH計算は、量子演算を表すためにダイアグラムを使用し、書き直し規則を用いて、関手意味写像を通して同じ演算子を表すダイアグラム間の変換を行う。 ZX 図と ZH 図のセマンティックマップを記述し、ユニタリ回路の解析に適し、任意の固定次元 D>1 の立方体を 1 つの ZXH-計算として測定する。 本稿では,ZX電卓の安定化器フラグメント'とZH電卓のマルチキャラクタフラグメント'の書き直し規則を実証する。
  論文  参考訳（メタデータ） (2023-04-06T18:00:31Z)
• The Basis of Design Tools for Quantum Computing: Arrays, Decision Diagrams, Tensor Networks, and ZX-Calculus [55.58528469973086]
  量子コンピュータは、古典的コンピュータが決して起こらない重要な問題を効率的に解決することを約束する。 完全に自動化された量子ソフトウェアスタックを開発する必要がある。 この研究は、今日のツールの"内部"の外観を提供し、量子回路のシミュレーション、コンパイル、検証などにおいてこれらの手段がどのように利用されるかを示す。
  論文  参考訳（メタデータ） (2023-01-10T19:00:00Z)
• Compilation of algorithm-specific graph states for quantum circuits [55.90903601048249]
  本稿では,高レベル言語で記述された量子回路から,アルゴリズム固有のグラフ状態を作成する量子回路コンパイラを提案する。 この計算は、このグラフ状態に関する一連の非パウリ測度を用いて実装することができる。
  論文  参考訳（メタデータ） (2022-09-15T14:52:31Z)
• Geometry of Interaction for ZX-Diagrams [0.0]
  ZX-カルキュラス(ZX-Calculus)は、方程式理論を備えた量子計算のための汎用的なグラフィカル言語である。 本稿では,ZX-Calculusのトークンマシンに基づく非同期モデルの提案と混合プロセスへの拡張について述べる。
  論文  参考訳（メタデータ） (2022-06-22T08:52:58Z)
• Circuit Extraction for ZX-diagrams can be #P-hard [0.0]
  ZX-計算のいくつかの応用は、ZX-ダイアグラムを同等の大きさの量子回路に効率的に変換できることに依存している。 本稿では、回路抽出問題は#P-hardであり、量子回路の強いシミュレーションのように、それ自体が困難であることを示す。
  論文  参考訳（メタデータ） (2022-02-18T13:50:24Z)
• Spatial-spectral Hyperspectral Image Classification via Multiple Random Anchor Graphs Ensemble Learning [88.60285937702304]
  本稿では,複数のランダムアンカーグラフアンサンブル学習(RAGE)を用いた空間スペクトルHSI分類手法を提案する。 まず、各選択されたバンドのより記述的な特徴を抽出し、局所的な構造と領域の微妙な変化を保存するローカルバイナリパターンを採用する。 次に,アンカーグラフの構成に適応隣接代入を導入し,計算複雑性を低減した。
  論文  参考訳（メタデータ） (2021-03-25T09:31:41Z)
• Simplification Strategies for the Qutrit ZX-Calculus [0.0]
  ZX-calculusは、ZX-diagramと呼ばれるテンソルネットワークを適切に表現するためのグラフィカル言語である。 ZX計算は、量子回路、凝縮物質系、量子アルゴリズム、量子エラー符号、および数え上げ問題に関する推論に応用を見出した。
  論文  参考訳（メタデータ） (2021-03-11T19:17:28Z)
• Hamiltonian systems, Toda lattices, Solitons, Lax Pairs on weighted Z-graded graphs [62.997667081978825]
  グラフ上の解に対して一次元の解を持ち上げることができる条件を特定する。 位相的に興味深いグラフの簡単な例であっても、対応する非自明なラックス対と関連するユニタリ変換は、Z階数グラフ上のラックス対に持ち上げないことを示す。
  論文  参考訳（メタデータ） (2020-08-11T17:58:13Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUINTIFYは、量子回路の定量的解析のためのオープンソースのフレームワークである。 Google Cirqをベースにしており、Clifford+T回路を念頭に開発されている。 ベンチマークのため、QUINTIFYは量子メモリと量子演算回路を含む。
  論文  参考訳（メタデータ） (2020-07-21T15:36:25Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。