論文の概要: Towards Classical Software Verification using Quantum Computers

• arxiv url: http://arxiv.org/abs/2404.18502v2
• Date: Mon, 24 Mar 2025 12:23:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-25 14:31:04.859996
• Title: Towards Classical Software Verification using Quantum Computers
• Title（参考訳）: 量子コンピュータを用いた古典的ソフトウェア検証に向けて
• Authors: Sebastian Issel, Kilian Tscharke, Pascal Debus,
• Abstract要約: 量子コンピュータを用いた古典的プログラムの形式的検証を高速化する可能性を探る。 アウトオブバウンドやオーバーフローのような一般的なエラーの最小例は、異なるソルバでテストされ、量子デバイスで試される。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: We explore the possibility of accelerating the formal verification of classical programs with a quantum computer. A common source of security flaws stems from the existence of common programming errors like use after free, null-pointer dereference, or division by zero. To aid in the discovery of such errors, we try to verify that no such flaws exist. In our approach, for some code snippet and undesired behaviour, a SAT instance is generated, which is satisfiable precisely if the behavior is present in the code. It is in turn converted to an optimization problem, that is solved on a quantum computer. This approach holds the potential of an asymptotically polynomial speedup. Minimal examples of common errors, like out-of-bounds and overflows, but also synthetic instances with special properties, specific number of solutions, or structure, are tested with different solvers and tried on a quantum device. We use the near-standard Quantum Approximation Optimisation Algorithm, an application of the Grover algorithm, and the Quantum Singular Value Transformation to find the optimal solution, and with it a satisfying assignment.
• Abstract（参考訳）: 量子コンピュータを用いた古典的プログラムの形式的検証を高速化する可能性を探る。 セキュリティ欠陥の共通の原因は、フリー、ヌルポインタの参照、ゼロの除算といった、一般的なプログラミングエラーの存在にある。 このような誤りの発見を支援するため、そのような欠陥が存在しないことを検証しようと試みる。 このアプローチでは、コードスニペットや望ましくない振る舞いに対して、SATインスタンスが生成される。 量子コンピュータで解く最適化問題に変換される。 このアプローチは漸近的に多項式のスピードアップの可能性を秘めている。 アウト・オブ・バウンドやオーバーフローのような一般的なエラーの最小例だけでなく、特別な性質、特定の数の解や構造を持つ合成インスタンスも、異なる解法を用いてテストされ、量子デバイス上で試される。 我々は,準標準量子近似最適化アルゴリズム,Groverアルゴリズムの適用,および量子特異値変換を用いて最適解を求める。

関連論文リスト

• Quantum algorithms: A survey of applications and end-to-end complexities [90.05272647148196]
  期待されている量子コンピュータの応用は、科学と産業にまたがる。 本稿では,量子アルゴリズムの応用分野について検討する。 私たちは、各領域における課題と機会を"エンドツーエンド"な方法で概説します。
  論文  参考訳（メタデータ） (2023-10-04T17:53:55Z)
• Enhancing Quantum Algorithms for Quadratic Unconstrained Binary Optimization via Integer Programming [0.0]
  本研究では,最適化のための量子および古典的手法の可能性を統合する。 線形緩和により問題のサイズを小さくし、最小サイズの量子マシンで問題を処理できるようにした。 実量子ハードウェアの計算結果を多数提示する。
  論文  参考訳（メタデータ） (2023-02-10T20:12:53Z)
• Deep Quantum Error Correction [73.54643419792453]
  量子誤り訂正符号(QECC)は、量子コンピューティングのポテンシャルを実現するための鍵となる要素である。 本研究では,新しいエンペンド・ツー・エンドの量子誤りデコーダを効率的に訓練する。 提案手法は,最先端の精度を実現することにより,QECCのニューラルデコーダのパワーを実証する。
  論文  参考訳（メタデータ） (2023-01-27T08:16:26Z)
• Quantum Worst-Case to Average-Case Reductions for All Linear Problems [66.65497337069792]
  量子アルゴリズムにおける最悪のケースと平均ケースの削減を設計する問題について検討する。 量子アルゴリズムの明示的で効率的な変換は、入力のごく一部でのみ正し、全ての入力で正しくなる。
  論文  参考訳（メタデータ） (2022-12-06T22:01:49Z)
• A Quantum Algorithm for Computing All Diagnoses of a Switching Circuit [73.70667578066775]
  ほとんどの人造システム、特にコンピュータは決定論的に機能する。 本稿では、量子物理学が確率法則に従うときの直観的なアプローチである量子情報理論による接続を提供する。
  論文  参考訳（メタデータ） (2022-09-08T17:55:30Z)
• Quantum Speedup for Higher-Order Unconstrained Binary Optimization and MIMO Maximum Likelihood Detection [2.5272389610447856]
  実数値の高次非制約二項最適化問題をサポートする量子アルゴリズムを提案する。 提案アルゴリズムは,古典的領域におけるクエリの複雑さを低減し,量子領域における2次高速化を実現する。
  論文  参考訳（メタデータ） (2022-05-31T00:14:49Z)
• Adiabatic Quantum Computing for Multi Object Tracking [170.8716555363907]
  マルチオブジェクト追跡(MOT)は、オブジェクト検出が時間を通して関連付けられているトラッキング・バイ・検出のパラダイムにおいて、最もよくアプローチされる。 これらの最適化問題はNPハードであるため、現在のハードウェア上の小さなインスタンスに対してのみ正確に解決できる。 本手法は,既成整数計画法を用いても,最先端の最適化手法と競合することを示す。
  論文  参考訳（メタデータ） (2022-02-17T18:59:20Z)
• A Hybrid Quantum-Classical Algorithm for Robust Fitting [47.42391857319388]
  本稿では,ロバストフィッティングのためのハイブリッド量子古典アルゴリズムを提案する。 私たちのコアコントリビューションは、整数プログラムの列を解く、新しい堅牢な適合式である。 実際の量子コンピュータを用いて得られた結果について述べる。
  論文  参考訳（メタデータ） (2022-01-25T05:59:24Z)
• Compilation of Fault-Tolerant Quantum Heuristics for Combinatorial Optimization [0.14755786263360526]
  最小限のフォールトトレラント量子コンピュータで試すのに、最適化のための量子アルゴリズムが最も実用的であるかを探る。 この結果から,2次高速化のみを実現する量子最適化が,古典的アルゴリズムよりも有利であるという考えが否定される。
  論文  参考訳（メタデータ） (2020-07-14T22:54:04Z)

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

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