Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

• URL: http://arxiv.org/abs/2502.07728v1
• Date: Tue, 11 Feb 2025 17:42:07 GMT
• Title: Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK
• Authors: Marcos Cramer, Lucian McIntyre,
• Abstract summary: Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software verification, specifically the SPARK framework for Ada, to ensure the reliability of LLM-generated code. We present Marmaragan, a tool that leverages an LLM in order to generate SPARK annotations for existing programs, enabling formal verification of the code.
• Score: 0.4143603294943439
• License:
• Abstract: Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software verification, specifically the SPARK framework for Ada, to ensure the reliability of LLM-generated code. We present Marmaragan, a tool that leverages an LLM in order to generate SPARK annotations for existing programs, enabling formal verification of the code. The tool is benchmarked on a curated set of SPARK programs, with annotations selectively removed to test specific capabilities. The performance of Marmaragan with GPT-4o on the benchmark is promising, with correct annotations having been generated for 50.7% of the benchmark cases. The results establish a foundation for future work on combining the power of LLMs with the reliability of formal software verification.

Related papers

• Next Steps in LLM-Supported Java Verification [0.8057006406834466]
  Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. This paper provides early results on how this rigorous toolset can be used to reliably elicit correct specification annotations from an unreliable LLM.
  arXiv  Detail & Related papers  (2025-02-03T17:55:50Z)
• Correctness Assessment of Code Generated by Large Language Models Using Internal Representations [4.32362000083889]
  We introduce OPENIA, a novel framework to assess the correctness of code generated by Large Language Models (LLMs) Our empirical analysis reveals that these internal representations encode latent information, which strongly correlates with the correctness of the generated code. OPENIA consistently outperforms baseline models, achieving higher accuracy, precision, recall, and F1-Scores with up to a 2X improvement in standalone code generation.
  arXiv  Detail & Related papers  (2025-01-22T15:04:13Z)
• Automatic Generation of Benchmarks and Reliable LLM Judgment for Code Tasks [0.8274693573069442]
  This work introduces a methodology to generate and evaluate LaaJ implementations, utilizing an automatically generated benchmark. The benchmark is used both to develop and validate the LaaJs and to validate and test the LLM code related solution using the LaaJs. Our approach enables the creation of high quality code task solutions.
  arXiv  Detail & Related papers  (2024-10-28T14:34:36Z)
• LLM4VV: Exploring LLM-as-a-Judge for Validation and Verification Testsuites [6.796136787585992]
  Large Language Models (LLM) are evolving and have significantly revolutionized the landscape of software development. This paper explores the idea of judging tests used to evaluate compiler implementations of directive-based programming models.
  arXiv  Detail & Related papers  (2024-08-21T15:54:17Z)
• 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)
• Towards Large Language Model Aided Program Refinement [10.089955747110444]
  Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Large language models (LLMs) enable automatic code generations from informal natural language specifications. We propose LLM4PR, a tool that combines formal program refinement techniques with informal LLM-based methods.
  arXiv  Detail & Related papers  (2024-06-26T04:29:27Z)
• Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
  Large language models (LLMs) can reach and even surpass human-level accuracy on a variety of benchmarks, but their overconfidence in incorrect responses is still a well-documented failure mode. We propose a framework for measuring an LLM's uncertainty with respect to the distribution of generated explanations for an answer.
  arXiv  Detail & Related papers  (2024-06-05T16:35:30Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  Large language models (LLMs) have been treated as knowledge bases due to their strong performance in knowledge probing tasks. How do we evaluate the capabilities of LLMs to consistently produce factually correct answers? We propose MOdel kNowledge relIabiliTy scORe (MONITOR), a novel metric designed to directly measure LLMs' factual reliability.
  arXiv  Detail & Related papers  (2023-10-15T12:40:30Z)
• LLMRec: Benchmarking Large Language Models on Recommendation Task [54.48899723591296]
  The application of Large Language Models (LLMs) in the recommendation domain has not been thoroughly investigated. We benchmark several popular off-the-shelf LLMs on five recommendation tasks, including rating prediction, sequential recommendation, direct recommendation, explanation generation, and review summarization. The benchmark results indicate that LLMs displayed only moderate proficiency in accuracy-based tasks such as sequential and direct recommendation.
  arXiv  Detail & Related papers  (2023-08-23T16:32:54Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  We propose LEVER, a simple approach to improve language-to-code generation by learning to verify the generated programs with their execution results. Specifically, we train verifiers to determine whether a program sampled from the LLMs is correct or not based on the natural language input, the program itself and its execution results. LEVER consistently improves over the base code LLMs(4.6% to 10.9% with code-davinci) and achieves new state-of-the-art results on all of them.
  arXiv  Detail & Related papers  (2023-02-16T18:23:22Z)

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.