論文の概要: Verifying Quantum Phase Estimation (QPE) using Prove-It
- arxiv url: http://arxiv.org/abs/2304.02183v1
- Date: Wed, 5 Apr 2023 01:21:00 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-06 13:47:50.862789
- Title: Verifying Quantum Phase Estimation (QPE) using Prove-It
- Title（参考訳）: Prove-It を用いた量子位相推定(QPE)の検証
- Authors: Wayne M. Witzel (1), Warren D. Craft (1 and 2), Robert Carr (2),
Deepak Kapur (2) ((1) Center for Computing Research, Quantum Computer
Science, Sandia National Laboratories, Albuquerque, NM, (2) Department of
Computer Science, The University of New Mexico, Albuquerque, NM)
- Abstract要約: Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムを検証するために使用された。
Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The general-purpose interactive theorem-proving assistant called Prove-It was
used to verify the Quantum Phase Estimation (QPE) algorithm, specifically
claims about its outcome probabilities. Prove-It is unique in its ability to
express sophisticated mathematical statements, including statements about
quantum circuits, integrated firmly within its formal theorem-proving
framework. We demonstrate our ability to follow a textbook proof to produce a
formally certified proof, highlighting useful automation features to fill in
obvious steps and make formal proving nearly as straightforward as informal
theorem proving. Finally, we make comparisons with formal theorem-proving in
other systems where similar claims about QPE have been proven.
- Abstract（参考訳）: Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムの検証に使用された。
Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有であり、公式な定理証明フレームワークにしっかりと組み込まれている。
我々は、教科書の証明に従って、正式に証明された証明を作成する能力を示し、明らかなステップを埋め、形式的な証明を非公式な定理証明とほぼ同等に簡単にする有用な自動化機能を強調する。
最後に、QPEに関する同様の主張が証明された他のシステムにおける公式な定理証明との比較を行う。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳（メタデータ） (2023-03-08T22:00:15Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - ProoFVer: Natural Logic Theorem Proving for Fact Verification [24.61301908217728]
本稿では,自然論理を用いた事実検証システムProoFVerを提案する。
証明の生成により、ProoFVerは説明可能なシステムになる。
証明により,人間がProoFVerの判断を正しくシミュレートできることが判明した。
論文 参考訳（メタデータ） (2021-08-25T17:23:04Z) - Depth-efficient proofs of quantumness [77.34726150561087]
量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。
本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
論文 参考訳（メタデータ） (2021-07-05T17:45:41Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳（メタデータ） (2020-12-20T18:15:12Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z) - Using Quantum Metrological Bounds in Quantum Error Correction: A Simple
Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。
我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
論文 参考訳（メタデータ） (2020-04-24T17:58:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。