論文の概要: PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
- arxiv url: http://arxiv.org/abs/2405.02580v1
- Date: Sat, 4 May 2024 06:28:27 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-07 19:20:44.599498
- Title: PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
- Title（参考訳）: PropertyGPT:LLMによる検索付加資産生成によるスマートコントラクトの形式検証
- Authors: Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, Yang Liu,
- Abstract要約: PropertyGPTは包括的で高品質なプロパティを生成し、基礎的な真実と比べて80%のリコールを達成することができる。
PropertyGPTはテスト対象37件中26件のCVE/アタックインシデントを検出し、12件のゼロデイ脆弱性を発見した。
- 参考スコア（独自算出の注目度）: 11.350635014083812
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: With recent advances in large language models (LLMs), this paper explores the potential of leveraging state-of-the-art LLMs, such as GPT-4, to transfer existing human-written properties (e.g., those from Certora auditing reports) and automatically generate customized properties for unknown code. To this end, we embed existing properties into a vector database and retrieve a reference property for LLM-based in-context learning to generate a new prop- erty for a given code. While this basic process is relatively straight- forward, ensuring that the generated properties are (i) compilable, (ii) appropriate, and (iii) runtime-verifiable presents challenges. To address (i), we use the compilation and static analysis feedback as an external oracle to guide LLMs in iteratively revising the generated properties. For (ii), we consider multiple dimensions of similarity to rank the properties and employ a weighted algorithm to identify the top-K properties as the final result. For (iii), we design a dedicated prover to formally verify the correctness of the generated prop- erties. We have implemented these strategies into a novel system called PropertyGPT, with 623 human-written properties collected from 23 Certora projects. Our experiments show that PropertyGPT can generate comprehensive and high-quality properties, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and also uncovered 12 zero-day vulnerabilities, resulting in $8,256 bug bounty rewards.
- Abstract（参考訳）: 近年の大規模言語モデル (LLM) の進歩により, GPT-4 のような最先端の LLM を活用して,既存の人間記述プロパティ(例えば Certora 監査報告)を転送し,未知のコードに対してカスタマイズされたプロパティを自動的に生成する可能性について検討する。
この目的のために、既存のプロパティをベクトルデータベースに埋め込み、LLMベースのインコンテキスト学習のための参照プロパティを検索して、与えられたコードに対して新しいprop-ertyを生成する。
この基本的なプロセスは比較的直線的であるが、生成された特性が確実にあることを保証している。
(i)コンパイル可能。
(二)適当、及び
(iii) 実行時検証可能な課題。
宛て
i) コンパイルと静的解析のフィードバックを外部の託宣として使用し、LCMを反復的に生成プロパティを更新する。
目的
(ii) 特性のランク付けには類似性の複数の次元を考慮し、最終結果としてトップK特性を同定するために重み付きアルゴリズムを用いる。
目的
第三に、生成した小道具の正しさを正式に検証する専用証明器を設計する。
そこで我々は,23のCertoraプロジェクトから623の人手書きプロパティを収集し,PropertyGPTと呼ばれる新しいシステムにこれらの戦略を実装した。
実験の結果,PropertyGPTは総合的かつ高品質な特性を生成できることがわかった。
テスト対象37のうち26のCVE/アタックインシデントを検出し、12のゼロデイ脆弱性を発見した。
関連論文リスト
- AttackQA: Development and Adoption of a Dataset for Assisting Cybersecurity Operations using Fine-tuned and Open-Source LLMs [0.0]
大規模言語モデル(LLM)は、ユーザクエリに対する応答を生成するために微調整される。
本研究では,AttackQAと呼ばれるサイバーセキュリティ質問応答(Q&A)データセットを開発する。
我々は、セキュリティオペレーションセンターのアナリスト向けに設計されたRAGベースのQ&Aシステムを構築するためにそれを利用している。
論文 参考訳（メタデータ） (2024-11-01T23:03:40Z) - ELF-Gym: Evaluating Large Language Models Generated Features for Tabular Prediction [33.03433653251314]
大規模言語モデル(LLM)を評価するためのフレームワークであるELF-Gymを提案する。
私たちは、トップパフォーマンスチームによって使用される251の"ゴールド"機能を含む、歴史的なKaggleコンペティションから、新たなデータセットをキュレートしました。
ベストケースのシナリオでは、LLMがゴールデン機能の約56%を意味的にキャプチャできるが、より要求の高い実装レベルでは、オーバーラップは13%に減少する。
論文 参考訳（メタデータ） (2024-10-13T13:59:33Z) - CopyLens: Dynamically Flagging Copyrighted Sub-Dataset Contributions to LLM Outputs [39.425944445393945]
CopyLensは,著作権付きデータセットが大規模言語モデルの応答に与える影響を分析するフレームワークである。
実験の結果、CopyLensは提案したベースラインよりも効率と精度を15.2%向上し、エンジニアリング手法より58.7%、OOD検出ベースラインより0.21AUC向上した。
論文 参考訳（メタデータ） (2024-10-06T11:41:39Z) - Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。
11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。
最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
論文 参考訳（メタデータ） (2024-07-23T15:31:26Z) - SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal Behaviors [64.9938658716425]
安全でないユーザリクエストを認識して拒否する、大規模な言語モデル(LLM)の既存の評価は、3つの制限に直面している。
まず、既存の手法では、安全でないトピックの粗い粒度を使い、いくつかのきめ細かいトピックを過剰に表現している。
第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。
第3に、既存の評価は大きなLCMに頼っているため、コストがかかる可能性がある。
論文 参考訳（メタデータ） (2024-06-20T17:56:07Z) - Do Neutral Prompts Produce Insecure Code? FormAI-v2 Dataset: Labelling Vulnerabilities in Code Generated by Large Language Models [3.4887856546295333]
この研究は、最先端の大規模言語モデル(LLM)の比較分析を提供する。
中立なゼロショットプロンプトを使って単純なCプログラムを書く際に、脆弱性が発生する可能性を分析する。
論文 参考訳（メタデータ） (2024-04-29T01:24:14Z) - ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
本稿では,LLMベースのフレームワークであるReEvalについて述べる。
本稿では、ChatGPTを用いてReEvalを実装し、2つの人気のあるオープンドメインQAデータセットのバリエーションを評価する。
我々の生成したデータは人間可読であり、大きな言語モデルで幻覚を引き起こすのに役立ちます。
論文 参考訳（メタデータ） (2023-10-19T06:37:32Z) - Self-RAG: Learning to Retrieve, Generate, and Critique through
Self-Reflection [74.51523859064802]
我々は、自己回帰検索拡張生成(Self-RAG)と呼ばれる新しいフレームワークを導入する。
自己RAGは、検索と自己回帰によってLMの品質と事実性を高める。
様々なタスクセットにおいて、最先端のLCMや検索強化モデルよりも大幅に優れています。
論文 参考訳（メタデータ） (2023-10-17T18:18:32Z) - Controllable Data Generation Via Iterative Data-Property Mutual Mappings [13.282793266390316]
本稿では,VAEベースのデータジェネレータを特性制御性で拡張し,乱れを確実にするフレームワークを提案する。
提案フレームワークは, 特性誤差, ゆがみ, 生成品質, トレーニング時間に関する性能評価を行うために, VAEベースの4つの制御可能ジェネレータ上に実装されている。
論文 参考訳（メタデータ） (2023-10-11T17:34:56Z) - Source Attribution for Large Language Model-Generated Data [57.85840382230037]
合成テキストの生成に寄与したデータプロバイダを特定することで、ソース属性を実行できることが不可欠である。
我々はこの問題を透かしによって取り組めることを示した。
本稿では,アルゴリズム設計により,これらの重要な特性を満足する情報源属性フレームワークを提案する。
論文 参考訳（メタデータ） (2023-10-01T12:02:57Z) - Struc-Bench: Are Large Language Models Really Good at Generating Complex Structured Data? [49.688233418425995]
Struc-Benchは、大きな言語モデル(LLM)を特徴とする包括的なベンチマークである。
Pスコア(Prompting Score)とHスコア(Heuristical Score)の2つの革新的な指標を提案する。
実験の結果,LLaMA-7Bに構造認識の微調整を適用すると,性能が大幅に向上することがわかった。
論文 参考訳（メタデータ） (2023-09-16T11:31:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。