論文の概要: Quantum automated theorem proving
- arxiv url: http://arxiv.org/abs/2601.07953v1
- Date: Mon, 12 Jan 2026 19:39:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-14 18:27:18.918551
- Title: Quantum automated theorem proving
- Title(参考訳): 量子自動定理証明
- Authors: Zheng-Zhi Sun, Qi Ye, Dong-Ling Deng,
- Abstract要約: 本稿では,量子自動定理証明のための一般的なフレームワークを提案する。
知識基盤の量子表現を導入し、様々なタスクに対する対応する推論アルゴリズムを提案する。
本稿では,命題論理と一階論理の両方において,量子解法を用いて自動推論を実現する方法を示す。
- 参考スコア(独自算出の注目度): 15.134110328567838
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of applications and the quest for enhanced theorem-proving capabilities remains a prominent pursuit in artificial intelligence. Here, we propose a generic framework for quantum automated theorem proving, where the intrinsic quantum superposition and entanglement features would lead to potential advantages. In particular, we introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks. We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic with quadratically reduced query complexity. In addition, we propose the quantum algebraic proving method for geometric theorems, extending Wu's algebraic approach beyond the classical setting. Through concrete examples, including geometry problems from the International Mathematical Olympiad, we demonstrate how a quantum computer may prove geometric theorems with quadratic better query complexity. Our results establish a primary approach towards building quantum automatic theorem provers, which would be crucial for practical applications of both near-term and future quantum technologies.
- Abstract(参考訳): 自動定理証明(英: Automated theorem proving、またはより広く自動化された推論)は、コンピュータプログラムを使用して数学的定理や論理的ステートメントを自動証明または証明することを目的としている。
膨大なアプリケーションにまたがって重要な役割を担い、拡張された定理証明能力の追求は、人工知能において依然として顕著な追求である。
本稿では,量子自動定理証明のための一般的な枠組みを提案し,本質的な量子重ね合わせと絡み合いが潜在的な利点をもたらす。
特に、知識基盤の量子表現を導入し、様々なタスクに対する対応する推論アルゴリズムを提案する。
命題論理と一階論理の両方において、クエリの複雑さを2次に減らした量子解法によって、自動推論がいかに達成できるかを示す。
さらに、Wuの代数的アプローチを古典的な設定を超えて拡張する、幾何学的定理の量子代数的証明法を提案する。
国際数理オリンピアードの幾何問題を含む具体的な例を通して、量子コンピュータが2次的により良いクエリ複雑性を持つ幾何定理をいかに証明できるかを実証する。
この結果から, 近い将来の量子技術の実用化に欠かせない量子自動定理プローサ構築への主要なアプローチが確立された。
関連論文リスト
- Artificial intelligence for representing and characterizing quantum systems [49.29080693498154]
大規模量子システムの効率的なキャラクタリゼーションは、量子科学における中心的な課題である。
人工知能(AI)の最近の進歩は、この課題に対処するための強力なツールとして現れている。
本稿では、これらのAIパラダイムが量子システム評価における2つのコアタスクにどのように貢献するかを論じる。
論文 参考訳(メタデータ) (2025-09-05T08:41:24Z) - A mathematical model for a universal digital quantum computer with an application to the Grover-Rudolph algorithm [0.0]
代数的確率論を用いた普遍デジタル量子計算のための新しいフレームワークを開発する。
量子回路を基本量子ゲートの有限列として定義する。
与えられた確率密度関数を近似する量子回路を設計する。
論文 参考訳(メタデータ) (2025-03-17T17:18:45Z) - QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
量子コンピューティングは、量子アルゴリズムによる古典的コンピューティングよりも大幅にスピードアップされていることが認識されている。
QCircuitBenchは、量子アルゴリズムの設計と実装におけるAIの能力を評価するために設計された最初のベンチマークデータセットである。
論文 参考訳(メタデータ) (2024-10-10T14:24:30Z) - Quantum algorithms: A survey of applications and end-to-end complexities [88.57261102552016]
期待されている量子コンピュータの応用は、科学と産業にまたがる。
本稿では,量子アルゴリズムの応用分野について検討する。
私たちは、各領域における課題と機会を"エンドツーエンド"な方法で概説します。
論文 参考訳(メタデータ) (2023-10-04T17:53:55Z) - No-signalling constrains quantum computation with indefinite causal
structure [45.279573215172285]
我々は、不定因果構造を持つ量子計算の定式化を開発する。
我々は高階量子マップの計算構造を特徴付ける。
計算的および情報理論的な性質を持つこれらの規則は、量子システム間のシグナル伝達関係のより物理的概念によって決定される。
論文 参考訳(メタデータ) (2022-02-21T13:43:50Z) - Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene
Algebra [11.078562853984211]
クリーネ代数に基づく古典的プログラム解析の成功に触発された量子プログラムの推論について検討する。
等等法則や古典的テストの優れた性質を含むKATの重要な特徴は、量子プログラムの文脈において保持されない。
本論文は,NKAの完全・音声意味モデルを特定するための自然な代替案として,NKA(Non-idempotent Kleene Algebra)を提案する。
論文 参考訳(メタデータ) (2021-10-13T20:27:01Z) - Depth-efficient proofs of quantumness [77.34726150561087]
量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。
本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
論文 参考訳(メタデータ) (2021-07-05T17:45:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。