論文の概要: SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation

• arxiv url: http://arxiv.org/abs/2605.25181v1
• Date: Sun, 24 May 2026 17:22:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-26 19:50:18.949169
• Title: SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation
• Title（参考訳）: SpecAlign: SystemVerilog Assertion生成のためのセマンティックアライメントフレームワーク
• Authors: Jaime Rafael Imperial, Hao Zheng,
• Abstract要約: SpecAlignはSystemVerilog Assertionのセマンティック評価と洗練のためのフレームワークである。 我々は,SpecAlignが意味的不整合を効果的に検出し,黄金のRTLに頼ることなくアサーションアライメントを改善することを示す。
• 参考スコア（独自算出の注目度）: 6.0174402828965725
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Existing Large Language Model (LLM) approaches to SystemVerilog Assertion (SVA) generation primarily focus on syntactic validity and formal verification outcomes, while semantic alignment between generated assertions and natural language specifications remains difficult to quantify. As a result, hallucinated or misaligned SVAs can reduce confidence and increase debugging efforts in the absence of golden RTL. This paper presents SpecAlign, a framework for semantic evaluation and refinement of LLM-generated SVAs. SpecAlign introduces two iterative alignment loops that assess both natural language properties and SVAs against the design specification using entailment-based classification. We improve alignment decisions by generating multiple reasoning paths using chain-of-thought prompting and aggregating them via a self-consistency voting mechanism. Misaligned assertions are analyzed to generate actionable feedback for refinement. We further define a quantitative alignment score to measure semantic consistency across iterations. Experimental results demonstrate that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL, providing a scalable complement to traditional formal verification evaluation metrics.
• Abstract（参考訳）: 既存のLarge Language Model (LLM) の SystemVerilog Assertion (SVA) 生成へのアプローチは主に構文的妥当性と形式的検証結果に重点を置いているが、生成したアサーションと自然言語仕様とのセマンティックアライメントは定量化が難しい。 その結果、幻覚性または不整合性SVAは、ゴールデンRTLが欠如している場合に、信頼性を低下させ、デバッグの労力を増大させることができる。 本稿では,LLM生成SVAのセマンティック評価と改良のためのフレームワークであるSpecAlignを提案する。 SpecAlignは2つの反復的なアライメントループを導入し、自然言語特性とSVAの両方をentailment-based classificationを使って設計仕様に対して評価する。 自己整合性投票機構を用いて、チェーン・オブ・ソート・プロンプトを用いて複数の推論経路を生成し、アライメント決定を改善する。 ミスアサーションを分析して、改善のための実用的なフィードバックを生成する。 さらに、イテレーション間のセマンティック一貫性を測定するための定量的アライメントスコアを定義します。 実験の結果,SpecAlignは黄金のRTLに頼ることなく意味的不整合を効果的に検出し,アサーションアライメントを改善し,従来の形式的検証評価指標をスケーラブルに補完することを示した。

関連論文リスト

• Reward-Guided Semantic Evolution for Test-time Adaptive Object Detection [82.2968697030677]
  Grounding DINOのような視覚言語モデル(VLM)を用いたオープン語彙オブジェクト検出は、テスト時間分布シフト時の性能劣化に悩まされる。 Reward-Guided Semantic Evolution (RGSE) は、テスト時にテキストの埋め込みを直接洗練するトレーニング不要のフレームワークである。
  論文  参考訳（メタデータ） (2026-05-06T06:17:41Z)
• FACTOR: Counterfactual Training-Free Test-Time Adaptation for Open-Vocabulary Object Detection [63.91351553178842]
  FACTORはオープン語彙オブジェクト検出のためのトレーニング不要なテスト時間適応である。 属性依存性の予測を選択的に抑制するために、属性の感度、意味的関連性、予測のバリエーションを定量化する。 PASCAL-C, COCO-C, FoggyCityscapes の実験では、FACTOR が従来の TTA 法より一貫して優れていたことが示されている。
  論文  参考訳（メタデータ） (2026-05-05T02:31:18Z)
• From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
  SystemVerilog Assertions (SVA) はデジタルハードウェアの正式な検証に不可欠である。 近年,大規模言語モデル(LLM)を用いてSVA生成を自動化する手法が研究されている。 本稿では,自然言語仕様からSVAを生成するツール拡張ReActエージェントProofLoopを提案する。
  論文  参考訳（メタデータ） (2026-04-25T01:46:33Z)
• SCALE: Semantic- and Confidence-Aware Conditional Variational Autoencoder for Zero-shot Skeleton-based Action Recognition [4.853241666510524]
  ゼロショットスケルトンに基づくアクション認識(ZSAR)は、これらのクラスからのトレーニングスケルトンなしでアクションクラスを認識することを目的としている。 本稿では,ZSARをクラス条件エネルギーランキングとして定式化する,軽量で決定論的セマンティックなセマンティック・アンド・信頼を意識したエネルギーベースフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-04-02T16:12:42Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  本稿では,大規模言語モデルとSMTソルバを組み合わせたニューロシンボリック・フレームワークを提案する。 本稿では,(1)形式的意味的等価性チェックによるマルチモデルコンセンサス,(2)適切な検証戦略に異なるクレーム型を指示するセマンティックルーティング,(3)最小補正サブセットによる正確な論理的エラーローカライゼーション,の3点を紹介する。 GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
  論文  参考訳（メタデータ） (2026-01-27T20:59:11Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。 AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。 このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
  論文  参考訳（メタデータ） (2025-07-14T14:43:14Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• Likelihood-Aware Semantic Alignment for Full-Spectrum Out-of-Distribution Detection [24.145060992747077]
  画像とテキストの対応を意味的に高次領域に促進する「Likelihood-Aware Semantic Alignment (LSA)フレームワーク」を提案する。 2つのF-OODベンチマークで15.26%$と18.88%$の差で既存の手法を上回り、提案したLSAの優れたOOD検出性能を実証した。
  論文  参考訳（メタデータ） (2023-12-04T08:53:59Z)

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

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