FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

• URL: http://arxiv.org/abs/2406.14408v2
• Date: Fri, 21 Jun 2024 02:51:41 GMT
• Title: FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
• Authors: Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, Xiaodan Liang,
• Abstract summary: We propose FVEL, an interactive formal verification environment with large language models (LLMs) FVEL transforms a given code to be verified into Isabelle, and then conducts verification via neural automated theorem proving with an LLM. The FVELER dataset includes code dependencies and verification processes that are formulated in Isabelle, containing 758 theories, 29,125 lemmas, and 200,646 proof steps in total.
• Score: 53.43068330741449
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs). However, current formal verification mainly resorts to symbolic verifiers or hand-craft rules, resulting in limitations for extensive and flexible verification. On the other hand, formal languages for automated theorem proving, such as Isabelle, as another line of rigorous verification, are maintained with comprehensive rules and theorems. In this paper, we propose FVEL, an interactive Formal Verification Environment with LLMs. Specifically, FVEL transforms a given code to be verified into Isabelle, and then conducts verification via neural automated theorem proving with an LLM. The joined paradigm leverages the rigorous yet abundant formulated and organized rules in Isabelle and is also convenient for introducing and adjusting cutting-edge LLMs. To achieve this goal, we extract a large-scale FVELER3. The FVELER dataset includes code dependencies and verification processes that are formulated in Isabelle, containing 758 theories, 29,125 lemmas, and 200,646 proof steps in total with in-depth dependencies. We benchmark FVELER in the FVEL environment by first fine-tuning LLMs with FVELER and then evaluating them on Code2Inv and SV-COMP. The results show that FVEL with FVELER fine-tuned Llama3- 8B solves 17.39% (69 -> 81) more problems, and Mistral-7B 12% (75 -> 84) more problems in SV-COMP. And the proportion of proof errors is reduced. Project page: https://fveler.github.io/.

Related papers

• Declarative Knowledge Distillation from Large Language Models for Visual Question Answering Datasets [9.67464173044675]
  Visual Question Answering (VQA) is the task of answering a question about an image. We present an approach for declarative knowledge distillation from Large Language Models (LLMs) Our results confirm that distilling knowledge from LLMs is in fact a promising direction besides data-driven rule learning approaches.
  arXiv  Detail & Related papers  (2024-10-12T08:17:03Z)
• Open-domain Implicit Format Control for Large Language Model Generation [52.83173553689678]
  We introduce a novel framework for controlled generation in large language models (LLMs) This study investigates LLMs' capabilities to follow open-domain, one-shot constraints and replicate the format of the example answers. We also develop a dataset collection methodology for supervised fine-tuning that enhances the open-domain format control of LLMs without degrading output quality.
  arXiv  Detail & Related papers  (2024-08-08T11:51:45Z)
• DARG: Dynamic Evaluation of Large Language Models via Adaptive Reasoning Graph [70.79413606968814]
  We introduce Dynamic Evaluation of LLMs via Adaptive Reasoning Graph Evolvement (DARG) to dynamically extend current benchmarks with controlled complexity and diversity. Specifically, we first extract the reasoning graphs of data points in current benchmarks and then perturb the reasoning graphs to generate novel testing data. Such newly generated test samples can have different levels of complexity while maintaining linguistic diversity similar to the original benchmarks.
  arXiv  Detail & Related papers  (2024-06-25T04:27:53Z)
• CaLM: Contrasting Large and Small Language Models to Verify Grounded Generation [76.31621715032558]
  Grounded generation aims to equip language models (LMs) with the ability to produce more credible and accountable responses. We introduce CaLM, a novel verification framework. Our framework empowers smaller LMs, which rely less on parametric memory, to validate the output of larger LMs.
  arXiv  Detail & Related papers  (2024-06-08T06:04:55Z)
• CheckEmbed: Effective Verification of LLM Solutions to Open-Ended Tasks [15.60762281287532]
  Large Language Models (LLMs) are revolutionizing various domains, yet verifying their answers remains a significant challenge. In this work, we propose CheckEmbed: an accurate, scalable, and simple LLM verification approach. CheckEmbed is driven by a straightforward yet powerful idea: compare their corresponding answer-level embeddings obtained with a model such as GPT Text Embedding Large.
  arXiv  Detail & Related papers  (2024-06-04T17:42:21Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  Large Language Models (LLMs) have shown success in code analysis and synthesis. We present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis.
  arXiv  Detail & Related papers  (2023-11-07T05:47:47Z)
• Hint-enhanced In-Context Learning wakes Large Language Models up for knowledge-intensive tasks [54.153914606302486]
  In-context learning (ICL) ability has emerged with the increasing scale of large language models (LLMs) We propose a new paradigm called Hint-enhanced In-Context Learning (HICL) to explore the power of ICL in open-domain question answering.
  arXiv  Detail & Related papers  (2023-11-03T14:39:20Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  Large language models (LLMs) have shown strong reasoning ability in several natural language processing tasks. LLMs with chain of thought (CoT) prompting require multi-step prompting and multi-token prediction, which is highly sensitive to individual mistakes. We propose and prove that LLMs also have similar self-verification abilities.
  arXiv  Detail & Related papers  (2022-12-19T15:51:52Z)

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.