論文の概要: QEDIA: Quantum Program Verification in Lean
- arxiv url: http://arxiv.org/abs/2610.17708v1
- Date: Tue, 13 Oct 2026 04:36:21 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-17 17:36:50.423389
- Title: QEDIA: Quantum Program Verification in Lean
- Title（参考訳）: QEDIA: リーンにおける量子プログラム検証
- Abstract要約: 従来の変数を用いた量子証明プログラムを検証するためのフレームワークであるQEDIAをLean 4で紹介する。
その基礎には、全てのレベルにわたって量子ホア論理QHL+を形式化し、部分的および全正当性の両方の論理音を証明するオープンライブラリがある。
本稿では,量子フーリエ変換,位相推定,リピート・アンティル・サクセス回路,ハミルトニアンシミュレーションなどの検証プログラムを用いてQEDIAを解説する。
- 参考スコア（独自算出の注目度）: 19.490519583967387
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present QEDIA, a framework for verifying quantum programs with classical variables in Lean 4. At its foundation is an open library that formalizes the quantum Hoare logic QHL+ across all these levels and proves the logic sound for both partial and total correctness. We construct the library and the program proofs, under human supervision, using an LLM-based prover agent, whose general-purpose core we extend for quantum program verification. We illustrate QEDIA with verified programs including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Hamiltonian simulation.
- Abstract（参考訳）: 量子計算と古典計算をインターリーブする実践的な量子プログラム:古典的なデータが実行された量子演算を形作り、測定結果が続く古典的な計算を形作る。
証明アシスタントにおけるそのようなプログラムの形式的検証には、量子力学の数学からプログラムの構文と意味論、仕様と証明規則まで、あらゆるレベルでこの相互作用を一貫して扱うプログラム論理を機械化する必要がある。
このような機械化は、それらの上に構築されたプログラム証明とともに、通常、かなりの手作業を必要とする。
従来の変数を用いた量子プログラムの検証フレームワークであるQEDIAをLean 4.0で紹介する。
その基礎には、全てのレベルにわたって量子ホア論理QHL+を形式化し、部分的および全正当性の両方の論理音を証明するオープンライブラリがある。
我々は、LLMベースの証明エージェントを用いて、図書館とプログラム証明を構築し、量子プログラム検証のために汎用コアを拡張した。
本稿では,量子フーリエ変換,位相推定,リピート・アンティル・サクセス回路,ハミルトニアンシミュレーションなどの検証プログラムを用いてQEDIAを解説する。
関連論文リスト
- QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
量子コンピューティングは、量子アルゴリズムによる古典的コンピューティングよりも大幅にスピードアップされていることが認識されている。
QCircuitBenchは、量子アルゴリズムの設計と実装におけるAIの能力を評価するために設計された最初のベンチマークデータセットである。
論文 参考訳（メタデータ） (2024-10-10T14:24:30Z) - Parallel Quantum Computing Simulations via Quantum Accelerator Platform Virtualization [44.99833362998488]
本稿では,量子回路実行の並列化モデルを提案する。
このモデルはバックエンドに依存しない機能を利用することができ、任意のターゲットバックエンド上で並列量子回路の実行を可能にする。
論文 参考訳（メタデータ） (2024-06-05T17:16:07Z) - A Case for Synthesis of Recursive Quantum Unitary Programs [9.287571320531457]
量子プログラムは、量子プログラミングに関連する直感的な量子知識のために、コーディングと検証が難しいことで知られている。
本稿では、新しい帰納的量子プログラム言語を含む、最初の量子プログラム合成フレームワークであるQ Synthを紹介する。
Q Synthは量子加算器回路、量子固有値反転回路、量子フーリエ変換を含む10個の量子ユニタリプログラムをうまく合成する。
論文 参考訳（メタデータ） (2023-11-20T03:01:36Z) - Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。
Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。
我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文 参考訳（メタデータ） (2022-11-11T18:50:52Z) - LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。
本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。
アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
論文 参考訳（メタデータ） (2021-10-04T12:20:23Z) - On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
そこで我々は,古典的な3つのハードラーニング問題に対処するために,QAEに基づく効果的な3つの学習プロトコルを考案した。
私たちの研究は、ハード量子物理学と量子情報処理タスクを達成するための高度な量子学習アルゴリズムの開発に新たな光を当てています。
論文 参考訳（メタデータ） (2021-06-29T14:01:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。