Selene: Pioneering Automated Proof in Software Verification

• URL: http://arxiv.org/abs/2401.07663v2
• Date: Wed, 5 Jun 2024 08:16:12 GMT
• Title: Selene: Pioneering Automated Proof in Software Verification
• Authors: Lichen Zhang, Shuai Lu, Nan Duan,
• Abstract summary: We introduce Selene, which is the first project-level automated proof benchmark constructed based on the real-world industrial-level operating system microkernel, seL4. Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of LLMs in the domain of automated proof generation.
• Score: 62.09555413263788
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ensuring correctness is a pivotal aspect of software engineering. Among the various strategies available, software verification offers a definitive assurance of correctness. Nevertheless, writing verification proofs is resource-intensive and manpower-consuming, and there is a great need to automate this process. We introduce Selene in this paper, which is the first project-level automated proof benchmark constructed based on the real-world industrial-level operating system microkernel, seL4. Selene provides a comprehensive framework for end-to-end proof generation and a lightweight verification environment. Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of LLMs in the domain of automated proof generation. Additionally, our further proposed augmentations indicate that the challenges presented by Selene can be mitigated in future research endeavors.

Related papers

• The Dual-use Dilemma in LLMs: Do Empowering Ethical Capacities Make a Degraded Utility? [54.18519360412294]
  Large Language Models (LLMs) must balance between rejecting harmful requests for safety and accommodating legitimate ones for utility. This paper presents a Direct Preference Optimization (DPO) based alignment framework that achieves better overall performance. Our resulting model, LibraChem, outperforms leading LLMs including Claude-3, GPT-4o, and LLaMA-3 by margins of 13.44%, 7.16%, and 7.10% respectively.
  arXiv  Detail & Related papers  (2025-01-20T06:35:01Z)
• The Potential of LLMs in Automating Software Testing: From Generation to Reporting [0.0]
  Manual testing, while effective, can be time consuming and costly, leading to an increased demand for automated methods. Recent advancements in Large Language Models (LLMs) have significantly influenced software engineering. This paper explores an agent-oriented approach to automated software testing, using LLMs to reduce human intervention and enhance testing efficiency.
  arXiv  Detail & Related papers  (2024-12-31T02:06:46Z)
• AutoPT: How Far Are We from the End2End Automated Web Penetration Testing? [54.65079443902714]
  We introduce AutoPT, an automated penetration testing agent based on the principle of PSM driven by LLMs. Our results show that AutoPT outperforms the baseline framework ReAct on the GPT-4o mini model.
  arXiv  Detail & Related papers  (2024-11-02T13:24:30Z)
• Towards Automated Penetration Testing: Introducing LLM Benchmark, Analysis, and Improvements [1.4433703131122861]
  Large language models (LLMs) have shown potential across various domains, including cybersecurity. There is currently no comprehensive, open, end-to-end automated penetration testing benchmark. This paper introduces a novel open benchmark for LLM-based automated penetration testing.
  arXiv  Detail & Related papers  (2024-10-22T16:18:41Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a novel framework that overcomes the lack of human-written proof to enable automated proof generation of Rust code. We demonstrate superior efficiency and precision compared to GPT-4o. This advancement leads to a significant improvement in performance, achieving a 70.50% accuracy rate in a benchmark crafted by human experts.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Prompting Large Language Models to Tackle the Full Software Development Lifecycle: A Case Study [72.24266814625685]
  We explore the performance of large language models (LLMs) across the entire software development lifecycle with DevEval. DevEval features four programming languages, multiple domains, high-quality data collection, and carefully designed and verified metrics for each task. Empirical studies show that current LLMs, including GPT-4, fail to solve the challenges presented within DevEval.
  arXiv  Detail & Related papers  (2024-03-13T15:13:44Z)
• A Preliminary Study on Using Large Language Models in Software Pentesting [2.0551676463612636]
  Large language models (LLM) are perceived to offer promising potentials for automating security tasks. We investigate the use of LLMs in software pentesting, where the main task is to automatically identify software security vulnerabilities in source code.
  arXiv  Detail & Related papers  (2024-01-30T21:42:59Z)
• Towards Generating Executable Metamorphic Relations Using Large Language Models [46.26208489175692]
  We propose an approach for automatically deriving executable MRs from requirements using large language models (LLMs) To assess the feasibility of our approach, we conducted a questionnaire-based survey in collaboration with Siemens Industry Software.
  arXiv  Detail & Related papers  (2024-01-30T13:52:47Z)
• 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)

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.