Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models

• URL: http://arxiv.org/abs/2412.10483v1
• Date: Fri, 13 Dec 2024 10:36:18 GMT
• Title: Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models
• Authors: Ruibang Liu, Guoqiang Li, Minyu Chen, Ling-I Wu, Jingyu Ke,
• Abstract summary: ACInv is an Automated Complex program loop Invariant generation tool. It combines static analysis with Large Language Models (LLMs) to generate the proper loop invariants. We conducted experiments on ACInv, which showed that ACInv outperformed previous tools on data sets with data structures.
• Score: 2.243213786359577
• License:
• Abstract: Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, the automation of loop invariant analysis has effectively resolved the problem. However, real-world programs that often mix complex data structures and control flows pose challenges to traditional loop invariant generation tools. To enhance the applicability of invariant generation techniques, we proposed ACInv, an Automated Complex program loop Invariant generation tool, which combines static analysis with Large Language Models (LLMs) to generate the proper loop invariants. We utilize static analysis to extract the necessary information for each loop and embed it into prompts for the LLM to generate invariants for each loop. Subsequently, we employ an LLM-based evaluator to assess the generated invariants, refining them by either strengthening, weakening, or rejecting them based on their correctness, ultimately obtaining enhanced invariants. We conducted experiments on ACInv, which showed that ACInv outperformed previous tools on data sets with data structures, and maintained similar performance to the state-of-the-art tool AutoSpec on numerical programs without data structures. For the total data set, ACInv can solve 21% more examples than AutoSpec and can generate reference data structure templates.

Related papers

• An Empirical Study on Self-correcting Large Language Models for Data Science Code Generation [1.335664823620186]
  Large Language Models (LLMs) have recently advanced many applications on software engineering tasks. CoT-SelfEvolve iteratively and automatically refines code through a self-correcting process.
  arXiv  Detail & Related papers  (2024-08-28T09:19:09Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpec is an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It can be successfully applied to verify the programs in a real-world X509-parser project.
  arXiv  Detail & Related papers  (2024-03-31T18:15:49Z)
• Planning, Creation, Usage: Benchmarking LLMs for Comprehensive Tool Utilization in Real-World Complex Scenarios [93.68764280953624]
  UltraTool is a novel benchmark designed to improve and evaluate Large Language Models' ability in tool utilization. It emphasizes real-world complexities, demanding accurate, multi-step planning for effective problem-solving. A key feature of UltraTool is its independent evaluation of planning with natural language, which happens before tool usage.
  arXiv  Detail & Related papers  (2024-01-30T16:52:56Z)
• AutoAct: Automatic Agent Learning from Scratch for QA via Self-Planning [54.47116888545878]
  AutoAct is an automatic agent learning framework for QA. It does not rely on large-scale annotated data and synthetic planning trajectories from closed-source models.
  arXiv  Detail & Related papers  (2024-01-10T16:57:24Z)
• Finding Inductive Loop Invariants using Large Language Models [14.846222005558666]
  Finding inductive loop invariants is an undecidable problem. Despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models in offering a new solution.
  arXiv  Detail & Related papers  (2023-11-14T06:58:09Z)
• Time-LLM: Time Series Forecasting by Reprogramming Large Language Models [110.20279343734548]
  Time series forecasting holds significant importance in many real-world dynamic systems. We present Time-LLM, a reprogramming framework to repurpose large language models for time series forecasting. Time-LLM is a powerful time series learner that outperforms state-of-the-art, specialized forecasting models.
  arXiv  Detail & Related papers  (2023-10-03T01:31:25Z)
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection [88.23337313766353]
  This work first provides a comprehensive statistical theory for transformers to perform ICL. We show that transformers can implement a broad class of standard machine learning algorithms in context. A emphsingle transformer can adaptively select different base ICL algorithms.
  arXiv  Detail & Related papers  (2023-06-07T17:59:31Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  In deductive verification and software model checking, dealing with certain specification language constructs can be problematic. We propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation.
  arXiv  Detail & Related papers  (2023-05-26T14:55:35Z)
• TSGM: A Flexible Framework for Generative Modeling of Synthetic Time Series [61.436361263605114]
  Time series data are often scarce or highly sensitive, which precludes the sharing of data between researchers and industrial organizations. We introduce Time Series Generative Modeling (TSGM), an open-source framework for the generative modeling of synthetic time series.
  arXiv  Detail & Related papers  (2023-05-19T10:11:21Z)
• Modelling Concurrency Bugs Using Machine Learning [0.0]
  This project aims to compare both common and recent machine learning approaches. We define a synthetic dataset that we generate with the scope of simulating real-life (concurrent) programs. We formulate hypotheses about fundamental limits of various machine learning model types.
  arXiv  Detail & Related papers  (2023-05-08T17:30:24Z)
• Synthetic Datasets for Neural Program Synthesis [66.20924952964117]
  We propose a new methodology for controlling and evaluating the bias of synthetic data distributions over both programs and specifications. We demonstrate, using the Karel DSL and a small Calculator DSL, that training deep networks on these distributions leads to improved cross-distribution generalization performance.
  arXiv  Detail & Related papers  (2019-12-27T21:28:10Z)

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.