論文の概要: 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のゼロデイ脆弱性を発見した。
関連論文リスト
- Optimizing Knowledge Integration in Retrieval-Augmented Generation with Self-Selection [72.92366526004464]
Retrieval-Augmented Generation (RAG) は、Large Language Models (LLM) がより正確で信頼性の高い応答を生成するのに有効であることが証明されている。
本稿では,自己選択型RAGフレームワークを提案する。このフレームワークでは,内部パラメトリック知識のみで生成されたペアの応答からLLMを選択できる。
論文 参考訳（メタデータ） (2025-02-10T04:29:36Z) - Invar-RAG: Invariant LLM-aligned Retrieval for Better Generation [43.630437906898635]
Invar-RAGと呼ばれる2段階ファインチューニングアーキテクチャを提案する。
検索段階では、LORAに基づく表現学習を統合してLLMベースの検索器を構築する。
生成段階では、抽出した情報に基づいて回答を生成する際のLCM精度を向上させるための精細調整法が用いられる。
論文 参考訳（メタデータ） (2024-11-11T14:25:37Z) - 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) - Peering into the Mind of Language Models: An Approach for Attribution in Contextual Question Answering [9.86691461253151]
大規模言語モデル(LLM)の隠れ状態表現を利用した文脈質問応答における帰属手法を提案する。
提案手法は,より詳細な属性を提供し,生成した回答の質を保ちながら,広範囲なモデル再訓練および検索モデルオーバーヘッドの必要性を回避している。
本稿では,LLM世代に対するトークンレベルのアノテーションを文脈質問応答設定に有する属性データセットであるVerifiability-granularを提案する。
論文 参考訳（メタデータ） (2024-05-28T09:12:44Z) - ProgGen: Generating Named Entity Recognition Datasets Step-by-step with Self-Reflexive Large Language Models [25.68491572293656]
大規模言語モデルは、名前付きエンティティ認識のような構造化された知識抽出タスクにおいて不足する。
本稿では,より優れたNERデータセットを生成するため,LCMを質素なNER能力で活用するための革新的で費用効率のよい戦略について検討する。
論文 参考訳（メタデータ） (2024-03-17T06:12:43Z) - 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) - Controllable Data Generation Via Iterative Data-Property Mutual Mappings [13.282793266390316]
本稿では,VAEベースのデータジェネレータを特性制御性で拡張し,乱れを確実にするフレームワークを提案する。
提案フレームワークは, 特性誤差, ゆがみ, 生成品質, トレーニング時間に関する性能評価を行うために, VAEベースの4つの制御可能ジェネレータ上に実装されている。
論文 参考訳（メタデータ） (2023-10-11T17:34:56Z) - Towards Verifiable Generation: A Benchmark for Knowledge-aware Language Model Attribution [48.86322922826514]
本稿では,知識認識型言語モデル属性(KaLMA)の新たな課題について述べる。
まず、属性のソースを構造化されていないテキストから知識グラフ(KG)に拡張し、そのリッチな構造は属性のパフォーマンスと作業シナリオの両方に役立ちます。
第2に,不完全な知識リポジトリを考慮した「意識的非能力」の設定を提案する。
第3に,テキスト品質,引用品質,引用アライメントを含む総合的な自動評価指標を提案する。
論文 参考訳（メタデータ） (2023-10-09T11:45:59Z) - 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) - Do-Not-Answer: A Dataset for Evaluating Safeguards in LLMs [59.596335292426105]
本稿では,大規模な言語モデルにおけるセーフガードを評価するための,最初のオープンソースデータセットを収集する。
我々は、自動安全性評価において、GPT-4に匹敵する結果を得るために、BERTライクな分類器をいくつか訓練する。
論文 参考訳（メタデータ） (2023-08-25T14:02:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。