論文の概要: FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection

• arxiv url: http://arxiv.org/abs/2609.07492v1
• Date: Mon, 07 Sep 2026 13:41:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-12 00:15:16.831885
• Title: FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
• Title（参考訳）: FPScan:浮動小数点異常検出のための自動拘束型アナライザ
• Abstract要約: FPScanは、浮動小数点プログラムにおける破滅的なキャンセルと吸収を正式に定義し、検出する新しいツールである。 提案手法は,プログラム変数の順序を推測する抽象的な解釈に基づいて,独自の静的解析器から始める。 オフザシェルフSMTソルバは、プログラムがこれらの重要な数値的な落とし穴のどれかを示すかどうかを決定するために使用される。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.
• Abstract（参考訳）: エラーのない浮動小数点プログラムを書くことは、特に数値解析やラウンドエラーの伝播に強い背景を持たないプログラマにとって、難しい課題である。 最先端技術は通常、静的または動的解析を用いてそのようなエラーをバウンドすることを目的としている。 しかし、吸収や破滅的なキャンセルといった重要な浮動小数点の落とし穴に明示的に対処するツールはほとんどない。 これらの異常は、ラウンドエラーが著しく増幅された状況を表しており、有限精度計算のセマンティクスは実数意味論から大きく逸脱する。 本稿では,浮動小数点プログラムにおける破滅的キャンセルと吸収の両方を正式に定義し,検出する新しいツールであるFPScanを提案する。 提案手法は,プログラム変数の順序を推測する抽象的な解釈に基づいて,独自の静的解析器から始める。 この等級情報は、エラーの伝播とプログラム内の数値精度をモデル化する一階制約のセットを構築するために使用される。 最後に,本プログラムがこれらの重要な数値落とし穴を示すか否かを判断するために,既製のSMTソルバを用いる。 浮動小数点プログラムのベンチマークスイートであるFPBenchを用いて,ツールの有効性を評価する実験を行った。 また,音質・分析時間に関する最先端のツールとの比較を行った。

関連論文リスト

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Revisiting Code Debloating with Ground Truth-based Evaluation [5.955975465516521]
  プログラムデブロは、パフォーマンスオーバーヘッド、アタックサーフェス、メンテナンスコストを削減するために、未使用のコードを削除することを目的としている。 その中心的な役割にもかかわらず、アプリケーションレベルのデブロは、パフォーマンスを測定するために不完全なプロキシに依存し続けている。 我々は,地道な評価パラダイムを通じて,アプリケーションレベルのデブロ化の基礎を再考する。
  論文  参考訳（メタデータ） (2026-04-20T01:58:17Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• Computing Floating-Point Errors by Injecting Perturbations [10.580959733598519]
  浮動小数点プログラムは近代科学と工学の基礎を形成する。 浮動小数点誤差は広く存在するが、浮動小数点プログラムにおいて重大なエラーを引き起こすのは入力のサブセットのみである。 本稿では,浮動小数点誤差を効果的かつ効率的に計算するためのPI検出器を提案する。
  論文  参考訳（メタデータ） (2025-07-11T10:19:14Z)
• Understanding and Mitigating Numerical Sources of Nondeterminism in LLM Inference [31.2331188304598]
  評価バッチサイズ、GPUカウント、GPUバージョンなどのシステム構成の変更は、生成されたレスポンスに大きな違いをもたらす可能性がある。 この変数の根本原因は、限定的な数値精度で浮動小数点算術の非連想性に遡る。 そこで我々は16ビットの精度で重みを格納するが、FP32では全ての計算を実行する軽量な推論パイプラインLayerCastを開発した。
  論文  参考訳（メタデータ） (2025-06-11T08:23:53Z)
• Satire: Computing Rigorous Bounds for Floating-Point Rounding Error in Mixed-Precision Loop-Free Programs [0.0]
  Satireは、設計者が分析時間内でエラーバウンド・タイネスを利得と交換できるツールだ。 風刺は、厳密な経験的エラー保証によって導かれる設計上のトレードオフに、数値ルーチンの設計で使用することができる。
  論文  参考訳（メタデータ） (2025-03-07T20:46:38Z)
• Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
  凸最適化問題を解くための新しい勾配のないアルゴリズムを提案する。 このような問題は医学、物理学、機械学習で発生する。 両種類の雑音下で提案アルゴリズムの収束保証を行う。
  論文  参考訳（メタデータ） (2024-11-21T10:26:17Z)
• An evaluation framework for dimensionality reduction through sectional curvature [59.40521061783166]
  本研究は,非教師付き次元減少性能指標を初めて導入することを目的としている。 その実現可能性をテストするために、この測定基準は最もよく使われる次元削減アルゴリズムの性能を評価するために用いられている。 新しいパラメータ化問題インスタンスジェネレータが関数ジェネレータの形式で構築されている。
  論文  参考訳（メタデータ） (2023-03-17T11:59:33Z)
• On the Convergence of Stochastic Gradient Descent in Low-precision Number Formats [3.408623772471354]
  SGD (Single-precision Gradient Descent) の収束は通常、実数の理論的結果と一致している。 しかし、計算が低精度の数値形式で実行されると、数値誤差が増大する。 これは、低精度計算に適応したSGD収束を研究するための説得力のある理由を与える。
  論文  参考訳（メタデータ） (2023-01-04T14:54:15Z)
• Deep Subspace Encoders for Nonlinear System Identification [0.0]
  そこで本稿では,状態推定にトラッピング予測損失とサブスペースエンコーダを用いる手法を提案する。 軽度条件下では,提案手法は局所的に一貫性があり,最適化安定性が向上し,データ効率が向上することを示す。
  論文  参考訳（メタデータ） (2022-10-26T16:04:38Z)
• Assembly Planning from Observations under Physical Constraints [65.83676649042623]
  提案アルゴリズムは, 物理安定性制約, 凸最適化, モンテカルロ木探索の簡単な組み合わせを用いて, 集合を計画する。 それは効率的で、最も重要なことは、オブジェクト検出のエラーに対して堅牢であり、実際のロボットシステムでは避けられないポーズ推定である。
  論文  参考訳（メタデータ） (2022-04-20T16:51:07Z)
• Bias-Variance Tradeoffs in Single-Sample Binary Gradient Estimators [100.58924375509659]
  ストレートスルー (ST) 推定器はその単純さと効率性から人気を得た。 計算の複雑さを低く保ちながら、STよりも改善するいくつかの手法が提案された。 我々は、トレードオフを理解し、元来主張された特性を検証するために、これらの手法のバイアスとばらつきの理論解析を行う。
  論文  参考訳（メタデータ） (2021-10-07T15:16:07Z)

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

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