PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation

• URL: http://arxiv.org/abs/2405.02580v2
• Date: Fri, 06 Dec 2024 08:41:01 GMT
• Title: PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
• Abstract summary: PropertyGPT can generate comprehensive and high-quality properties, achieving an 80% recall compared to the ground truth.<n>PropertyGPT detected 26 CVEs/attack incidents out of 37 tested and also uncovered 12 zero-day vulnerabilities, leading to $8,256 in bug bounty rewards.
• Score: 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 property for a given code. While this basic process is relatively straightforward, ensuring that the generated properties are (i) compilable, (ii) appropriate, and (iii) 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 properties. We have implemented these strategies into a novel LLM-based property generation tool called PropertyGPT. 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, leading to $8,256 in bug bounty rewards.

Related papers

• PROGRESS: Property-Guided Regression Search for Semantic Falsification [16.94326144914702]
  We present PROGRESS (PROperty-Guided REgression Search for Semantic Falsification)<n>It integrates intent-driven properties into coverage-guided, search-based evolutionary test generation to reach deep program states.<n>It detects 328/562 current-version bugs (58%) versus none for regression-test generation, and satisfies all preconditions for 70/150 hard-to-reach properties versus 18 for standalone jqwik.
  arXiv  Detail & Related papers  (2026-07-29T18:12:12Z)
• Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts [0.7929185276093964]
  This studyleverages Large Language Models to generate high-quality properties for Soliditybased smart contracts.<n>We evaluate LLMs using various prompting techniques (e.g., zero shot, few shot, and prompt chaining)<n>Overall, we find that Gemini Pro 1.5, when combined with prompt chaining, achieves the highest average mutation score of 25.99%.<n>However, our per contract analysis reveals notable variance, particularly for the LibBit contract, where Gemini Pro 1.5 under prompt chaining achieves a mutation score of 74.34%.
  arXiv  Detail & Related papers  (2026-07-25T17:49:49Z)
• Beyond Fixed Depths and Widths: Optimizing Textual Decoding Tries in LLM-based Generative Recommendation [59.20704286413859]
  We propose a novel framework that co-designs textual term IDs and their underlying decoding trie.<n> BONSAI achieves up to a 21.6% relative improvement over state-of-the-art baselines.
  arXiv  Detail & Related papers  (2026-07-18T04:31:02Z)
• Overcoming the Generalization Limits of SLM Finetuning for Shape-Based Extraction of Datatype and Object Properties [6.295923933999817]
  Small language models (SLMs) have shown promises for relation extraction (RE) when extracting RDF triples guided by SHACL shapes.<n>This paper investigates how SLMs handle both datatype and object properties for a complete RDF graph extraction.
  arXiv  Detail & Related papers  (2025-11-05T12:16:51Z)
• Loong: Synthesize Long Chain-of-Thoughts at Scale through Verifiers [103.4410890572479]
  We introduce the Loong Project: an open-source framework for scalable synthetic data generation and verification.<n>LoongBench is a curated seed dataset containing 8,729 human-vetted examples across 12 domains.<n>LoongEnv is a modular synthetic data generation environment that supports multiple prompting strategies to produce new question-answer-code triples.
  arXiv  Detail & Related papers  (2025-09-03T06:42:40Z)
• Use Property-Based Testing to Bridge LLM Code Generation and Validation [38.25155484701058]
  Large Language Models (LLMs) excel at code generation, but ensuring their outputs to be functionally correct is a persistent challenge.<n>This paper introduces Property-Generated Solver, a novel framework that leverages Property-Based Testing (PBT) to validate high-level program properties.<n>Property-Generated Solver employs two collaborative LLM-based agents: a Generator dedicated to code generation and iterative refinement, and a Tester that manages the PBT life-cycle.
  arXiv  Detail & Related papers  (2025-06-23T06:01:12Z)
• LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation [7.52190283487474]
  Formal property verification (FPV) provides the capability to model and validate design behaviors.<n>Current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone.<n>This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties.
  arXiv  Detail & Related papers  (2025-06-22T01:21:03Z)
