論文の概要: Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256
- arxiv url: http://arxiv.org/abs/2607.14082v1
- Date: Wed, 15 Jul 2026 17:56:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-16 16:39:12.855076
- Title: Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256
- Title（参考訳）: リーンにおけるショアのアルゴリズム構築:RSA-2048とP-256における量子攻撃のエージェント形式化
- Abstract要約: Shorのアルゴリズムとその変種は、リーンの形式化を要求されるケースを提示している。
エージェント形式化により、このアルゴリズムファミリーをLeanでフォーマル化する。
結果が、より広範なマシンチェックによる量子暗号解析の道を開くと期待している。
- 参考スコア（独自算出の注目度）: 12.461767160402479
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models are increasingly assisting with demanding formal theorem-proving tasks, particularly when grounded in machine-checked libraries such as Lean. Agentic systems further amplify this process by searching, reusing, and extending existing formal developments to uncover new discoveries. In quantum computing, Shor's algorithm and its variants present such a demanding case for Lean formalization. In this work, we formalize this algorithm family in Lean through agentic formalization: software agents analyze sources, write Lean code and repair proofs, with human review of the scientific claims and machine checking of the resulting formal proofs. Our formalization develops the mathematical foundations for analyzing quantum attacks in two cryptographic settings: a 2048-bit modulus in the RSA-2048 and the standardized elliptic curve over a 256-bit prime field (P-256). To support these analyses, the formalization ranges from quantum algorithms for order finding to reversible quantum circuits for modular and elliptic-curve arithmetic. Based on [Quantum 5, 433] and [ASIACRYPT 2017, 241--270], we formalize the logical resource estimates for RSA-2048 and P-256, respectively, and provide additional estimates of classical operations. We expect the results pave the way for broader machine-checked quantum cryptanalysis and represent a step toward AI-assisted design and verification of quantum algorithms.
- Abstract（参考訳）: 大規模な言語モデルは、特にリーンのようなマシンチェックされたライブラリに基礎を置いているとき、フォーマルな定理を証明するタスクを要求するのをますます助けています。
エージェントシステムは、新しい発見を明らかにするために、既存の公式な開発を探索、再利用、拡張することで、このプロセスをさらに増幅する。
量子コンピューティングにおいて、ショアのアルゴリズムとその変種はリーン形式化の要求されたケースを示す。
ソフトウェアエージェントはソースを分析し、リーンコードを書き、証明を修復し、科学的クレームの人間によるレビューと結果の形式的証明のマシンチェックを行います。
我々の定式化は、RSA-2048における2048ビットの弾性率と256ビットの素体(P-256)上の標準楕円曲線の2つの暗号設定で量子攻撃を解析するための数学的基盤を開発する。
これらの解析をサポートするために、形式化は秩序探索のための量子アルゴリズムからモジュラーおよび楕円曲線演算のための可逆的な量子回路まで様々である。
我々は, [Quantum 5, 433] と [ASIACRYPT 2017. 241--270] に基づいて, RSA-2048 と P-256 の論理的資源推定をそれぞれ定式化し, 古典的演算のさらなる推定を行う。
この結果は、より広範な機械学習による量子暗号解析の道を開くものであり、AIによる量子アルゴリズムの設計と検証への一歩となると期待している。
関連論文リスト
- Verifiable quantum advantage in extremely low depth [52.51019642214249]
浅量子回路では解けない問題を格子ベースの仮定で解くのが困難である。
浅量子回路は、解を効率よく検証できる古典的な難題を解くのに十分な構造を持っていることを証明している。
論文 参考訳（メタデータ） (2026-09-01T15:54:34Z) - GroverGPT: A Large Language Model with 8 Billion Parameters for Quantum Searching [43.496857395654764]
量子チューリングマシンの出力をシミュレートするために,大規模言語モデルを活用する可能性について検討する。
特殊なモデルであるGroverGPTは、15兆以上のトークンでトレーニングされた。
OpenAIのGPT-4o(45%の精度)を一貫して上回り、6ビットと10ビットのデータセットでほぼ100%の精度を達成した。
また、3から6キュービットのデータで訓練すると、20キュービットを超えるシステムに対して95%を超える精度で強い一般化を示した。
論文 参考訳（メタデータ） (2024-12-30T20:23:10Z) - Quantum Sieving for Code-Based Cryptanalysis and Its Limitations for ISD [0.0]
上述したサブルーチンの量子変種を設計することで、コードシービングのための最初の量子アルゴリズムを導入する。
我々の量子ウォークアルゴリズムは、局所性に敏感なフィルタリング層を追加することにより、基礎となる探索問題の構造を利用する。
我々の分析は、このフレームワークが量子IDDアルゴリズムの最先端性を上回るように適応されるべきであることを強調している。
論文 参考訳（メタデータ） (2024-08-29T11:47:33Z) - Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [62.46800898243033]
量子学習理論の最近の進歩は、様々な古典的な入力によって生成された測定データから、大きな量子ビット回路の線形特性を効率的に学習できるのか?
我々は、小さな予測誤差を達成するためには、$d$で線形にスケーリングするサンプルの複雑さが必要であることを証明し、それに対応する計算複雑性は、dで指数関数的にスケールする可能性がある。
そこで本研究では,古典的影と三角展開を利用したカーネルベースの手法を提案し,予測精度と計算オーバーヘッドとのトレードオフを制御可能とした。
論文 参考訳（メタデータ） (2024-08-22T08:21:28Z) - Quantum Subroutine for Variance Estimation: Algorithmic Design and Applications [80.04533958880862]
量子コンピューティングは、アルゴリズムを設計する新しい方法の基礎となる。
どの場の量子スピードアップが達成できるかという新たな課題が生じる。
量子サブルーチンの設計は、従来のサブルーチンよりも効率的で、新しい強力な量子アルゴリズムに固い柱を向ける。
論文 参考訳（メタデータ） (2024-02-26T09:32:07Z) - Generalized quantum Arimoto-Blahut algorithm and its application to
quantum information bottleneck [55.22418739014892]
量子アリーモト・ブラフトアルゴリズムをRamakrishnanらにより一般化する。
3つの量子系を持つ量子情報ボトルネックに対して,我々のアルゴリズムを適用した。
数値解析により,我々のアルゴリズムはアルゴリズムよりも優れていることが示された。
論文 参考訳（メタデータ） (2023-11-19T00:06:11Z) - A comment on "Factoring integers with sublinear resources on a
superconducting quantum processor" [0.0]
そこで我々はSchnorr's lattice-based integer factorizationアルゴリズムのオープンソース実装について述べる。
我々の実装は、シュノーラーの整数を70ビットまでしか持たないハイブリッド量子+古典版に対する主張された部分線型格子次元が示している。
我々は、我々の実装が、他のハイブリッド量子/古典的整数分解アルゴリズムのアイデアをテストするための、コミュニティの場として機能することを願っている。
論文 参考訳（メタデータ） (2023-07-18T21:46:54Z) - Pitfalls of the sublinear QAOA-based factorization algorithm [0.8987776881291144]
主要な分解問題は、広くデプロイされた公開鍵暗号ツールの中心にある。
Shorの量子分解アルゴリズムの実装には、数の大きさと線形にスケールする重要なリソースが必要である。
Yanらによる最近の提案は、部分線型量子資源による分解問題を解く可能性を主張している。
論文 参考訳（メタデータ） (2023-03-08T15:23:50Z) - End-to-end resource analysis for quantum interior point methods and portfolio optimization [63.4863637315163]
問題入力から問題出力までの完全な量子回路レベルのアルゴリズム記述を提供する。
アルゴリズムの実行に必要な論理量子ビットの数と非クリフォードTゲートの量/深さを報告する。
論文 参考訳（メタデータ） (2022-11-22T18:54:48Z) - Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。
Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。
我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文 参考訳（メタデータ） (2022-11-11T18:50:52Z) - Classical variational simulation of the Quantum Approximate Optimization
Algorithm [0.0]
パラメタライズドゲートからなる層状量子回路をシミュレートする手法を提案する。
マルチキュービット波動関数のニューラルネットワークパラメトリゼーションを用いる。
シミュレーションした最大の回路では、4QAOA層で54量子ビットに達する。
論文 参考訳（メタデータ） (2020-09-03T15:55:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。