論文の概要: Misquoted No More: Securely Extracting F* Programs with IO

• arxiv url: http://arxiv.org/abs/2602.19973v1
• Date: Mon, 23 Feb 2026 15:37:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-24 17:42:02.885344
• Title: Misquoted No More: Securely Extracting F* Programs with IO
• Title（参考訳）: Misquoted No More: IOでF*プログラムを安全に抽出する
• Abstract要約: 効果を表すモナドを使用する浅層埋め込みは、証明指向言語で人気がある。 浅い組込みプログラムが検証されると、しばしばOCamlやCのような主流言語に抽出される。 私たちはこのアイデアに基づいていますが、翻訳バリデーションの使用を最初の抽出ステップに制限します。
• 参考スコア（独自算出の注目度）: 0.3848364262836075
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate, syntactically, that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO to a deeply embedded lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary adversarial contexts. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.
• Abstract（参考訳）: 効果を表すモナドを用いた浅層埋め込みは、形式的検証に便利なため、証明指向言語で人気がある。 浅い組込みプログラムが検証されると、しばしばOCamlやCのような主流言語に抽出され、より大きなコードベースにリンクされる。 抽出プロセスが完全には検証されていないのは、しばしば引用(浅く埋め込まれたプログラムを深く埋め込まれたプログラムに変える)が伴うためであり、引用を検証することが大きな課題である。 代わりに、いくつかの先行研究は、個々の抽出結果を認証するために翻訳バリデーションを使用して正式な正当性を保証する。 このアイデアに基づいて構築するが、翻訳バリデーションの使用をリレーショナルクォーテーションと呼ばれる最初の抽出ステップに制限し、メタプログラムを使用して、与えられた浅層プログラムのタイピング導出を構築する。 このメタプログラミングは、タイピングの派生が元のプログラムの構造に従うため、単純である。 構文的に、入力導出が元のプログラムに有効であることを検証したら、元のプログラムに意味論的に関連があることが保証されたコードを生成する検証された構文生成関数に渡す。 この一般的な考え方を応用してSEIO*を構築する。これは、IOで浅い埋め込みF*プログラムを、正式なセキュアなコンパイル保証を提供しながら、深く埋め込まれたラムダ計算に抽出するフレームワークである。 2つの言語間の論理的関係を用いて、SEIO*がRobost Relational Hyperproperty Preservation (RrHP)を保証しているというF*のマシンチェック証明を考案した。 これは、これまでセキュリティよりも正確性に重点を置いてきた、認証と認証の抽出における最先端以上のものだ。

関連論文リスト

• Guaranteeing Faithful Evidence Extraction in Speculative Retrieval-Augmented Generation [1.002229589104305]
  本稿では、投機的RAGのための新しい忠実度第一パラダイムである制約付きハイブリッドデコーディング(CHyD)を紹介する。 提案手法は,検索した文書中の連続スパンの生成を制限するハードデコード制約を強制する。 以上の結果から,既存のハイブリッド手法では抽出精度が技術領域で40%以下に低下する傾向がみられた。
  論文  参考訳（メタデータ） (2026-09-09T11:21:07Z)
• The Illusion of High Utility in Safety Alignment of Text-to-Image Diffusion Models [49.67749928542536]
  テキスト・ツー・イメージ(T2I)拡散モデルの安全性の確保は,有害な世代を抑えることを目的としている。 近年の手法は高いユーティリティで高い安全性を提供するように思われるが、この結論は主に粗いグローバルユーティリティメトリクスに依存している。 構造的評価で実用性を測定すると、この錯覚は壊れる:OnA(質問回答を用いたテキストから画像への忠実度評価) 本研究では,組込み拡散とプロンプト間関係構造を明示的に保存する安全アライメント目標であるStructureAware Geometric Regularization (SAGE)を提案する。
  論文  参考訳（メタデータ） (2026-07-01T04:00:27Z)
• Weave of Formal Thought [51.56484100374058]
  WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。 本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。 Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
  論文  参考訳（メタデータ） (2026-06-24T15:58:11Z)
• NL2Scratch: An Executable Benchmark and Evaluation for Block-Based Programming [62.89531126732269]
  NL2Scratchは自然言語からスクラッチ生成のための実行可能なベンチマークである。 23,594例のセマンティック検証プールと,スロットバランス800例の診断ベンチマークを構築した。 命令調整と微調整によるLLM実験では、語彙的類似性と意味的アライメントとの間に顕著なギャップが示される。
  論文  参考訳（メタデータ） (2026-06-20T14:22:59Z)
• Is Code Better Than Language for Algorithmic Reasoning [58.86873062890482]
  ツール拡張言語モデルでは、中間表現と実行機構の両方を変えるため、自然言語推論とコード実行パイプラインを比較することは困難である。 モデルは、その推論を実行可能なコードとして表現し、言語モデルは、そのコードを文脈でシミュレートして、回答を生成する。 中間介入は自然言語の推論と有意に異なるものではない(+0.15pp)。
  論文  参考訳（メタデータ） (2026-06-14T04:17:21Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDulは、入力変換を統一し、定義を単一の複合抽象化に述語する言語である。 我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
  論文  参考訳（メタデータ） (2025-11-13T18:06:21Z)
• SLICET5: Static Program Slicing using Language Models with Copy Mechanism and Constrained Decoding [13.61350801915956]
  静的プログラムスライシングはソフトウェア工学の基本的な技術である。 ourtoolは静的プログラムスライシングをシーケンス・ツー・シーケンスタスクとして再構成する新しいスライシングフレームワークである。 ourtoolは、最先端のベースラインを一貫して上回る。
  論文  参考訳（メタデータ） (2025-09-22T03:14:47Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。 本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。 このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
  論文  参考訳（メタデータ） (2024-01-29T16:32:36Z)
• BOOST: Harnessing Black-Box Control to Boost Commonsense in LMs' Generation [60.77990074569754]
  本稿では,凍結した事前学習言語モデルを,より汎用的な生成に向けて操る,計算効率のよいフレームワークを提案する。 具体的には、まず、文に常識的スコアを割り当てる参照なし評価器を構築する。 次に、スコアラをコモンセンス知識のオラクルとして使用し、NADOと呼ばれる制御可能な生成法を拡張して補助ヘッドを訓練する。
  論文  参考訳（メタデータ） (2023-10-25T23:32:12Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)

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

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