Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs

• URL: http://arxiv.org/abs/2501.12972v1
• Date: Wed, 22 Jan 2025 15:57:29 GMT
• Title: Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
• Authors: Jan Corazza, Ivan Gavran, Gabriela Moreira, Daniel Neider,
• Abstract summary: One of the most powerful ways of establishing software correctness is by using formal methods.<n>Our work addresses this critical disadvantage by automating the creation of a formal model.<n>In this way, we significantly reduce the amount of time necessary to create formal models.
• Score: 7.087237546722617
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct -- vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model -- a mathematical abstraction of the software system -- which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we "fill in the blanks" using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.

Related papers

• Inference-Time Intervention in Large Language Models for Reliable Requirement Verification [2.3759432635713895]
  Inference-time intervention techniques provide a promising alternative to fine-tuning. We demonstrate how interventions enable fine-grained control for automating the usually time-intensive requirement verification process. Our method achieves robust and reliable outputs, significantly improving over both a baseline model and a fine-tuning approach.
  arXiv  Detail & Related papers  (2025-03-18T10:49:36Z)
• Contract Based Program Models for Software Model Checking [0.0]
  We propose a formalism previously developed for the purposes of compositional model checking. We describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written inC.
  arXiv  Detail & Related papers  (2025-03-14T09:34:59Z)
• Adversarial Reasoning at Jailbreaking Time [49.70772424278124]
  We develop an adversarial reasoning approach to automatic jailbreaking via test-time computation. Our approach introduces a new paradigm in understanding LLM vulnerabilities, laying the foundation for the development of more robust and trustworthy AI systems.
  arXiv  Detail & Related papers  (2025-02-03T18:59:01Z)
• Assisting Mathematical Formalization with A Learning-based Premise Retriever [29.06255449960557]
  We introduce an innovative method for training a premise retriever to support the formalization of mathematics. Our approach employs a BERT model to embed proof states and premises into a shared latent space. To streamline the formalization process, we will release a search engine that enables users to query Mathlib theorems directly using proof states.
  arXiv  Detail & Related papers  (2025-01-21T06:32:25Z)
• Leveraging Large Language Models and Machine Learning for Smart Contract Vulnerability Detection [0.0]
  We train and test machine learning algorithms to classify smart contract codes according to type in order to compare model performance. Our research combines machine learning and large language models to provide a rich and interpretable framework for detecting different smart contract vulnerabilities.
  arXiv  Detail & Related papers  (2025-01-04T08:32:53Z)
• Leveraging Fine-Tuned Language Models for Efficient and Accurate Smart Contract Auditing [5.65127016235615]
  This paper investigates the feasibility of using smaller, fine-tuned models to achieve comparable or even superior results in smart contract auditing. We introduce the FTSmartAudit framework, which is designed to develop cost-effective, specialized models for smart contract auditing. Our contributions include: (1) a single-task learning framework that streamlines data preparation, training, evaluation, and continuous learning; (2) a robust dataset generation method utilizing domain-special knowledge distillation to produce high-quality datasets from advanced models like GPT-4o; and (3) an adaptive learning strategy to maintain model accuracy and robustness.
  arXiv  Detail & Related papers  (2024-10-17T09:09:09Z)
• Adversarial Contrastive Decoding: Boosting Safety Alignment of Large Language Models via Opposite Prompt Optimization [34.29833630422768]
  Adversarial Contrastive Decoding (ACD) is an optimization-based framework to generate two opposite system prompts for prompt-based contrastive decoding. ACD achieves much better safety performance than previous model training-free decoding methods without sacrificing original generation ability.
  arXiv  Detail & Related papers  (2024-06-24T15:51:30Z)
• DeAL: Decoding-time Alignment for Large Language Models [59.63643988872571]
  Large Language Models (LLMs) are nowadays expected to generate content aligned with human preferences. We propose DeAL, a framework that allows the user to customize reward functions and enables Detime Alignment of LLMs. Our experiments show that we can DeAL with fine-grained trade-offs, improve adherence to alignment objectives, and address residual gaps in LLMs.
  arXiv  Detail & Related papers  (2024-02-05T06:12:29Z)
• Increasing Trust in Language Models through the Reuse of Verified Circuits [1.8434042562191815]
  Language Models (LMs) are increasingly used for a wide range of prediction tasks, but their training can often neglect rare edge cases. We show that a model can be trained to meet this standard if built using mathematically and logically specified frameworks. We find extensive reuse of the addition circuits for both tasks, easing verification of the more complex subtractor model.
  arXiv  Detail & Related papers  (2024-02-04T21:33:18Z)
• Adapting Large Language Models for Content Moderation: Pitfalls in Data Engineering and Supervised Fine-tuning [79.53130089003986]
  Large Language Models (LLMs) have become a feasible solution for handling tasks in various domains. In this paper, we introduce how to fine-tune a LLM model that can be privately deployed for content moderation.
  arXiv  Detail & Related papers  (2023-10-05T09:09:44Z)
• Cheaply Evaluating Inference Efficiency Metrics for Autoregressive Transformer APIs [66.30706841821123]
  Large language models (LLMs) power many state-of-the-art systems in natural language processing. LLMs are extremely computationally expensive, even at inference time. We propose a new metric for comparing inference efficiency across models.
  arXiv  Detail & Related papers  (2023-05-03T21:51:42Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  Large language models (LLMs) for automatic code generation have achieved breakthroughs in several programming tasks. Training data for these models is usually collected from the Internet (e.g., from open-source repositories) and is likely to contain faults and security vulnerabilities. This unsanitized training data can cause the language models to learn these vulnerabilities and propagate them during the code generation procedure.
  arXiv  Detail & Related papers  (2023-02-08T11:54:07Z)
• The Right Tool for the Job: Matching Model and Instance Complexities [62.95183777679024]
  As NLP models become larger, executing a trained model requires significant computational resources incurring monetary and environmental costs. We propose a modification to contextual representation fine-tuning which, during inference, allows for an early (and fast) "exit" We test our proposed modification on five different datasets in two tasks: three text classification datasets and two natural language inference benchmarks.
  arXiv  Detail & Related papers  (2020-04-16T04:28:08Z)

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.