• Structured Extraction of Process Structure Properties Relationships in Materials Science [10.10021626682367]
  We introduce a novel annotation schema designed to extract generic process-structure-properties relationships from scientific literature. We demonstrate the utility of this approach using a dataset of 128 abstracts, with annotations drawn from two distinct domains. Our results indicate that fine-tuning LLMs can significantly improve entity extraction performance over the BERT-CRF baseline on Domain I.
  arXiv  Detail & Related papers  (2025-04-04T22:44:02Z)
• Latent Factor Models Meets Instructions: Goal-conditioned Latent Factor Discovery without Task Supervision [50.45597801390757]
  Instruct-LF is a goal-oriented latent factor discovery system. It integrates instruction-following ability with statistical models to handle noisy datasets.
  arXiv  Detail & Related papers  (2025-02-21T02:03:08Z)
• Invar-RAG: Invariant LLM-aligned Retrieval for Better Generation [43.630437906898635]
  We propose a novel two-stage fine-tuning architecture called Invar-RAG. In the retrieval stage, an LLM-based retriever is constructed by integrating LoRA-based representation learning. In the generation stage, a refined fine-tuning method is employed to improve LLM accuracy in generating answers based on retrieved information.
  arXiv  Detail & Related papers  (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]
  Large language models (LLMs) are fine-tuned for generating responses to user queries. In this study, we develop a cybersecurity question-answering (Q&A) dataset, called AttackQA. We employ it to build a RAG-based Q&A system designed for analysts in security operations centers.
  arXiv  Detail & Related papers  (2024-11-01T23:03:40Z)
• ELF-Gym: Evaluating Large Language Models Generated Features for Tabular Prediction [33.03433653251314]
  We propose ELF-Gym, a framework for evaluating Large Language Models (LLMs) We curated a new dataset from historical Kaggle competitions, including 251 "golden" features used by top-performing teams. We empirically demonstrate that, in the best-case scenario, LLMs can semantically capture approximately 56% of the golden features, but at the more demanding implementation level this overlap drops to 13%.
  arXiv  Detail & Related papers  (2024-10-13T13:59:33Z)
• CopyLens: Dynamically Flagging Copyrighted Sub-Dataset Contributions to LLM Outputs [39.425944445393945]
  We introduce CopyLens, a framework to analyze how copyrighted datasets may influence Large Language Models responses. Experiments show that CopyLens improves efficiency and accuracy by 15.2% over our proposed baseline, 58.7% over prompt engineering methods, and 0.21 AUC over OOD detection baselines.
  arXiv  Detail & Related papers  (2024-10-06T11:41:39Z)
