論文の概要: CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes
- arxiv url: http://arxiv.org/abs/2606.25561v1
- Date: Wed, 24 Jun 2026 08:37:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-25 17:05:30.280867
- Title: CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes
- Title（参考訳）: CrypFormBench: 暗号スキーマのための大規模言語モデルのベンチマーク形式解析能力
- Abstract要約: 大規模言語モデル(LLM)は有望な代替手段であるが、この領域におけるそれらの有効性は未解明のままである。
CrypFormBench (C.F.B) は,5つのコアLLM機能を評価するために,シンボル的および計算的セキュリティを共同でカバーするベンチマークである。
677のスキームにまたがる700のインスタンス、7つの主要な形式検証言語、160のセキュリティプロパティで構成されている。
クロード3.5は100点中48.7点で最高得点を記録した。
- 参考スコア（独自算出の注目度）: 16.171581449458582
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Manual formal analysis of cryptographic schemes is labor-intensive and requires substantial expertise. While model-checking tools (e.g., Scyther and Tamarin) and computational-security tools (e.g., CryptoVerif and EasyCrypt) improve the automation of security proofs, they still rely on experts to abstract schemes and write tool-specific formal descriptions. Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored due to the absence of standardized evaluation methodologies. To fill this gap, we introduce CrypFormBench (C.F.B for short), a comprehensive benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities: interpretation, generation, completion, transformation, and correction. It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties. The evaluation of 9 state-of-the-art LLMs reveals that most of them perform well on interpretation and completion, given their code-awareness advantages, but struggle with generation, transformation, and correction. Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100. We further provide practical guidance, e.g., few-shot prompting, Pass@K sampling, and lightweight fine-tuning, to mitigate the executability bottleneck and improve tool-usable outputs. Taken together, our benchmark and analyses offer a grounded view of current progress and concrete directions toward reliable LLM-assisted formal cryptographic analysis.
- Abstract（参考訳）: 暗号方式のマニュアル形式解析は労働集約的であり、かなりの専門知識を必要とする。
モデルチェックツール(ScytherやTamarinなど)や計算セキュリティツール(CryptoVerifやEasyCryptなど)はセキュリティ証明の自動化を改善しているが、それでも専門家は抽象的なスキームやツール固有の形式記述に頼っている。
大規模言語モデル(LLM)は有望な代替手段であるが、標準化された評価手法がないため、この領域でのそれらの有効性は未解明のままである。
CrypFormBench(略してC.F.B)は、シンボルと計算のセキュリティを共同でカバーし、解釈、生成、完了、変換、修正の5つの中核LSM機能を評価するための総合ベンチマークである。
677のスキームにまたがる700のインスタンス、7つの主要な形式検証言語、160のセキュリティプロパティで構成されている。
9つの最先端LCMの評価は、コード認識の優位性を考えると、そのほとんどが解釈と完成に優れており、生成、変換、修正に苦戦していることを示している。
クロード3.5は100点中48.7点で最高得点を記録した。
さらに、実行可能性ボトルネックを緩和し、ツール使用可能なアウトプットを改善するために、実用的なガイダンス、例えば、数発のプロンプト、Pass@Kサンプリング、軽量な微調整を提供する。
ベンチマークと分析を合わせて、信頼性の高いLCM支援形式暗号解析に向けた現在の進捗状況と具体的な方向性を概観する。
関連論文リスト
- Beyond the Syntax: Do Security Experts Trust LLMs for NIDS Rule Engineering? [70.17374586573033]
本稿では,Large Language Models(LLMs)に基づくNIDSルールエンジニアリングを人間中心で調査する。
LLMは構文的に正しい規則を生成するが、専門家は部分的にしか展開できないと考えている。
大規模モデルは構文的に有効な規則を一貫して生成するが、小型モデルはIDSルールの生成にはほとんど効果がない。
論文 参考訳（メタデータ） (2026-07-07T07:09:56Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。
NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。
7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。
以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
論文 参考訳（メタデータ） (2026-04-24T14:28:10Z) - Compiled AI: Deterministic Code Generation for LLM-Based Workflow Automation [3.225273674498579]
我々は,大言語モデルがコンパイルフェーズ中に実行可能なコードアーティファクトを生成するパラダイムであるコンパイルAIについて研究し,その後,さらなるモデル実行を必要とせずに決定的に実行する。
当社のコントリビューションは、ハイテイクなランタイムエンタープライズへの適用に関するシステム指向の研究です。
論文 参考訳（メタデータ） (2026-04-06T20:25:20Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - LLMxCPG: Context-Aware Vulnerability Detection Through Code Property Graph-Guided Large Language Models [2.891351178680099]
本稿では,コードプロパティグラフ(CPG)とLarge Language Models(LLM)を統合し,堅牢な脆弱性検出を行う新しいフレームワークを提案する。
より簡潔で正確なコードスニペット表現を提供するアプローチの能力は、より大きなコードセグメントの分析を可能にします。
実証的な評価は、検証済みデータセット間でLLMxCPGの有効性を示し、最先端のベースラインよりもF1スコアが15～40%改善されている。
論文 参考訳（メタデータ） (2025-07-22T13:36:33Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - BinMetric: A Comprehensive Binary Analysis Benchmark for Large Language Models [50.17907898478795]
本稿では,バイナリ解析タスクにおける大規模言語モデルの性能評価のためのベンチマークであるBinMetricを紹介する。
BinMetricは6つの実用的なバイナリ分析タスクにわたる20の実際のオープンソースプロジェクトから得られた1000の質問で構成されている。
本ベンチマークの実証実験では, 各種LLMのバイナリ解析能力について検討し, その強度と限界を明らかにした。
論文 参考訳（メタデータ） (2025-05-12T08:54:07Z) - CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection [2.5228276786940182]
本稿では,異なる手法の脆弱性検出能力を評価するためのベンチマークフレームワークであるCASTLEを紹介する。
我々は,25個のCWEをカバーする250個のマイクロベンチマークプログラムを手作りしたデータセットを用いて,静的解析ツール13,LLM10,形式検証ツール2を評価した。
論文 参考訳（メタデータ） (2025-03-12T14:30:05Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructions [72.56339136017759]
BigCodeBenchは、大規模言語モデル(LLM)に対して、139のライブラリと7つのドメインから1140のきめ細かいタスクに対して、複数の関数呼び出しをツールとして呼び出すためのベンチマークである。
評価の結果,LLMは機能コールを正確に使用するための複雑な指示に従うことができず,スコアは最大60%,人的性能は97%と極めて低いことがわかった。
そこで本研究では,BigCodeBench-Instructという自然言語指向の変種を提案する。
論文 参考訳（メタデータ） (2024-06-22T15:52:04Z) - SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
SORRY-Benchは、安全でないユーザ要求を認識し拒否する大規模言語モデル(LLM)能力を評価するためのベンチマークである。
まず、既存の手法では、安全でないトピックの粗い分類を使い、いくつかのきめ細かいトピックを過剰に表現している。
第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。
論文 参考訳（メタデータ） (2024-06-20T17:56:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。