Selene: Pioneering Automated Proof in Software Verification

本文介绍了软件工程中确保正确性的关键方面。在各种可用的策略中，软件验证提供了明确的正确性保证。然而，编写验证证明是资源密集型且耗费人力的，因此迫切需要自动化此过程。本文介绍了Selene，这是第一个基于实际工业级项目seL4操作系统微内核构建的项目级自动化证明基准。Selene提供了全面的端到端评估框架和轻量级验证环境。我们使用先进的LLMs（如GPT-3.5-turbo和GPT-4）进行实验，突显了大型语言模型在自动证明生成领域的能力。此外，我们进一步提出的增强措施表明，Selene所面临的挑战可以在未来的研究中得到缓解。

自动化软件验证是一项资源密集型的任务，本文试图通过构建Selene项目，基于seL4操作系统微内核的真实工业级项目，提供一个全面的框架来进行端到端的评估和轻量级验证环境，以解决自动化软件验证的问题。

本文提出了Selene，这是第一个基于工业级项目构建的自动化证明基准，它展示了大型语言模型在自动证明生成领域的能力。

本文使用了先进的LLMs，如GPT-3.5-turbo和GPT-4，进行实验，并提出了进一步的增强方案以解决Selene所面临的挑战。此外，本文的实验设计充分考虑了数据集和开源代码等方面。

在这个领域中，最近的相关研究包括：1. Automated Formal Verification of seL4: A Comprehensive, Machine-Checked Formalization 2. DeepSpec: Verified Compilation for x86-TSO