• Traceable LLM-based validation of statements in knowledge graphs [0.0]
  This article presents a method for verifying RDF triples using LLMs.<n>Because the LLMs cannot currently reliably identify the origin of the information used to construct the response to the user prompt, our approach is to avoid using internal LLM factual knowledge altogether.<n>Instead, verified RDF statements are compared to chunks of external documents retrieved through a web search or Wikipedia.
  arXiv  Detail & Related papers  (2024-09-11T12:27:41Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  This paper introduces a systematic evaluation framework to assess Large Language Models in detecting cryptographic misuses. Our in-depth analysis of 11,940 LLM-generated reports highlights that the inherent instabilities in LLMs can lead to over half of the reports being false positives. The optimized approach achieves a remarkable detection rate of nearly 90%, surpassing traditional methods and uncovering previously unknown misuses in established benchmarks.
  arXiv  Detail & Related papers  (2024-07-23T15:31:26Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal Behaviors [64.9938658716425]
  Existing evaluations of large language models' (LLMs) ability to recognize and reject unsafe user requests face three limitations. First, existing methods often use coarse-grained of unsafe topics, and are over-representing some fine-grained topics. Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations. Third, existing evaluations rely on large LLMs for evaluation, which can be expensive.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)
• Peering into the Mind of Language Models: An Approach for Attribution in Contextual Question Answering [9.86691461253151]
  We introduce a novel method for attribution in contextual question answering, leveraging the hidden state representations of large language models (LLMs) Our approach bypasses the need for extensive model retraining and retrieval model overhead, offering granular attributions and preserving the quality of generated answers. We present Verifiability-granular, an attribution dataset which has token level annotations for LLM generations in the contextual question answering setup.
  arXiv  Detail & Related papers  (2024-05-28T09:12:44Z)
• Do Neutral Prompts Produce Insecure Code? FormAI-v2 Dataset: Labelling Vulnerabilities in Code Generated by Large Language Models [3.4887856546295333]
  This study provides a comparative analysis of state-of-the-art large language models (LLMs) We analyze how likely they generate vulnerabilities when writing simple C programs using a neutral zero-shot prompt.
  arXiv  Detail & Related papers  (2024-04-29T01:24:14Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  This paper presents ReEval, an LLM-based framework using prompt chaining to perturb the original evidence for generating new test cases. We implement ReEval using ChatGPT and evaluate the resulting variants of two popular open-domain QA datasets. Our generated data is human-readable and useful to trigger hallucination in large language models.
  arXiv  Detail & Related papers  (2023-10-19T06:37:32Z)
• Self-RAG: Learning to Retrieve, Generate, and Critique through Self-Reflection [74.51523859064802]
  We introduce a new framework called Self-Reflective Retrieval-Augmented Generation (Self-RAG) Self-RAG enhances an LM's quality and factuality through retrieval and self-reflection. It significantly outperforms state-of-the-art LLMs and retrieval-augmented models on a diverse set of tasks.
  arXiv  Detail & Related papers  (2023-10-17T18:18:32Z)
• Controllable Data Generation Via Iterative Data-Property Mutual Mappings [13.282793266390316]
  We propose a framework to enhance VAE-based data generators with property controllability and ensure disentanglement. The proposed framework is implemented on four VAE-based controllable generators to evaluate its performance on property error, disentanglement, generation quality, and training time.
  arXiv  Detail & Related papers  (2023-10-11T17:34:56Z)
• Towards Verifiable Generation: A Benchmark for Knowledge-aware Language Model Attribution [48.86322922826514]
  This paper defines a new task of Knowledge-aware Language Model Attribution (KaLMA) First, we extend attribution source from unstructured texts to Knowledge Graph (KG), whose rich structures benefit both the attribution performance and working scenarios. Second, we propose a new Conscious Incompetence" setting considering the incomplete knowledge repository. Third, we propose a comprehensive automatic evaluation metric encompassing text quality, citation quality, and text citation alignment.
  arXiv  Detail & Related papers  (2023-10-09T11:45:59Z)
• Source Attribution for Large Language Model-Generated Data [57.85840382230037]
  It is imperative to be able to perform source attribution by identifying the data provider who contributed to the generation of a synthetic text. We show that this problem can be tackled by watermarking. We propose a source attribution framework that satisfies these key properties due to our algorithmic designs.
  arXiv  Detail & Related papers  (2023-10-01T12:02:57Z)
• Struc-Bench: Are Large Language Models Really Good at Generating Complex Structured Data? [49.688233418425995]
  Struc-Bench is a comprehensive benchmark featuring prominent Large Language Models (LLMs) We propose two innovative metrics, P-Score (Prompting Score) and H-Score (Heuristical Score) Our experiments show that applying our structure-aware fine-tuning to LLaMA-7B leads to substantial performance gains.
  arXiv  Detail & Related papers  (2023-09-16T11:31:58Z)
• Do-Not-Answer: A Dataset for Evaluating Safeguards in LLMs [59.596335292426105]
  This paper collects the first open-source dataset to evaluate safeguards in large language models. We train several BERT-like classifiers to achieve results comparable with GPT-4 on automatic safety evaluation.
  arXiv  Detail & Related papers  (2023-08-25T14:02:12Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.