論文の概要: 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)の検証
• 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に関する同様の主張が証明された他のシステムにおける公式な定理証明との比較を行う。

関連論文リスト

• TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability [59.079078796751496]
  我々は,研究レベルの理論計算機科学(TCS)証明生成において,Large Language Models(LLMs)を評価するためのベンチマークであるTCS-Benchを紹介する。 TCS-Benchは、理論計算機科学の会場で発表された論文の定理証明タスクで構成されている。
  論文  参考訳（メタデータ） (2026-08-10T12:36:16Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。 我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。 我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-13T01:33:20Z)
• A Formalization of the Generalized Quantum Stein's Lemma in Lean [0.0]
  我々は、リーン対話的定理証明器において、ハヤシとヤマサキ(2024年)で提示された証明を定式化する。 これは、これまでコンピュータで検証された証明を持つ物理学で最も技術的に要求される定理である。
  論文  参考訳（メタデータ） (2025-10-09T17:41:13Z)
• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。 本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。 我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
  論文  参考訳（メタデータ） (2025-10-01T16:06:40Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
  論文  参考訳（メタデータ） (2025-06-12T10:31:23Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• 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)
• Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs [3.444844635251667]
  確率的振る舞いに関する局所的推論のための新しい量子ホア論理を提案する。 論理学における証明規則は意味論的意味論に関して健全であることを示す。 結果として得られる論理フレームワークは、CoqQLRと呼ばれ、古典量子プログラムに関する半自動推論を容易にする。
  論文  参考訳（メタデータ） (2023-08-09T07:23:22Z)
• 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)

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

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