論文の概要: FVRuleLearner: Operator-Level Reasoning Tree (OP-Tree)-Based Rules Learning for Formal Verification

• arxiv url: http://arxiv.org/abs/2604.03245v1
• Date: Fri, 06 Mar 2026 21:41:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-12 18:41:08.540261
• Title: FVRuleLearner: Operator-Level Reasoning Tree (OP-Tree)-Based Rules Learning for Formal Verification
• Title（参考訳）: FVRuleLearner: 形式検証のための演算子レベル推論木(OP-Tree)に基づくルール学習
• Authors: Lily Jiaxin Wan, Chia-Tung Ho, Yunsheng Bai, Cunxi Yu, Deming Chen, Haoxing Ren,
• Abstract要約: 我々は,新しい演算子推論木(OP-Tree)上に構築された演算子レベルルール(Op-Rule)学習フレームワークであるFVRuleLearnerを紹介する。 提案されたFVRuleLearnerは、構文の正しさが3.95%向上し、関数の正しさが31.17%向上した。
• 参考スコア（独自算出の注目度）: 15.777696568084066
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The remarkable reasoning and code generation capabilities of large language models (LLMs) have recently motivated increasing interest in automating formal verification (FV), a process that ensures hardware correctness through mathematically precise assertions but remains highly labor-intensive, particularly through the translation of natural language into SystemVerilog Assertions (NL-to-SVA). However, LLMs still struggle with SVA generation due to limited training data and the intrinsic complexity of FV operators. Consequently, a more efficient and robust methodology for ensuring correct SVA operator selection is essential for producing functionally correct assertions. To address these challenges, we introduce FVRuleLearner, an Operator-Level Rule (Op-Rule) learning framework built on a novel Operator Reasoning Tree (OP-Tree), which models SVA generation as structured, interpretable reasoning. FVRuleLearner operates in two complementary phases: (1) Training: it constructs OP-Tree that decomposes NL-to-SVA alignment into fine-grained, operator-aware questions, combining reasoning paths that lead to correct assertions; and (2) Testing: it performs operator-aligned retrieval to fetch relevant reasoning traces from the learned OP-Tree and generate new rules for unseen specifications. In the comprehensive studies, the proposed FVRuleLearner outperforms the state-of-the-art baseline by 3.95% in syntax correctness and by 31.17% in functional correctness on average. Moreover, FVRuleLearner successfully reduces an average of 70.33% of SVA functional failures across diverse operator categories through a functional taxonomy analysis, showing the effectiveness of applying learned OP-Tree to the Op-Rule generations for unseen NL-to-SVA tasks. These results establish FVRuleLearner as a new paradigm for domain-specific reasoning and rule learning in formal verification.
• Abstract（参考訳）: 大規模言語モデル(LLM)の顕著な推論とコード生成能力は、数学的に正確なアサーションを通じてハードウェアの正当性を保証するプロセスであるフォーマル検証(FV)の自動化への関心の高まりを動機付けている。 しかし、LLMは、限られたトレーニングデータとFV演算子の本質的な複雑さのために、SVA生成に苦戦している。 したがって、機能的に正しいアサーションを生成するためには、正しいSVA演算子選択を保証するためのより効率的で堅牢な方法論が不可欠である。 これらの課題に対処するために、我々は、SVA生成を構造化、解釈可能な推論としてモデル化する新しい演算子推論ツリー(OP-Tree)上に構築された演算子レベルルール(Op-Rule)学習フレームワークであるFVRuleLearnerを紹介した。 FVRuleLearnerは,(1)NL-to-SVAアライメントを細粒度に分解したOP-Treeを構築し,正しいアサーションにつながる推論経路を組み合わせ,(2)テスト: 学習したOP-Treeから関連する推論トレースを取得して,未知の仕様の新しいルールを生成する。 包括的な研究において、提案されたFVRuleLearnerは、構文の正しさが3.95%、関数の正しさが31.17%向上した。 さらに、FVRuleLearnerは、機能分類分析により、さまざまなオペレータカテゴリにわたるSVA機能障害の平均70.33%を削減し、未知のNL-to-SVAタスクに対して、OP-TreeをOp-Rule世代に適用する効果を示した。 これらの結果は、FVRuleLearnerを、形式検証におけるドメイン固有の推論とルール学習の新しいパラダイムとして確立する。

