論文の概要: Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt
- arxiv url: http://arxiv.org/abs/2609.06226v1
- Date: Sat, 05 Sep 2026 18:49:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-10 19:44:08.220049
- Title: Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt
- Title（参考訳）: Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt
- Abstract要約: 大規模言語モデル(LLM)は、最近、形式的証明生成において大きな進歩を遂げた。
計算セキュリティの議論は、有効な証明は確率、逆ゲーム、不変量、仮定および境界を調整しなければならないと仮定する。
本稿では、これらの依存関係をマルチモーダル生成に公開するビジュアルスクラッチパッドアプローチであるScratchyを提案する。
- 参考スコア（独自算出の注目度）: 8.739112129971362
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models (LLMs) have recently made substantial progress in formal proof generation, yet presenting distinctive challenges in cryptographic area. Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds, which can be provided by a machine-checked framework named EasyCrypt. Although all objects may appear in available context, LLMs still struggle because proof-theoretic dependencies are typically implicit in a linear representation and distributed across multiple programs. So, this paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation. Given the natural-language security description, with formal context and target propositions, the proof objects can be normalized into a typed proof-relation graph. Then a structure-preserving visual compiler transforms the graph into the formula-rich visual proof state that guides a multimodal model in generating the EasyCrypt proof. Also, the Scratchy-eval, a 114-task dataset derived from reliable official EasyCrypt files, has been introduced. It contains 64 security-form proof generations and 50 multiple-choice knowledge tests. After a series of evaluations, covering semantic grounding, relational invariants, and game reductions, classical LLMs like GPT-5.6-Sol and Claude-Opus-5 have gained a clear advantage from Scratchy's structured visual proof states. This contrast suggests that explicit proof structure can make the improvement and multimodal proof-state representation as a promising direction for computer-aided cryptography.
- Abstract（参考訳）: 大規模言語モデル (LLM) は、最近、形式的証明生成においてかなりの進歩を遂げているが、暗号領域では顕著な課題が提示されている。
計算セキュリティの議論は、有効な証明は確率、敵ゲーム、不変量、仮定、境界を調整しなければならないと仮定している。
すべてのオブジェクトが利用可能なコンテキストに現れるかもしれないが、LLMは証明理論の依存関係が一般に線形表現で暗黙的であり、複数のプログラムに分散しているため、依然として苦労している。
そこで本稿では,これらの依存関係をマルチモーダル生成に公開するビジュアルスクラッチパッドアプローチであるScratchyを提案する。
形式的な文脈と目的命題を持つ自然言語のセキュリティ記述を考えると、証明対象は型付き証明関係グラフに正規化することができる。
次に、構造保存ビジュアルコンパイラは、グラフを式豊富な視覚的証明状態に変換し、EasyCrypt証明を生成する際に、マルチモーダルモデルを導く。
また、信頼できる公式なEasyCryptファイルから派生した114タスクのデータセットであるScratchy-evalも導入された。
64のセキュリティ形式の証明世代と50の多重選択知識テストを含んでいる。
GPT-5.6-SolやClaude-Opus-5のような古典的なLCMは、セマンティックグラウンド、リレーショナル不変量、ゲーム削減といった一連の評価の後、スクラッチの構造化された視覚的証明状態から明らかな優位性を得た。
この対照的に、明示的な証明構造は、コンピュータ支援暗号の有望な方向として、改善とマルチモーダルな証明状態表現を実現することを示唆している。
関連論文リスト
- UniProbe: A Learnable Token-Level Hallucination Detector for Large VLMs using Multi-Structural Internal Representations [61.85916280854257]
LVLM(Large Vision-Language Models)は印象的な視覚的推論と対話機能を実現するが、視覚入力によるコンテンツサポートを幻覚させることが多い。
textbfUniProbeは軽量で統一された学習可能な検出器で、凍ったLVLMの不均一な計算トレースを1つの前方パスからモデル化する。
論文 参考訳（メタデータ） (2026-08-11T12:01:59Z) - Game Hopping in Lean [5.623680633781937]
本稿では,ゲームベースの暗号証明を機械化するリーン4フレームワークであるHOPSCOTCHを紹介する。
セキュリティ定義は、ステートフルな確率的オラクル間の区別不可能性として表現され、証明は標準的なゲームホッピングパラダイムに従う。
本稿では, IND-CCAの暗号化-then-MACのセキュリティ, DDHからのElGamal暗号化のセキュリティ, ワンタイムシークレットからパブリックキーのIND-CPAセキュリティへの影響, GGM擬似ランダム機能構築の形式化された証明を行った。
論文 参考訳（メタデータ） (2026-08-06T16:52:16Z) - CryptanalysisBench: Can LLMs do Cryptanalysis? [76.79639292270497]
CryptanalysisBenchは、暗号プリミティブの6つのファミリーにまたがる191のタスクである。
我々のベンチマークは3つの階層から構成されている: (i) 実用的ブレークを既知のプリミティブ; (ii) 実用的ブレークを知らないプリミティブ。
5つのフロンティアモデルではタイア1スキームの65%-86%、全力で6-12ティア2スキーム、全スケールダウンモデルの24-61が破られる。
論文 参考訳（メタデータ） (2026-07-20T22:09:40Z) - ShannonProver: Towards Automating Formal Cryptographic Proofs [14.266077895853288]
ShannonProverは暗号証明を自動化するエージェントフレームワークである。
暗号化者がセキュリティモデルを提供し、ターゲット定理をProvレベルの証明義務に分解する設定をターゲットにしている。
本稿では,ShannonProverがケーススタディの暗号証明工学のかなりの部分を自動化可能であることを示す。
論文 参考訳（メタデータ） (2026-07-03T00:50:51Z) - Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。
LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。
本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
論文 参考訳（メタデータ） (2026-04-07T19:33:54Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
大規模言語モデル(LLM)は、コード解析と合成に成功している。
我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。
プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
論文 参考訳（メタデータ） (2023-11-07T05:47:47Z) - CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
この文書はセキュリティプロトコル検証器CryptoVerifを示す。
これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。
自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
論文 参考訳（メタデータ） (2023-10-23T07:53:38Z) - Towards General Visual-Linguistic Face Forgery Detection [95.73987327101143]
ディープフェイクは現実的な顔操作であり、セキュリティ、プライバシー、信頼に深刻な脅威をもたらす可能性がある。
既存の方法は、このタスクを、デジタルラベルまたはマスク信号を使用して検出モデルをトレーニングするバイナリ分類として扱う。
本稿では, 微粒な文レベルのプロンプトをアノテーションとして用いた, VLFFD (Visual-Linguistic Face Forgery Detection) という新しいパラダイムを提案する。
論文 参考訳（メタデータ） (2023-07-31T10:22:33Z) - Publicly-Verifiable Deletion via Target-Collapsing Functions [81.13800728941818]
ターゲットの折り畳みは、公開可能な削除(PVD)を可能にすることを示す。
我々は、弱い暗号的仮定から公開可能な削除を支援する様々なプリミティブを得るために、このフレームワークを構築している。
論文 参考訳（メタデータ） (2023-03-15T15:00:20Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。