論文の概要: LLMs as verification oracles for Solidity

• arxiv url: http://arxiv.org/abs/2509.19153v1
• Date: Tue, 23 Sep 2025 15:32:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-24 20:41:27.925883
• Title: LLMs as verification oracles for Solidity
• Title（参考訳）: 固体の検証オーラクルとしてのLCM
• Authors: Massimo Bartoletti, Enrico Lipparini, Livio Pompianu,
• Abstract要約: 本稿では,この役割において,最先端の推論LLMである GPT-5 を初めて体系的に評価する。 我々は,大規模な検証タスクのデータセット上でその性能をベンチマークし,その出力を確立された形式的検証ツールと比較し,実世界の監査シナリオにおける実効性を評価する。 我々の研究は、AIの収束における新たなフロンティアと、セキュアなスマートコントラクト開発と監査のための形式的手法を示唆している。
• 参考スコア（独自算出の注目度）: 1.3887048755037537
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ensuring the correctness of smart contracts is critical, as even subtle flaws can lead to severe financial losses. While bug detection tools able to spot common vulnerability patterns can serve as a first line of defense, most real-world exploits and losses stem from errors in the contract business logic. Formal verification tools such as SolCMC and the Certora Prover address this challenge, but their impact remains limited by steep learning curves and restricted specification languages. Recent works have begun to explore the use of large language models (LLMs) for security-related tasks such as vulnerability detection and test generation. Yet, a fundamental question remains open: can LLMs serve as verification oracles, capable of reasoning about arbitrary contract-specific properties? In this paper, we provide the first systematic evaluation of GPT-5, a state-of-the-art reasoning LLM, in this role. We benchmark its performance on a large dataset of verification tasks, compare its outputs against those of established formal verification tools, and assess its practical effectiveness in real-world auditing scenarios. Our study combines quantitative metrics with qualitative analysis, and shows that recent reasoning-oriented LLMs can be surprisingly effective as verification oracles, suggesting a new frontier in the convergence of AI and formal methods for secure smart contract development and auditing.
• Abstract（参考訳）: スマートコントラクトの正しさを保証することは、微妙な欠陥でさえ、深刻な財政的損失につながる可能性があるため、非常に重要です。 一般的な脆弱性パターンを見つけることのできるバグ検出ツールは、防御の第一線として機能するが、実際の悪用と損失のほとんどは、コントラクトビジネスロジックのエラーに起因する。 SolCMCやCertora Proverのような形式的な検証ツールはこの課題に対処するが、その影響は急勾配の学習曲線や制限された仕様言語によって制限されている。 近年,脆弱性検出やテスト生成といったセキュリティ関連のタスクに対して,大規模言語モデル(LLM)の利用が検討されている。 LLMは検証のオラクルとして機能し、任意のコントラクト固有のプロパティを推論できますか? 本稿では,GPT-5のシステム評価を初めて実施し,その役割について述べる。 我々は,大規模な検証タスクのデータセット上でその性能をベンチマークし,その出力を確立された形式的検証ツールと比較し,実世界の監査シナリオにおける実効性を評価する。 本研究は,定量的メトリクスと質的分析を組み合わせることで,近年の推論指向LLMは,AIの収束における新たなフロンティアと,スマートコントラクト開発と監査のための形式的手法の確立を示唆する証拠として,驚くほど有効であることを示す。

関連論文リスト

• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  本稿では,Slither-based detectors, Large Language Models (LLMs), Kontrol, Forgeを統合した新しい検出パイプラインを提案する。 私たちのアプローチは、欠陥を確実に検出し、証明を生成するように設計されています。
  論文  参考訳（メタデータ） (2025-09-16T12:46:11Z)
• Verifying the Verifiers: Unveiling Pitfalls and Potentials in Fact Verifiers [59.168391398830515]
  我々は,14のファクトチェックベンチマークのサンプルを用いて,12の事前学習LDMと1つの特殊ファクト検証器を評価した。 データセットにおけるアノテーションエラーとあいまいさに対処することの重要性を強調します。 最上位のパフォーマンスを実現するために、前作でしばしば見落とされがちな、数ショットのインコンテキストの例を持つフロンティアLSM。
  論文  参考訳（メタデータ） (2025-06-16T10:32:10Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [60.881609323604685]
  ブラックボックスAPIを通じてアクセスされるLarge Language Models (LLM)は、信頼の課題をもたらす。 ユーザーは、宣伝されたモデル機能に基づいたサービスの料金を支払う。 プロバイダは、運用コストを削減するために、特定のモデルを安価で低品質の代替品に隠蔽的に置き換えることができる。 この透明性の欠如は、公正性を損なうとともに、信頼を損なうとともに、信頼性の高いベンチマークを複雑にする。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。 11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。 最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
  論文  参考訳（メタデータ） (2024-07-23T15:31:26Z)
• An Insight into Security Code Review with LLMs: Capabilities, Obstacles, and Influential Factors [9.309745288471374]
  セキュリティコードレビューは時間と労力を要するプロセスです。 既存のセキュリティ分析ツールは、一般化の貧弱、偽陽性率の高い、粗い検出粒度に悩まされている。 大きな言語モデル(LLM)は、これらの課題に対処するための有望な候補と考えられている。
  論文  参考訳（メタデータ） (2024-01-29T17:13:44Z)
• Understanding the Effectiveness of Large Language Models in Detecting Security Vulnerabilities [12.82645410161464]
  5つの異なるセキュリティデータセットから5,000のコードサンプルに対して、16の事前学習された大規模言語モデルの有効性を評価する。 全体として、LSMは脆弱性の検出において最も穏やかな効果を示し、データセットの平均精度は62.8%、F1スコアは0.71である。 ステップバイステップ分析を含む高度なプロンプト戦略は、F1スコア(平均0.18まで)で実世界のデータセット上でのLLMのパフォーマンスを著しく向上させることがわかった。
  論文  参考訳（メタデータ） (2023-11-16T13:17:20Z)
• A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
  論理的推論の文脈において,大規模言語モデル(LLM)の自己検証能力について詳しく検討する。 本研究の主目的は,既存のLCMが誤った推論手順を正確に識別するのに苦労し,自己検証法の有効性を保証できないことにある。
  論文  参考訳（メタデータ） (2023-11-14T07:13:10Z)
• Large Language Model-Powered Smart Contract Vulnerability Detection: New Perspectives [8.524720028421447]
  本稿では, GPT-4 のような大規模言語モデル (LLM) を利用する機会, 課題, 潜在的な解決策を体系的に分析する。 高いランダム性でより多くの答えを生成することは、正しい答えを生み出す可能性を大幅に押し上げるが、必然的に偽陽性の数が増加する。 本稿では,GPTLens と呼ばれる,従来の一段階検出を2つの相乗的段階に分割し,生成と識別を行う逆方向のフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-10-02T12:37:23Z)

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

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