論文の概要: LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking

• arxiv url: http://arxiv.org/abs/2602.24010v1
• Date: Fri, 27 Feb 2026 13:34:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-02 19:48:24.447789
• Title: LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
• Title（参考訳）: LeGend: ハードウェアモデルチェックにおけるLemma生成のためのデータ駆動フレームワーク
• Authors: Mingkai Miao, Guangyu Hu, Wei Zhang, Hongce Zhang,
• Abstract要約: RTL設計のプロパティチェックは、形式的検証における中心的なタスクである。 グラフ解析のパラダイムを1回に1度のグローバル表現学習に置き換えたLeGendを紹介する。 実験の結果、LeGendは様々なベンチマークで2つの最先端のIC3/PDRエンジンを加速している。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: RTL設計のプロパティチェックは、形式的検証における中心的なタスクである。 利用可能なエンジンのうち、IC3/PDRは、インダクティブな一般化(CTI立方体を補題に一般化するステップ)に批判的に依存する性能を持つ広く使われているバックボーンである。 それまでの作業では、このステップをガイドし、奨励的な結果を達成するためにマシンラーニングを調査してきたが、ほとんどのメソッドでは、グラフ毎のグラフ分析パラダイムを採用していた。 本稿では,このパラダイムを1回のグローバル表現学習に置き換えるLeGendを紹介する。 LeGendは、グローバル回路特性をキャプチャするラッチ埋め込みを生成するために、ドメイン適応型の自己教師付きモデルを事前訓練する。 これらの事前計算された埋め込みは、軽量モデルで無視できるオーバーヘッドで高品質のレムマを予測し、高速な推論から高価な学習を効果的に分離することを可能にする。 実験の結果、LeGendは2つの最先端のIC3/PDRエンジンを様々なベンチマークで加速し、形式的検証をスケールアップする有望な方法を示している。

関連論文リスト

• HELP: HyperNode Expansion and Logical Path-Guided Evidence Localization for Accurate and Efficient GraphRAG [53.30561659838455]
  大きな言語モデル(LLM)は、しばしば固有の知識境界と幻覚に苦しむ。 Retrieval-Augmented Generation (RAG) は、マルチホップ推論に不可欠な構造的相互依存性をしばしば見落としている。 ヘルプは、複数の単純でマルチホップなQAベンチマークで競合性能を達成し、グラフベースのRAGベースラインよりも28.8$times$のスピードアップを実現している。
  論文  参考訳（メタデータ） (2026-02-24T14:05:29Z)
• On the Out-of-Distribution Generalization of Reasoning in Multimodal LLMs for Simple Visual Planning Tasks [56.98385132295952]
  簡単な計画課題において,チェーン・オブ・ソート・アプローチがいかに一般化するかを評価する。 複数のテキスト形式を組み合わせた推論トレースが、最高の(かつ非自明な)OOD一般化をもたらすことが分かりました。 純粋にテキストベースのモデルは、画像ベースの入力を利用するモデルよりも一貫して優れています。
  論文  参考訳（メタデータ） (2026-02-17T09:51:40Z)
• UniT: Unified Multimodal Chain-of-Thought Test-time Scaling [85.590774707406]
  統一モデルは単一のアーキテクチャ内でマルチモーダル理解と生成の両方を扱うことができるが、通常は出力を反復的に書き換えることなく単一のパスで操作する。 マルチモーダルなテストタイムスケーリングのためのフレームワークであるUniTを導入し、単一の統一モデルで複数のラウンドをまたいだ推論、検証、精査を可能にします。
  論文  参考訳（メタデータ） (2026-02-12T18:59:49Z)
• Guided Verifier: Collaborative Multimodal Reasoning via Dynamic Process Supervision [11.159231524113764]
  マルチモーダル大規模言語モデル(MLLM)の複雑な推論能力を高めるための重要なメカニズムとして強化学習(RL)が登場した。 本稿では,これらの構造的制約に対処する textbfGuided Verifier フレームワークを提案する。 我々は,マルチモーダル幻覚をターゲットとした特殊なデータ合成パイプラインを開発し,プロセスレベルの負の textbfCoRe データセットとtextbfCorrect-guide textbfReasoning トラジェクトリを構築し,ガイド付き検証器を訓練する。
  論文  参考訳（メタデータ） (2026-02-04T07:38:42Z)
• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  線形木探索はLarge Language Model (LLM) 研究の基盤となっている。 本稿では,検索アルゴリズムを3つのコアコンポーネントに分解する統合フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-11T03:29:18Z)
• THOR: Tool-Integrated Hierarchical Optimization via RL for Mathematical Reasoning [25.605096023894834]
  大規模言語モデル (LLM) は数学的推論において顕著な進歩を遂げた。 最近の進歩にもかかわらず、既存の手法は3つの重要な課題に直面している。 我々はこれらの制限を克服するためにTHOR(Tool-Integrated Hierarchical Optimization via RL)を提案する。 提案手法は多種多様なモデルに対して強い一般化を示し,推論モデルと非推論モデルの両方で効果的に機能する。
  論文  参考訳（メタデータ） (2025-09-17T07:16:12Z)
• GLAD: Generalizable Tuning for Vision-Language Models [41.071911050087586]
  GLAD (Generalizable LoRA tuning with RegulArized GraDient) という,よりシンプルで汎用的なフレームワークを提案する。 我々は,LoRAを適用するだけで,現在の最先端のプロンプトベースの手法に匹敵するダウンストリームタスクのパフォーマンスが得られることを示す。
  論文  参考訳（メタデータ） (2025-07-17T12:58:15Z)
• Fractional Reasoning via Latent Steering Vectors Improves Inference Time Compute [60.151643048803145]
  本稿では,推論時の推論強度を連続的に制御するフレームワークであるフラクショナル推論を提案する。 提案手法は, より深い推論を伴う潜在ステアリングベクトルを抽出し, 調整可能なスケーリング係数で再適用することによって機能する。 GSM8K、MATH500、GPQAの実験により、フラクショナル推論は様々な推論タスクやモデルのパフォーマンスを一貫して改善することを示した。
  論文  参考訳（メタデータ） (2025-06-18T21:15:59Z)
• Learning Efficient and Generalizable Graph Retriever for Knowledge-Graph Question Answering [75.12322966980003]
  大規模言語モデル(LLM)は、様々な領域にわたって強い帰納的推論能力を示している。 既存のRAGパイプラインのほとんどは非構造化テキストに依存しており、解釈可能性と構造化推論を制限する。 近年,知識グラフ解答のための知識グラフとLLMの統合について検討している。 KGQAにおける効率的なグラフ検索のための新しいフレームワークであるRAPLを提案する。
  論文  参考訳（メタデータ） (2025-06-11T12:03:52Z)
• Optimizing Chain-of-Thought Reasoning: Tackling Arranging Bottleneck via Plan Augmentation [34.042565099565934]
  そこで本研究では,抽象的な計画を通じてモデルを整理し,構成ステップを生成するための計画ベーストレーニングと推論手法を提案する。 その結果,CoTデータを直接微調整した場合と比較して,ボトルネックの緩和に優れた性能が得られた。
  論文  参考訳（メタデータ） (2024-10-22T08:38:50Z)
• Fine-Tuning on Diverse Reasoning Chains Drives Within-Inference CoT Refinement in LLMs [63.36637269634553]
  本稿では,LLMを微調整し,一つの推論ステップで思考の逆連鎖(DCoT)を生成する手法を提案する。 DCoTの微調整により,モデルファミリおよびスケール間のCoTベースライン上での性能が向上することを示す。 我々の研究は、定量的解析と手動評価の両方で、観測された利益は、最初の推論連鎖を洗練させるモデルの能力に由来することを明らかにしているため、重要である。
  論文  参考訳（メタデータ） (2024-07-03T15:01:18Z)
• Towards interpretable-by-design deep learning algorithms [11.154826546951414]
  I という名前のフレームワークは、標準教師付き分類問題をトレーニングデータから派生したプロトタイプのセットに類似した関数に再キャストする。 本稿では,そのようなDLモデルを概念的にシンプルで説明可能なプロトタイプモデルにすることができることを示す。
  論文  参考訳（メタデータ） (2023-11-19T18:40:49Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。