LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking

• URL: http://arxiv.org/abs/2602.24010v1
• Date: Fri, 27 Feb 2026 13:34:48 GMT
• Title: LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
• Authors: Mingkai Miao, Guangyu Hu, Wei Zhang, Hongce Zhang,
• Abstract summary: Property checking of RTL designs is a central task in formal verification.<n>We introduce LeGend, which replaces a per-clause graph analysis paradigm with one-time global representation learning.<n> Experiments show LeGend accelerates two state-of-the-art IC3/PDR engines across a diverse set of benchmarks.
• Score: 3.5968163492929346
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Property checking of RTL designs is a central task in formal verification. Among available engines, IC3/PDR is a widely used backbone whose performance critically depends on inductive generalization, the step that generalizes a concrete counterexample-to-induction (CTI) cube into a lemma. Prior work has explored machine learning to guide this step and achieved encouraging results, yet most methods adopt a per-clause graph analysis paradigm: for each clause they repeatedly build and analyze graphs, incurring heavy overhead and creating a scalability bottleneck. We introduce LeGend, which replaces this paradigm with one-time global representation learning. LeGend pre-trains a domain-adapted self-supervised model to produce latch embeddings that capture global circuit properties. These precomputed embeddings allow a lightweight model to predict high-quality lemmas with negligible overhead, effectively decoupling expensive learning from fast inference. Experiments show LeGend accelerates two state-of-the-art IC3/PDR engines across a diverse set of benchmarks, presenting a promising path to scale up formal verification.

Related papers

• HELP: HyperNode Expansion and Logical Path-Guided Evidence Localization for Accurate and Efficient GraphRAG [53.30561659838455]
  Large Language Models (LLMs) often struggle with inherent knowledge boundaries and hallucinations.<n>Retrieval-Augmented Generation (RAG) frequently overlooks structural interdependencies essential for multi-hop reasoning.<n>Help achieves competitive performance across multiple simple and multi-hop QA benchmarks and up to a 28.8$times$ speedup over leading Graph-based RAG baselines.
  arXiv  Detail & Related papers  (2026-02-24T14:05:29Z)
• On the Out-of-Distribution Generalization of Reasoning in Multimodal LLMs for Simple Visual Planning Tasks [56.98385132295952]
  We evaluate how well chain-of-thought approaches generalize on a simple planning task.<n>We find that reasoning traces which combine multiple text formats yield the best (and non-trivial) OOD generalization.<n> purely text-based models consistently outperform those utilizing image-based inputs.
  arXiv  Detail & Related papers  (2026-02-17T09:51:40Z)
• UniT: Unified Multimodal Chain-of-Thought Test-time Scaling [85.590774707406]
  Unified models can handle both multimodal understanding and generation within a single architecture, yet they typically operate in a single pass without iteratively refining their outputs.<n>We introduce UniT, a framework for multimodal test-time scaling that enables a single unified model to reason, verify, and refine across multiple rounds.
  arXiv  Detail & Related papers  (2026-02-12T18:59:49Z)
• Guided Verifier: Collaborative Multimodal Reasoning via Dynamic Process Supervision [11.159231524113764]
  Reinforcement Learning (RL) has emerged as a pivotal mechanism for enhancing the complex reasoning capabilities of Multimodal Large Language Models (MLLMs)<n>In this paper, we propose the textbfGuided Verifier framework to address these structural limitations.<n>We develop a specialized data synthesis pipeline targeting multimodal hallucinations, constructing textbfCoRe dataset of process-level negatives and textbfCorrect-guide textbfReasoning trajectories to train the guided verifier.
  arXiv  Detail & Related papers  (2026-02-04T07:38:42Z)
• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  Deliberative tree search is a cornerstone of Large Language Model (LLM) research.<n>This paper introduces a unified framework that deconstructs search algorithms into three core components.
  arXiv  Detail & Related papers  (2025-10-11T03:29:18Z)
• THOR: Tool-Integrated Hierarchical Optimization via RL for Mathematical Reasoning [25.605096023894834]
  Large Language Models (LLMs) have made remarkable progress in mathematical reasoning.<n>Despite recent advances, existing methods struggle with three key challenges.<n>We propose THOR (Tool-Integrated Hierarchical Optimization via RL) to overcome these limitations.<n>Our approach demonstrates strong generalization across diverse models, performing effectively in both reasoning and non-reasoning models.
  arXiv  Detail & Related papers  (2025-09-17T07:16:12Z)
• GLAD: Generalizable Tuning for Vision-Language Models [41.071911050087586]
  We propose a simpler and more general framework called GLAD (Generalizable LoRA tuning with RegulArized GraDient)<n>We show that merely applying LoRA achieves performance in downstream tasks comparable to current state-of-the-art prompt-based methods.
  arXiv  Detail & Related papers  (2025-07-17T12:58:15Z)
• Fractional Reasoning via Latent Steering Vectors Improves Inference Time Compute [60.151643048803145]
  We propose Fractional Reasoning, a framework that enables continuous control over reasoning intensity at inference time.<n>Our method operates by extracting the latent steering vector associated with deeper reasoning and reapplying it with a tunable scaling factor.<n> Experiments on GSM8K, MATH500, and GPQA demonstrate that Fractional Reasoning consistently improves performance across diverse reasoning tasks and models.
  arXiv  Detail & Related papers  (2025-06-18T21:15:59Z)
• Learning Efficient and Generalizable Graph Retriever for Knowledge-Graph Question Answering [75.12322966980003]
  Large Language Models (LLMs) have shown strong inductive reasoning ability across various domains.<n>Most existing RAG pipelines rely on unstructured text, limiting interpretability and structured reasoning.<n>Recent studies have explored integrating knowledge graphs with LLMs for knowledge graph question answering.<n>We propose RAPL, a novel framework for efficient and effective graph retrieval in KGQA.
  arXiv  Detail & Related papers  (2025-06-11T12:03:52Z)
• Optimizing Chain-of-Thought Reasoning: Tackling Arranging Bottleneck via Plan Augmentation [34.042565099565934]
  We propose a plan-based training and reasoning method that guides models to generate arranging steps through abstract plans. Results show that compared to fine-tuning directly with CoT data, our approach achieves a better performance on alleviating arranging bottleneck.
  arXiv  Detail & Related papers  (2024-10-22T08:38:50Z)
• Fine-Tuning on Diverse Reasoning Chains Drives Within-Inference CoT Refinement in LLMs [63.36637269634553]
  We introduce a novel approach where LLMs are fine-tuned to generate a sequence of Diverse Chains of Thought (DCoT) within a single inference step.<n>We show that fine-tuning on DCoT improves performance over the CoT baseline across model families and scales.<n>Our work is also significant because both quantitative analyses and manual evaluations reveal the observed gains stem from the models' ability to refine an initial reasoning chain.
  arXiv  Detail & Related papers  (2024-07-03T15:01:18Z)
• Towards interpretable-by-design deep learning algorithms [11.154826546951414]
  A proposed framework named I recasts the standard supervised classification problem into a function of similarity to a set of prototypes derived from the training data. We show that one can turn such DL models into conceptually simpler, explainable-through-prototypes ones.
  arXiv  Detail & Related papers  (2023-11-19T18:40:49Z)

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.