論文の概要: Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

• arxiv url: http://arxiv.org/abs/2512.06850v1
• Date: Sun, 07 Dec 2025 14:03:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-09 22:03:54.555131
• Title: Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
• Title（参考訳）: フロート」が高い形式:浮動小数点算術の形式的検証
• Authors: Hansa Mohanty, Vaisakh Naduvodi Viswambharan, Deepak Narayan Gadde,
• Abstract要約: 本稿では,金の基準モデルに対する直接RTL-RTLモデルによる浮動小数点演算の検証方法を提案する。 この方法論はエージェントAIベースの形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。 その結果, RTL-to-RTLモデルの直接チェックは, 適用効率が向上し, スタンドアロンの検証よりもアサーションが少なくなることがわかった。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of floating-point arithmetic remains challenging due to non-linear arithmetic behavior and the tight coupling between control and datapath logic. Existing approaches often rely on high-level C models for equivalence checking against Register Transfer Level (RTL) designs, but this introduces abstraction gaps, translation overhead, and limits scalability at the RTL level. To address these challenges, this paper presents a scalable methodology for verifying floating-point arithmetic using direct RTL-to-RTL model checking against a golden reference model. The approach adopts a divide-and conquer strategy that decomposes verification into modular stages, each captured by helper assertions and lemmas that collectively prove a main correctness theorem. Counterexample (CEX)-guided refinement is used to iteratively localize and resolve implementation defects, while targeted fault injection validates the robustness of the verification process against precision-critical datapath errors. To assess scalability and practicality, the methodology is extended with agentic AI-based formal property generation, integrating large language model (LLM)-driven automation with Human-in-the-Loop (HITL) refinement. Coverage analysis evaluates the effectiveness of the approach by comparing handwritten and AI-generated properties in both RTL-to-RTL model checking and standalone RTL verification settings. Results show that direct RTL-to-RTL model checking achieves higher coverage efficiency and requires fewer assertions than standalone verification, especially when combined with AI-generated properties refined through HITL guidance.
• Abstract（参考訳）: 浮動小数点演算の形式的検証は、非線形算術挙動と制御とデータパス論理の密結合により依然として困難である。 既存のアプローチは、レジスタ転送レベル(RTL)設計に対する等価性チェックのために高レベルのCモデルに依存することが多いが、これは抽象的なギャップ、変換オーバーヘッド、RTLレベルでのスケーラビリティの制限をもたらす。 これらの課題に対処するため、金の基準モデルに対する直接RTL-RTLモデルチェックを用いて浮動小数点演算を検証するためのスケーラブルな手法を提案する。 このアプローチでは、検証をモジュラーステージに分解する分割と征服の戦略を採用し、それぞれが主正性定理を集合的に証明するヘルパーアサーションと補題によって捕獲される。 Counterexample (CEX)-guided refinement は、実装欠陥を反復的にローカライズおよび解決するために使用され、ターゲットの障害注入は、精度クリティカルなデータパスエラーに対する検証プロセスの堅牢性を検証する。 スケーラビリティと実用性を評価するため、この方法論はエージェントAIに基づく形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。 カバレッジ解析は, RTL-to-RTLモデルチェックとスタンドアロンRTL検証設定の両方で手書きとAI生成プロパティを比較して, アプローチの有効性を評価する。 その結果、直接RTL-RTLモデル検査は、高いカバレッジ効率を実現し、特にHITLガイダンスによって改良されたAI生成特性と組み合わせた場合、スタンドアロン検証よりもアサーションを少なくすることを示した。

関連論文リスト

• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  データ駆動の不確実性スコアに基づくステップレベルの推論検証の軽量な代替案を提案する。 本研究は, LLMの内部状態が不確実性を符号化し, 信頼性の高い検証信号として機能することが示唆された。
  論文  参考訳（メタデータ） (2025-11-09T03:38:29Z)
• ORGEval: Graph-Theoretic Evaluation of LLMs in Optimization Modeling [18.8099769877788]
  ORGEvalは線形および混合整数線形プログラムの定式化における大規模言語モデルの能力を評価するためのグラフ理論評価フレームワークである。 ORGEvalはモデル等価性の検出に成功し、ランダムなパラメータ構成で100%一貫した結果が得られることを示す。 この結果から,全てのLLMにおいて最適化モデリングは依然として困難であるが,DeepSeek-V3とClaude-Opus-4は直接的プロンプト下では最高の精度を達成できることがわかった。
  論文  参考訳（メタデータ） (2025-10-31T16:35:52Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Adaptive Rectification Sampling for Test-Time Compute Scaling [10.160759436445526]
  よりきめ細かいレベルでの誤りの修正を支援するために,適応整形サンプリング(AR-Sampling)を提案する。 提案手法により, よりきめ細かいレベルでの再考が可能となり, 解の精度が向上し, 合理的な数のトークンが生成される。
  論文  参考訳（メタデータ） (2025-04-02T02:57:52Z)
• Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving [17.289776394847063]
  そこで本研究では,各ステップの中間フィードバックをループ上で行う新しい検証手法を提案する。 検証としてリーンを用いることで、ステップバイステップのローカル検証がモデルの推論精度と効率を大幅に向上させることを示す。
  論文  参考訳（メタデータ） (2025-03-12T18:20:47Z)
• Bridging Internal Probability and Self-Consistency for Effective and Efficient LLM Reasoning [53.25336975467293]
  パープレキシティや自己整合性などの手法の第一理論誤差分解解析について述べる。 パープレキシティ法は、適切な整合関数が存在しないため、かなりのモデル誤差に悩まされる。 本稿では、自己整合性とパープレキシティを統合したReasoning-Pruning Perplexity Consistency(RPC)と、低確率推論経路を排除したReasoning Pruningを提案する。
  論文  参考訳（メタデータ） (2025-02-01T18:09:49Z)
• In-context Demonstration Matters: On Prompt Optimization for Pseudo-Supervision Refinement [71.60563181678323]
  大規模言語モデル(LLM)は様々なタスクで大きな成功を収めており、生成品質をさらに向上させるためには微調整が必要である場合もある。 これらの課題に対処する直接的な解決策は、教師なしの下流タスクから高信頼のデータを生成することである。 本稿では,プロンプトと全体的な擬似スーパービジョンを両立させる新しい手法,擬似教師付きデモアライメント・アライメント・アライメント・プロンプト・最適化(PAPO)アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2024-10-04T03:39:28Z)

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

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