論文の概要: Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations

• arxiv url: http://arxiv.org/abs/2609.05658v1
• Date: Fri, 04 Sep 2026 18:41:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-10 19:44:08.103974
• Title: Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations
• Title（参考訳）: セマンティックス保存RTL変換に対するLLM生成系Verilogアサーションのロバスト性
• Abstract要約: 大規模言語モデル(LLM)は、SystemVerilog Assertion(SVA)の自動生成のために、ますます研究されている。 ほとんどの評価では、入力の単一の構文表現に正確さを報告している。 そのような点の精度は、モデルの正しい出力が同じRTLの振る舞いが異なる場合に安定であるかどうかを明らかにしない。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) are increasingly being explored for automating SystemVerilog Assertion (SVA) generation, yet most evaluations report correctness on a single syntactic representation of an input. Such point accuracy does not reveal whether a model's correct output is stable when the same RTL behavior is written differently. This paper presents a controlled metamorphic evaluation of LLM-based SVA generation under semantics-preserving RTL transformations. Starting from the VERT dataset, we construct a quality-filtered conditional-control pool and a stratified 40-program evaluation set containing 295 assignment behaviors. We evaluate two open code models, Qwen2.5-Coder-7B and DeepSeek-Coder-V2-Lite, with an identical evaluation prompt and greedy decoding. Three transformations are studied: operand reordering, deterministic identifier renaming, and redundant parenthesization. Beyond baseline and transformed accuracy, we measure conditional robustness, invariance failure, and any-flip rate, with 10,000-sample clustered bootstrap intervals at the RTL-program level. Across all six model-transformation conditions, 9.7%-27.0% of behaviors that were correct on the original RTL become incorrect after a semantics-preserving transformation. Aggregate accuracy can therefore hide substantial instability: under identifier renaming, DeepSeek-Coder-V2-Lite improves from 53.9% to 63.7% accuracy while 19.5% of its originally correct behaviors fail. Manual review of 30 sampled correct-to-wrong transitions identifies dropped path predicates, branch-polarity errors, Boolean-structure corruption, and output-contract violations. The results show that point accuracy alone is insufficient for characterizing LLM reliability in assertion generation and motivate robustness-aware evaluation for AI-assisted hardware verification.
• Abstract（参考訳）: 大規模言語モデル (LLMs) はSystemVerilog Assertion (SVA) 生成の自動化のためにますます研究されているが、ほとんどの評価では入力の単一の構文表現に対して正確性を報告している。 そのような点の精度は、モデルの正しい出力が同じRTLの振る舞いが異なる場合に安定であるかどうかを明らかにしない。 本稿では,LLMに基づくSVA生成のセマンティクス保存RTL変換における制御されたメタモルフィック評価について述べる。 VERTデータセットから、品質フィルタ付き条件制御プールと、295の割当て動作を含む階層化された40プログラム評価セットを構築する。 我々は、Qwen2.5-Coder-7BとDeepSeek-Coder-V2-Liteの2つのオープンコードモデルを評価する。 オペランド・リオーダー、決定論的識別子・リネーム、冗長な括弧化の3つの変換が研究されている。 ベースラインと変換精度の他に、RTLプログラムレベルで1万サンプルのクラスタリングブートストラップ間隔で条件付きロバスト性、不分散故障、および任意のフリップ速度を測定する。 6つのモデル変換条件全体で、元のRTLで正しい行動の9.7%-27.0%は意味論的保存変換後に誤りとなる。 識別子のリネームの下では、DeepSeek-Coder-V2-Liteは53.9%から63.7%に改善され、19.5%の本来の正しい動作は失敗する。 30個の正解遷移のマニュアルレビューでは、減少経路述語、分岐極性誤差、ブール構造破損、出力-契約違反が特定されている。 その結果、点精度だけではアサーション生成におけるLCMの信頼性を特徴づけるには不十分であり、AI支援ハードウェア検証のためのロバストネス・アウェア評価を動機付けていることがわかった。

関連論文リスト