関連論文リスト

• Learning to Disentangle Latent Reasoning Rules with Language VAEs: A Systematic Study [37.52166353495979]
  本研究は,推論規則を言語モデル内に明示的に組み込んで記憶する方法について検討する。 本稿では,Transformer ベースの言語 VAE における推論規則を学習するための完全なパイプラインを提案する。
  論文  参考訳（メタデータ） (2025-06-24T08:38:03Z)
• TreeLoRA: Efficient Continual Learning via Layer-Wise LoRAs Guided by a Hierarchical Gradient-Similarity Tree [52.44403214958304]
  本稿では階層的な勾配の類似性を利用して階層型アダプタを構築する新しい手法であるTreeLoRAを紹介する。 タスク類似度推定の計算負担を軽減するために,より低い信頼度境界に基づくアルゴリズムを開発するために,バンド手法を用いる。 視覚変換器 (ViTs) と大規模言語モデル (LLMs) の両方を用いた実験により, 提案手法の有効性と有効性を示す。
  論文  参考訳（メタデータ） (2025-06-12T05:25:35Z)
• Sneaking Syntax into Transformer Language Models with Tree Regularization [33.74552367356904]
  構文的帰納バイアスの導入は、トランスフォーマー言語モデルにおけるより堅牢でデータ効率のよい学習を解放する可能性がある。 ここでは,銀パースからの括弧決定を微分可能性制約の集合に変換する補助的損失関数であるTreeRegを紹介する。 TreeRegは標準のLM目標とシームレスに統合され、アーキテクチャの変更は不要である。
  論文  参考訳（メタデータ） (2024-11-28T03:27:48Z)
• Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting [0.0]
  高品質なシステムVerilog Assertions (SVA) を自動生成する大規模言語モデル(LLM)に基づくフローを提案する。 サブタスクに着目したファインチューニング手法を導入し,機能的に正しいアサーションの数を7.3倍に増やした。 実験では、このアプローチを使って構文エラーのないアサーション数が26%増加した。
  論文  参考訳（メタデータ） (2024-11-23T03:52:32Z)
• Inherently Interpretable Tree Ensemble Learning [7.868733904112288]
  浅い決定木をベース学習として使用すると、アンサンブル学習アルゴリズムが本質的に解釈可能であることを示す。 木アンサンブルを固有の解釈可能性を持つ機能的ANOVA表現に変換する解釈アルゴリズムを開発した。 シミュレーションと実世界のデータセットを用いた実験により,提案手法はモデル解釈と予測性能のトレードオフを良くすることを示した。
  論文  参考訳（メタデータ） (2024-10-24T18:58:41Z)
• Optimized Feature Generation for Tabular Data via LLMs with Decision Tree Reasoning [53.241569810013836]
  本稿では,大規模言語モデル(LLM)を用いて,効率的な特徴生成ルールを同定するフレームワークを提案する。 我々は、自然言語で容易に表現できるため、この推論情報を伝達するために決定木を使用します。 OCTreeは様々なベンチマークで様々な予測モデルの性能を継続的に向上させる。
  論文  参考訳（メタデータ） (2024-06-12T08:31:34Z)
• Prompt Optimization via Adversarial In-Context Learning [51.18075178593142]
  adv-ICLは、ジェネレータとディスクリミネータの間の2プレイヤーゲームとして実装される。 ジェネレータは、判別器を騙すのに十分な出力を生成する。 本稿では,Adv-ICLが最先端のプロンプト最適化技術を大幅に改善することを示す。
  論文  参考訳（メタデータ） (2023-12-05T09:44:45Z)
• Improved Algorithms for Neural Active Learning [74.89097665112621]
  非パラメトリックストリーミング設定のためのニューラルネットワーク(NN)ベースの能動学習アルゴリズムの理論的および経験的性能を改善する。 本研究では,SOTA(State-of-the-art (State-the-art)) 関連研究で使用されるものよりも,アクティブラーニングに適する人口減少を最小化することにより,2つの後悔の指標を導入する。
  論文  参考訳（メタデータ） (2022-10-02T05:03:38Z)

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

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