論文の概要: NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration

• arxiv url: http://arxiv.org/abs/2608.17304v1
• Date: Tue, 18 Aug 2026 02:58:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-19 21:40:53.190977
• Title: NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
• Title（参考訳）: NeuroAbs: プロパティチェックアクセラレーションのためのニューロシンボリックRTL抽象化フレームワーク
• Abstract要約: NeuroAbsは、RTL抽象化のための神経シンボリックなフレームワークである。 本稿では,RTL抽象化のための神経シンボリックフレームワークであるNeuroAbsを紹介する。
• 参考スコア（独自算出の注目度）: 20.480455486175952
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification is a crucial technique for ensuring the functional correctness of hardware designs. In the context of property checking, a key challenge is how to efficiently prove a user-specified property in the face of increasingly complex RTL designs. To address this challenge, abstraction techniques are often employed to reduce system complexity and accelerate the verification process. However, prior RTL abstraction methods either require significant manual effort or rely on rule-based techniques that lack flexibility. This paper introduces NeuroAbs, a neuro-symbolic framework for RTL abstraction. NeuroAbs first uses LLM-assisted RTL analysis to identify signals suitable for abstraction. It then combines LLM-based abstraction with an AST-based symbolic RTL representation to better align the generated abstraction with the intended transformation. The soundness of each abstraction is checked using satisfiability modulo theories (SMT) solving. If the abstraction is too coarse for a successful proof, NeuroAbs applies counterexample-guided abstraction refinement (CEGAR) to iteratively refine the model. Experimental results show that NeuroAbs significantly improves the efficiency of hardware property checking across a range of verification tasks.
• Abstract（参考訳）: 形式的検証はハードウェア設計の機能的正しさを保証する重要な手法である。 プロパティチェックの文脈において重要な課題は、複雑化するRTL設計に直面したユーザ指定プロパティを効率的に証明する方法である。 この課題に対処するために、システムの複雑さを減らし、検証プロセスを加速するために、しばしば抽象化技術が使用される。 しかし、以前のRTL抽象化メソッドは、かなりの手作業を必要とするか、柔軟性に欠けるルールベースの技術に依存している。 本稿では,RTL抽象化のための神経シンボリックフレームワークであるNeuroAbsを紹介する。 NeuroAbs はまず LLM 支援 RTL 解析を用いて抽象化に適した信号を特定する。 次に、LLMベースの抽象化とASTベースのシンボリックRTL表現を組み合わせることで、生成された抽象化と意図した変換をよりよく整合させる。 各抽象化の健全性は、満足度変調理論(SMT)の解法を用いて検証される。 もしこの抽象化が成功した証明には大きすぎるなら、NeuroAbs はモデルを反復的に洗練するために反例誘導抽象化洗練 (CEGAR) を適用している。 実験の結果,NeuroAbsは様々な検証タスクにおいてハードウェア特性チェックの効率を著しく向上させることがわかった。

関連論文リスト

• A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation [59.98516959731531]
  抽象推論能力は、抽象ルールを抽出し適用するためのLLMの知性と能力を反映する。 既存のベンチマークは、高価な手作業のアノテーション、そのスケールの制限、あるいは真の推論ではなく暗記のリスク測定に頼っている。 我々はA2RBenchという名の自動パイプラインを導入し、生成、拡張、評価、分析を行う。
  論文  参考訳（メタデータ） (2026-05-17T06:14:20Z)
• RLAD: Training LLMs to Discover Abstractions for Solving Reasoning Problems [98.98963933669751]
  問題が発生したら、複数の抽象化を提案できるモデルをトレーニングし、続いてソリューション構築のインセンティブを与えるRLを作ります。 この結果、RLトレーニングパラダイムはRLADと呼ばれ、抽象化ジェネレータとソリューションジェネレータを共同で訓練する。 我々は、大規模なテスト予算で多くのソリューションを生成するよりも、より多くのテスト時間計算を抽象化の生成に割り当てることが、パフォーマンスに有益であることを示しています。
  論文  参考訳（メタデータ） (2025-10-02T17:44:23Z)
• Structural Abstraction and Selective Refinement for Formal Verification [0.5735035463793008]
  ロボットアプリケーションの安全性検証は、ロボットが通常操作する環境の複雑さのため、非常に難しい。 通常のソリューションアプローチは抽象化であり、より正確に振る舞いの抽象化です。 そこで我々は,ロボット環境のボクセル表現の文脈において,構造的抽象化を提案する。
  論文  参考訳（メタデータ） (2025-05-29T01:44:47Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [30.938876549335067]
  本稿では,新しいニューロン-シンボリックRTL最適化フレームワークであるSymRTLOを提案する。 有限状態機械(FSM)論理の解析と最適化のための記号モジュールを提案する。 Synopsys Design Compiler と Yosys による RTL-Rewriter ベンチマークの実験では、SymRTLO は 43.9% と 62.5% と 51.1% に向上している。
  論文  参考訳（メタデータ） (2025-04-14T16:15:55Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• AbsInstruct: Eliciting Abstraction Ability from LLMs through Explanation Tuning with Plausibility Estimation [60.40409210088717]
  抽象化能力は人間の知性において不可欠であり、NLP研究における様々なタスクにも有用である。 既存の研究によると、LLMは抽象能力に欠けており、その改善方法はまだ解明されていない。 本稿では,命令チューニングによるLLMの抽象化能力を向上するフレームワークAbsInstructを設計する。
  論文  参考訳（メタデータ） (2024-02-16T12:47:11Z)
• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  ニューラル抽象化は、最近、複雑な非線形力学モデルの形式近似として導入されている。 我々は形式的帰納的合成法を用いて、これらのセマンティクスを用いた動的モデルをもたらすニューラル抽象化を生成する。
  論文  参考訳（メタデータ） (2023-07-28T13:22:32Z)
• Learning Dynamic Abstract Representations for Sample-Efficient Reinforcement Learning [22.25237742815589]
  多くの現実世界の問題において、学習エージェントは問題の抽象化と解決策を同時に学ぶ必要がある。 本稿では,強化学習を行いながら状態抽象化を構築するための新しいトップダウン手法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T23:05:43Z)
• Residual Reinforcement Learning from Demonstrations [51.56457466788513]
  報酬信号の最大化のために,従来のフィードバックコントローラからの制御動作を適用することで,ロボット作業の課題を解決する手段として,残留強化学習(Residual reinforcement learning, RL)が提案されている。 視覚的インプットから学習するための残差定式化を拡張し,実演を用いて報酬をスパースする。 6-DoFのUR5アームと28-DoFのデキスタラスハンドのシミュレーション操作に関する実験的評価は、デモからの残留RLが、行動クローニングやRL微調整よりも柔軟に、見えない環境条件に一般化できることを実証している。
  論文  参考訳（メタデータ） (2021-06-15T11:16:49Z)

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

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