• Semantic Drift in Bug Resolution: How Behavioral Signals Propagate from Reports to Tests and Patches [18.727291516223115]
  Desc2Fixは、バグレポートのセマンティックアライメント、テストのトリガー、開発者による修正を測定するフレームワークである。 GPT-4o と DeepSeek-Chat を用いて,Defects4J と SWT-Bench の2,857 個のレポート・パッチを解析した。
  論文  参考訳（メタデータ） (2026-07-20T22:32:23Z)
• LLM-as-a-Verifier: A General-Purpose Verification Framework [74.40111651545979]
  本稿では,汎用検証フレームワーク LLM-as-a-Verifier を紹介する。 追加のトレーニングを必要とせずに、エージェントタスクに対してきめ細かいフィードバックを提供する。 いくつかのベンチマークで最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-07-06T17:59:35Z)
• Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
  コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。 この問題は、事前評価が結果駆動である変換において特に深刻である。 ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。 このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
  論文  参考訳（メタデータ） (2026-05-27T19:57:15Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Correct Answers from Sound Reasoning: Verifiable Process Supervision for Language Models [94.68358825189738]
  本稿では,予測精度と推論品質を協調的に最適化する検証済み領域の学習後フレームワークを提案する。 我々は,エンジン信号に対して推論ステップを確定的に検証できる制御テストベッドであるチェスのVPSを評価する。 VPSは、推論品質を著しく向上させながら精度を保ち、勝利率エラーを最大30%削減し、一貫性をほぼ飽和状態に回復する。
  論文  参考訳（メタデータ） (2026-04-03T15:19:46Z)
• ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
  大規模言語モデル(LLM)は、自然言語を最適化コードに変換することができるが、サイレント障害は重大なリスクをもたらす。 2つの相補的な方向からサイレント障害に対処するReLoopを紹介します。
  論文  参考訳（メタデータ） (2026-02-17T20:20:33Z)
• FidelityGPT: Correcting Decompilation Distortions with Retrieval Augmented Generation [23.291593625603653]
  逆コンパイルはマシンコードを可読形式に変換し、ソースコードなしで解析とデバッグを可能にする。 変数のリネームや構造的単純化といった既存の手法は部分的な改善を提供するが、堅牢な検出と修正は欠如している。 本稿では,意味的歪みを系統的に検出し,修正することにより,デコンパイルされたコード精度と可読性を向上するフレームワークであるFidelityGPTを提案する。
  論文  参考訳（メタデータ） (2025-10-22T14:11:44Z)
• SemGuard: Real-Time Semantic Evaluator for Correcting LLM-Generated Code [46.20378145112059]
  ポストホック修復パイプラインは、実行後にのみそのような障害を検出する。 本稿では,実時間で行レベルのセマンティック監視を行うセマンティック評価フレームワークSemGuardを紹介する。
  論文  参考訳（メタデータ） (2025-09-29T09:21:32Z)
• Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
  本稿では,22の大規模C/C++プロジェクトから得られた関数レベル修正の信頼性の高いベンチマークであるReDefを紹介する。 欠陥ケースはコミットの反転によって固定され、クリーンケースはポストホック履歴チェックによって検証される。 このパイプラインは3,164の欠陥と10,268のクリーンな修正をもたらし、既存のリソースよりも信頼性の高いラベルを提供する。
  論文  参考訳（メタデータ） (2025-09-11T07:07:11Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。 このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。 19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• Tail-to-Tail Non-Autoregressive Sequence Prediction for Chinese Grammatical Error Correction [49.25830718574892]
  本稿では,Tail-to-Tail (textbfTtT) という新しいフレームワークを提案する。 ほとんどのトークンが正しいので、ソースからターゲットに直接転送でき、エラー位置を推定して修正することができる。 標準データセット、特に可変長データセットに関する実験結果は、文レベルの精度、精度、リコール、F1-Measureの観点からTtTの有効性を示す。
  論文  参考訳（メタデータ） (2021-06-03T05:56:57Z)

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

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