FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware

• URL: http://arxiv.org/abs/2410.23299v1
• Date: Tue, 15 Oct 2024 21:48:57 GMT
• Title: FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware
• Authors: Minwoo Kang, Mingjie Liu, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren,
• Abstract summary: We present FVEval, the first comprehensive benchmark for characterizing large language models (LLMs) performance in tasks pertaining to formal verification (FV) The benchmark consists of three sub-tasks that measure LLM capabilities at different levels. We present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with FV.
• Score: 4.480157114854711
• License:
• Abstract: The remarkable reasoning and code generation capabilities of large language models (LLMs) have spurred significant interest in applying LLMs to enable task automation in digital chip design. In particular, recent work has investigated early ideas of applying these models to formal verification (FV), an approach to verifying hardware implementations that can provide strong guarantees of confidence but demands significant amounts of human effort. While the value of LLM-driven automation is evident, our understanding of model performance, however, has been hindered by the lack of holistic evaluation. In response, we present FVEval, the first comprehensive benchmark and evaluation framework for characterizing LLM performance in tasks pertaining to FV. The benchmark consists of three sub-tasks that measure LLM capabilities at different levels: from the generation of SystemVerilog assertions (SVAs) given natural language descriptions to reasoning about the design RTL and suggesting assertions directly without additional human input. As test instances, we present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with industrial FV workflows. A wide range of existing LLMs, both proprietary and open-source, are evaluated against FVEval, based on which we investigate where today's LLMs stand and how we might further enable their application toward improving productivity in digital FV. Our benchmark and evaluation code is available at \url{https://github.com/NVlabs/FVEval}.

Related papers

• AutoBench-V: Can Large Vision-Language Models Benchmark Themselves? [55.14033256706175]
  Large Vision-Language Models (LVLMs) have become essential for advancing the integration of visual and linguistic information. We introduce AutoBench-V, an automated framework for serving evaluation on demand. Through an extensive evaluation of seven popular LVLMs across five demanded user inputs, the framework shows effectiveness and reliability.
  arXiv  Detail & Related papers  (2024-10-28T17:55:08Z)
• VulnLLMEval: A Framework for Evaluating Large Language Models in Software Vulnerability Detection and Patching [0.9208007322096533]
  Large Language Models (LLMs) have shown promise in tasks like code translation. This paper introduces VulnLLMEval, a framework designed to assess the performance of LLMs in identifying and patching vulnerabilities in C code. Our study includes 307 real-world vulnerabilities extracted from the Linux kernel.
  arXiv  Detail & Related papers  (2024-09-16T22:00:20Z)
• 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)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  Large Language Models (LLMs) have demonstrated impressive capability in many natural language tasks. LLMs are prone to produce errors, hallucinations and inconsistent statements when performing multi-step reasoning. We introduce Q*, a framework for guiding LLMs decoding process with deliberative planning.
  arXiv  Detail & Related papers  (2024-06-20T13:08:09Z)
• An Empirical Study of Automated Vulnerability Localization with Large Language Models [21.84971967029474]
  Large Language Models (LLMs) have shown potential in various domains, yet their effectiveness in vulnerability localization remains underexplored. Our investigation encompasses 10+ leading LLMs suitable for code analysis, including ChatGPT and various open-source models. We explore the efficacy of these LLMs using 4 distinct paradigms: zero-shot learning, one-shot learning, discriminative fine-tuning, and generative fine-tuning.
  arXiv  Detail & Related papers  (2024-03-30T08:42:10Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  We introduce a novel task, Counterfactual Logical Modification (CLOMO), and a high-quality human-annotated benchmark. In this task, LLMs must adeptly alter a given argumentative text to uphold a predetermined logical relationship. We propose an innovative evaluation metric, the Self-Evaluation Score (SES), to directly evaluate the natural language output of LLMs.
  arXiv  Detail & Related papers  (2023-11-29T08:29:54Z)
• SEED-Bench-2: Benchmarking Multimodal Large Language Models [67.28089415198338]
  Multimodal large language models (MLLMs) have recently demonstrated exceptional capabilities in generating not only texts but also images given interleaved multimodal inputs. SEED-Bench-2 comprises 24K multiple-choice questions with accurate human annotations, which spans 27 dimensions. We evaluate the performance of 23 prominent open-source MLLMs and summarize valuable observations.
  arXiv  Detail & Related papers  (2023-11-28T05:53:55Z)
• ReForm-Eval: Evaluating Large Vision Language Models via Unified Re-Formulation of Task-Oriented Benchmarks [76.25209974199274]
  Large vision-language models (LVLMs) exhibit surprising capabilities to perceive visual signals and perform visually grounded reasoning. Our benchmark and evaluation framework will be open-sourced as a cornerstone for advancing the development of LVLMs.
  arXiv  Detail & Related papers  (2023-10-04T04:07:37Z)
• Measuring and Improving Chain-of-Thought Reasoning in Vision-Language Models [61.28463542324576]
  Vision-language models (VLMs) have recently demonstrated strong efficacy as visual assistants that can generate human-like outputs. We evaluate existing state-of-the-art VLMs and find that even the best-performing model is unable to demonstrate strong visual reasoning capabilities and consistency. We propose a two-stage training framework aimed at improving both the reasoning performance and consistency of VLMs.
  arXiv  Detail & Related papers  (2023-09-08T17:49:44Z)

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.