論文の概要: Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp
- arxiv url: http://arxiv.org/abs/2605.01008v1
- Date: Fri, 01 May 2026 18:21:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-05 20:33:49.537526
- Title: Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp
- Title(参考訳): QrispにおけるECCDLPのための実装ショアOracleのセマンティックスによる検証
- Authors: Lei Zhang, Zhiyuan Chen,
- Abstract要約: 本稿では,Qrisp上に構築されたエンドツーエンドでコンパイル可能なCDLP実装に対して,セマンティクス第一の検証視点を提案する。
プログラムセマンティクスのレベルで実装されたオラクルを指定し、そのキーコンポーネントに対する洗練スタイルの検証義務を導出し、結果として生じるオラクルファミリーに対して高い複雑性の議論を提供する。
- 参考スコア(独自算出の注目度): 9.455788055292418
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Shor-style quantum algorithms for the elliptic-curve discrete logarithm problem (ECDLP) are highly sensitive to the exact semantics of their group-operation oracles. Consequently, minor implementation choices can invalidate the intended mathematical model and lead to misleading conclusions. This paper introduces a semantics-first verification perspective for an end-to-end, compilable ECDLP implementation built on Qrisp. We specify the implemented oracle at the level of program semantics, derive refinement-style verification obligations for its key components, and provide a high-level complexity argument for the resulting oracle family. A small case study highlights that (i) the core point-update primitive agrees with a classical reference on well-formed inputs, yet (ii) controlled execution may violate the expected control law under the evaluated toolchain, despite a passing trivial control sanity check. These results position semantic auditing as a practical prerequisite for trustworthy ECDLP-oriented quantum software.
- Abstract(参考訳): 楕円曲線離散対数問題(ECDLP)に対するショアスタイルの量子アルゴリズムは、それらの群演算オラクルの正確な意味に非常に敏感である。
結果として、小さな実装の選択は意図した数学的モデルを無効にし、誤った結論を導き出すことができる。
本稿では,Qrisp上に構築されたエンドツーエンドでコンパイル可能なCDLP実装に対して,セマンティクス第一の検証視点を提案する。
プログラムセマンティクスのレベルで実装されたオラクルを指定し、その鍵となるコンポーネントに対する洗練スタイルの検証義務を導出し、結果として生じるオラクルファミリーに対して高い複雑性の議論を提供する。
小さなケーススタディはそれを強調します
(i)中核点更新プリミティブは、十分に整形された入力に関する古典的な参照と一致するが、
二 管理執行は、自明な管理衛生検査を経たにもかかわらず、評価ツールチェーンの下で期待される制御法に違反しうる。
これらの結果から, セマンティック監査は, 信頼性の高いCDLP指向量子ソフトウェアのための現実的な前提条件として位置づけられた。
関連論文リスト
- Breaking the Computational Barrier: Provably Efficient Actor-Critic for Low-Rank MDPs [53.412166189410904]
低ランクマルコフ決定過程(MDPs)の下で広く採用されているRLオーラクルの階層を確立するために,教師付き学習を計算プロキシとして利用する。
本研究の目的は,政策評価にのみ依存する新しい楽観的アクター批判アルゴリズムを提案することである。
提案アルゴリズムは,従来の計算コストの高い計画や最適化オーラクルを回避しつつ,既存のサンプル複雑度保証よりも優れていることを示す。
論文 参考訳(メタデータ) (2026-05-02T04:46:54Z) - SPPO: Sequence-Level PPO for Long-Horizon Reasoning Tasks [41.49967840381499]
Sequence-Level PPO (SPPO) は、PPOのサンプルテキスト効率と結果ベースの更新の安定性を調和させるスケーラブルなアルゴリズムである。
SPPOは標準のPPOをはるかに上回り、計算量の多いグループベースの手法の性能に匹敵する。
論文 参考訳(メタデータ) (2026-04-10T01:58:21Z) - Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
SOTA LLMが形式言語の構造的・階層的複雑性を把握できるかどうかは不明である。
ChomskyBench はchomsky Hierarchy のレンズを通して LLM を体系的に評価するためのベンチマークである。
ChomskyBenchは、各レベルで機能をテストするように設計された、言語認識と生成タスクの包括的なスイートで構成されている。
論文 参考訳(メタデータ) (2026-04-03T04:06:39Z) - TableMind++: An Uncertainty-Aware Programmatic Agent for Tool-Augmented Table Reasoning [44.20336483508951]
テーブル推論は、意味的理解と正確な数値操作を共同で行うモデルを必要とする。
これらの制約に対処するため、我々は以前TableMindをチューニングベースの自律型プログラムエージェントとして提案した。
この基盤をTableMind++に拡張し、新しい不確実性を認識した推論フレームワークを導入しました。
論文 参考訳(メタデータ) (2026-03-08T08:31:33Z) - CoT-Seg: Rethinking Segmentation with Chain-of-Thought Reasoning and Self-Correction [50.67483317563736]
本稿では,段階的に考察し,必要な情報を検索し,結果を生成し,自己評価を行い,結果を洗練するシステムを提案する。
CoT-Segは、思考の連鎖推論と自己補正を組み合わせることで、推論セグメンテーションを再考する、トレーニング不要のフレームワークである。
論文 参考訳(メタデータ) (2026-01-24T11:41:54Z) - A Posteriori Certification Framework for Generalized Quantum Arimoto-Blahut Algorithms [41.15017547767954]
本稿では,一般化量子Arimoto-Blahut (QAB) アルゴリズムに対する後続認証の視点を紹介する。
我々は、凸性とかなり弱い数値検証条件の下で、QAB反復が大域最小化器に収束することを示す大域収束定理を証明した。
応用として、チャネルの量子相対エントロピーを計算するための認定反復スキームを開発する。
論文 参考訳(メタデータ) (2026-01-14T09:10:41Z) - Continual Quantum Architecture Search with Tensor-Train Encoding: Theory and Applications to Signal Processing [68.35481158940401]
CL-QASは連続的な量子アーキテクチャ検索フレームワークである。
振幅のエンコードと変分量子回路の忘れを犠牲にすることの課題を緩和する。
制御可能なロバスト性表現性、サンプル効率の一般化、およびバレンプラトーを使わずに滑らかな収束を実現する。
論文 参考訳(メタデータ) (2026-01-10T02:36:03Z) - Principled RL for Diffusion LLMs Emerges from a Sequence-Level Perspective [85.06838178922791]
強化学習(RL)は自己回帰言語モデルに非常に効果的であることが証明されている。
しかし、これらの手法を拡散大言語モデル(dLLM)に適応させることは、根本的な課題を提起する。
本稿では,全シーケンス生成を単一アクションとして扱い,ELBOを抽出可能なシークエンスレベル確率プロキシとして利用する,原則的RLフレームワークを提案する。
論文 参考訳(メタデータ) (2025-12-03T13:05:32Z) - Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
プログラム解析のトレンドは、入力プログラムの言語内で検証条件を符号化することである。
Inductive Predicate Synthesis Modulo Programs (IPS-MP) を提案する。
論文 参考訳(メタデータ) (2024-07-11T12:51:08Z) - An Information Bottleneck Approach for Controlling Conciseness in
Rationale Extraction [84.49035467829819]
我々は,情報ボトルネック(IB)の目的を最適化することで,このトレードオフをよりよく管理できることを示す。
我々の完全教師なしのアプローチは、文上のスパース二項マスクを予測する説明器と、抽出された合理性のみを考慮したエンドタスク予測器を共同で学習する。
論文 参考訳(メタデータ) (2020-05-01T23:26:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。