論文の概要: VyZX: Formal Verification of a Graphical Quantum Language
- arxiv url: http://arxiv.org/abs/2311.11571v2
- Date: Mon, 15 Jul 2024 17:10:09 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-17 02:54:11.562211
- Title: VyZX: Formal Verification of a Graphical Quantum Language
- Title（参考訳）: VyZX: グラフィカル量子言語の形式的検証
- Authors: Adrian Lehmann, Ben Caldwell, Bhakti Shah, Robert Rand,
- Abstract要約: 帰納的表現は形式的推論の意味論を定義する。
VyZXは、帰納的に定義されたグラフィカル言語を推論するためのライブラリである。
VyZX における帰納グラフは、ZX-計算の書き直し規則の正しさを証明するためにどのように用いられるかを示す。
- 参考スコア（独自算出の注目度）: 0.17476232824732776
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define semantics for formal reasoning. This highlights a gap where algorithm design and proof assistants require a fundamentally different structure of graphs, particularly for process theories which represent programs using graphs. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category theory definitions. A key goal for VyZX is to Verify the ZX-calculus, a graphical language for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph's semantic interpretation. We show how inductive graphs in VyZX are used to prove the correctness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. VyZX integrates easily with the proof engineer's workflow through visualization and automation.
- Abstract（参考訳）: グラフの数学的表現は、しばしば隣接行列やリストに似ており、ホワイトボードの推論やアルゴリズムの設計を促進する表現である。
証明アシスタントの領域では、帰納的表現は形式的推論の意味論を効果的に定義する。
これは、特にグラフを用いたプログラムを表現するプロセス理論において、アルゴリズム設計と証明アシスタントが根本的に異なるグラフ構造を必要とするギャップを浮き彫りにする。
このギャップに対処するため、帰納的に定義されたグラフィカル言語を推論するための検証済みライブラリであるVyZXを提案する。
これらの帰納的構成は、圏論の定義から自然に生じる。
VyZXの重要な目標は、量子計算を推論するグラフィカル言語であるZX-calculusを検証することである。
ZX-計算は、グラフの意味的解釈を保存するダイアグラム的な書き直し規則の集合を伴っている。
本稿では、VyZXにおける帰納グラフが、ZX-計算の書き換え規則の正しさを証明するためにどのように使われているかを示し、それを標準証明アシスタント技術を用いて実際に適用する。
VyZXは、ビジュアライゼーションと自動化を通じて、証明エンジニアのワークフローと簡単に統合できる。
関連論文リスト
- Logical Entity Representation in Knowledge-Graphs for Differentiable
Rule Learning [71.05093203007357]
本稿では,知識グラフ内のエンティティのコンテキスト情報をエンコードするための論理エンティティ・リプレゼンテーション(LERP)を提案する。
LERPは、エンティティの隣接部分グラフ上の確率論的論理関数のベクトルとして設計されている。
我々のモデルは知識グラフ補完において他のルール学習法よりも優れており、最先端のブラックボックス法に匹敵する、あるいは優れている。
論文 参考訳（メタデータ） (2023-05-22T05:59: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) - GraphQ IR: Unifying Semantic Parsing of Graph Query Language with
Intermediate Representation [91.27083732371453]
本稿では,グラフクエリ言語,すなわちGraphQ IRに対する統合中間表現(IR)を提案する。
セマンティックギャップをブリッジするIRの自然言語のような表現と、グラフ構造を維持するための正式に定義された構文によって、ニューラルネットワークによるセマンティックパーシングは、ユーザクエリをより効果的にGraphQ IRに変換することができる。
我々のアプローチは、KQA Pro、Overnight、MetaQAにおける最先端のパフォーマンスを一貫して達成できます。
論文 参考訳（メタデータ） (2022-05-24T13:59:53Z) - VyZX : A Vision for Verifying the ZX Calculus [0.5735035463793007]
VyZXは、Coq証明アシスタントにおける検証済みのZX計算である。
本稿では,VyZXの基礎となる証明と設計の選択肢とその応用について考察する。
論文 参考訳（メタデータ） (2022-05-11T21:37:23Z) - Addition and Differentiation of ZX-diagrams [0.0]
ZX-ダイアグラムの追加に関する一般帰納的定義を導入する。
ZX-ダイアグラムの誘導的分化を提供する。
また、結果を適用してイジング・ハミルトン多様体の図形を導出する。
論文 参考訳（メタデータ） (2022-02-23T09:52:26Z) - Joint Graph Learning and Matching for Semantic Feature Correspondence [69.71998282148762]
本稿では,グラフマッチングを向上するための信頼度の高いグラフ構造を探索するために,GLAMという共用電子グラフ学習とマッチングネットワークを提案する。
提案手法は,3つの人気ビジュアルマッチングベンチマーク (Pascal VOC, Willow Object, SPair-71k) で評価される。
すべてのベンチマークにおいて、従来の最先端のグラフマッチング手法よりも大きなマージンを達成している。
論文 参考訳（メタデータ） (2021-09-01T08:24:02Z) - ExplaGraphs: An Explanation Graph Generation Task for Structured
Commonsense Reasoning [65.15423587105472]
スタンス予測のための説明グラフ生成の新しい生成および構造化コモンセンスリゾニングタスク(および関連するデータセット)を紹介します。
具体的には、信念と議論が与えられた場合、モデルは、議論が信念を支持しているかどうかを予測し、予測されたスタンスに対する非自明で完全で曖昧な説明として機能する常識強化グラフを生成する必要がある。
グラフの83%は、様々な構造と推論深度を持つ外部のコモンセンスノードを含んでいる。
論文 参考訳（メタデータ） (2021-04-15T17:51:36Z) - Quantum Algorithms and Oracles with the Scalable ZX-calculus [0.0]
スケーラブルなZX計算は、量子アルゴリズムを記述・証明するための形式的で直感的でコンパクトなフレームワークを提供する。
Deutsch-Jozsa、Bernstein-Vazirani、Simon、Groverアルゴリズム。
論文 参考訳（メタデータ） (2021-04-02T13:27:48Z) - Simplification Strategies for the Qutrit ZX-Calculus [0.0]
ZX-calculusは、ZX-diagramと呼ばれるテンソルネットワークを適切に表現するためのグラフィカル言語である。
ZX計算は、量子回路、凝縮物質系、量子アルゴリズム、量子エラー符号、および数え上げ問題に関する推論に応用を見出した。
論文 参考訳（メタデータ） (2021-03-11T19:17:28Z) - On Explainability of Graph Neural Networks via Subgraph Explorations [48.56936527708657]
本稿では,グラフニューラルネットワーク(GNN)を説明するための新しい手法,SubgraphXを提案する。
我々の研究は,GNNのサブグラフを明示的に識別する最初の試みである。
論文 参考訳（メタデータ） (2021-02-09T22:12:26Z) - Hamiltonian systems, Toda lattices, Solitons, Lax Pairs on weighted
Z-graded graphs [62.997667081978825]
グラフ上の解に対して一次元の解を持ち上げることができる条件を特定する。
位相的に興味深いグラフの簡単な例であっても、対応する非自明なラックス対と関連するユニタリ変換は、Z階数グラフ上のラックス対に持ち上げないことを示す。
論文 参考訳（メタデータ） (2020-08-11T17:58:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。