AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation

• URL: http://arxiv.org/abs/2406.18627v1
• Date: Wed, 26 Jun 2024 14:47:28 GMT
• Title: AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation
• Authors: Vaishnavi Pulavarthi, Deeksha Nandal, Soham Dan, Debjit Pal,
• Abstract summary: We present a novel benchmark to evaluate Large-Language Models' effectiveness for assertion generation. AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM.
• Score: 6.3585378855805725
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Assertions have been the de facto collateral for simulation-based and formal verification of hardware designs for over a decade. The quality of hardware verification, \ie, detection and diagnosis of corner-case design bugs, is critically dependent on the quality of the assertions. There has been a considerable amount of research leveraging a blend of data-driven statistical analysis and static analysis to generate high-quality assertions from hardware design source code and design execution trace data. Despite such concerted effort, all prior research struggles to scale to industrial-scale large designs, generates too many low-quality assertions, often fails to capture subtle and non-trivial design functionality, and does not produce any easy-to-comprehend explanations of the generated assertions to understand assertions' suitability to different downstream validation tasks. Recently, with the advent of Large-Language Models (LLMs), there has been a widespread effort to leverage prompt engineering to generate assertions. However, there is little effort to quantitatively establish the effectiveness and suitability of various LLMs for assertion generation. In this paper, we present AssertionBench, a novel benchmark to evaluate LLMs' effectiveness for assertion generation quantitatively. AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM. We use AssertionBench to compare state-of-the-art LLMs to assess their effectiveness in inferring functionally correct assertions for hardware designs. Our experiments demonstrate how LLMs perform relative to each other, the benefits of using more in-context exemplars in generating a higher fraction of functionally correct assertions, and the significant room for improvement for LLM-based assertion generators.

Related papers

• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench I is the first realistic benchmark built from real-world commit histories of Mathlib4. Eleanstic is a scalable parallel verification infrastructure optimized for proof checking across multiple versions of Mathlib.
  arXiv  Detail & Related papers  (2025-04-27T05:04:02Z)
• Are LLMs Ready for Practical Adoption for Assertion Generation? [6.3585378855805725]
  The quality of hardware verification, i.e., detection and diagnosis of corner-case design bugs, is critically dependent on the quality of the assertions. With the onset of generative AI such as Transformers and Large-Language Models (LLMs), there has been a renewed interest in developing novel, effective, and scalable techniques of generating functional and security assertions.
  arXiv  Detail & Related papers  (2025-02-28T01:34:45Z)
• Scalable Best-of-N Selection for Large Language Models via Self-Certainty [65.31658824274894]
  Best-of-N selection is a key technique for improving the reasoning performance of Large Language Models. We propose self-certainty, a novel and efficient metric to estimate response quality without requiring external reward models. Our findings establish self-certainty as a practical and efficient way for improving LLM reasoning capabilities.
  arXiv  Detail & Related papers  (2025-02-25T19:08:07Z)
• FACT-AUDIT: An Adaptive Multi-Agent Framework for Dynamic Fact-Checking Evaluation of Large Language Models [79.41859481668618]
  Large Language Models (LLMs) have significantly advanced the fact-checking studies. Existing automated fact-checking evaluation methods rely on static datasets and classification metrics. We introduce FACT-AUDIT, an agent-driven framework that adaptively and dynamically assesses LLMs' fact-checking capabilities.
  arXiv  Detail & Related papers  (2025-02-25T07:44:22Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  Recent advances in large language models (LLMs) have improved their performance on coding benchmarks. However, improvement is plateauing due to the exhaustion of readily available high-quality data. We propose Sol-Ver, a self-play solver-verifier framework that jointly improves a single model's code and test generation capacity.
  arXiv  Detail & Related papers  (2025-02-20T18:32:19Z)
• Scoring Verifiers: Evaluating Synthetic Verification for Code and Reasoning [59.25951947621526]
  We propose an approach which can transform existing coding benchmarks into scoring and ranking datasets to evaluate the effectiveness of synthetic verifiers. We release four new benchmarks (HE-R, HE-R+, MBPP-R, and MBPP-R+), and analyzed synthetic verification methods with standard, reasoning-based, and reward-based LLMs. Our experiments show that reasoning can significantly improve test case generation and that scaling the number of test cases enhances the verification accuracy.
  arXiv  Detail & Related papers  (2025-02-19T15:32:11Z)
• Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting [0.0]
  We present a large language model (LLM) -based flow to automatically generate high-quality SystemVerilog Assertions (SVA) We introduce a novel sub-task-focused fine-tuning approach, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Experiments demonstrate a 26% increase in the number of assertions free from syntax errors using this approach.
  arXiv  Detail & Related papers  (2024-11-23T03:52:32Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  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.
  arXiv  Detail & Related papers  (2024-10-15T21:48:57Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• TestBench: Evaluating Class-Level Test Case Generation Capability of Large Language Models [8.22619177301814]
  We introduce TestBench, a benchmark for class-level LLM-based test case generation. We construct a dataset of 108 Java programs from 9 real-world, large-scale projects on GitHub. We propose a fine-grained evaluation framework that considers five aspects of test cases: syntactic correctness, compilation correctness, test correctness, code coverage rate, and defect detection rate.
  arXiv  Detail & Related papers  (2024-09-26T06:18:06Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  Verifiers or reward models are often used to enhance the reasoning performance of large language models (LLMs) We propose training verifiers using the ubiquitous next-token prediction objective, jointly on verification and solution generation. We demonstrate that GenRM outperforms discriminative, DPO verifiers, and LLM-as-a-Judge.
  arXiv  Detail & Related papers  (2024-08-27T17:57:45Z)
• 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)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  We reformulate open-ended generation tasks into token-level prediction tasks. We instruct an LLM to self-evaluate its answers. We benchmark a range of scoring methods based on self-evaluation.
  arXiv  Detail & Related papers  (2023-12-14T19:09:22Z)
• 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)
• Revisiting Out-of-distribution Robustness in NLP: Benchmark, Analysis, and LLMs Evaluations [111.88727295707454]
  This paper reexamines the research on out-of-distribution (OOD) robustness in the field of NLP. We propose a benchmark construction protocol that ensures clear differentiation and challenging distribution shifts. We conduct experiments on pre-trained language models for analysis and evaluation of OOD robustness.
  arXiv  Detail & Related papers  (2023-06-07T17:47:03Z)
• Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
  Self-Checker is a framework comprising a set of plug-and-play modules that facilitate fact-checking. This framework provides a fast and efficient way to construct fact-checking systems in low-resource environments.
  arXiv  Detail & Related papers  (2023-05-24T01:46:07Z)

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.