論文の概要: Testing Deep Learning Libraries via Neurosymbolic Constraint Learning

• arxiv url: http://arxiv.org/abs/2601.15493v1
• Date: Wed, 21 Jan 2026 21:54:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-23 21:37:20.42819
• Title: Testing Deep Learning Libraries via Neurosymbolic Constraint Learning
• Title（参考訳）: ニューロシンボリック制約学習による深層学習ライブラリのテスト
• Authors: M M Abid Naziri, Shinhae Kim, Feiran Qin, Marcelo d'Amorim, Saikat Dutta,
• Abstract要約: ディープラーニング(DL)ライブラリ(例えばPyTorch)はAI開発で人気がある。 DLライブラリをテストする上で重要な課題は、API仕様の欠如である。 動的に学習された入力制約を用いてDLライブラリAPIをテストする最初のニューロシンボリック手法であるCentaurを開発する。
• 参考スコア（独自算出の注目度）: 3.491101173753068
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Deep Learning (DL) libraries (e.g., PyTorch) are popular in AI development. These libraries are complex and contain bugs. Researchers have proposed various bug-finding techniques for such libraries. Yet, there is much room for improvement. A key challenge in testing DL libraries is the lack of API specifications. Prior testing approaches often inaccurately model the input specifications of DL APIs, resulting in missed valid inputs that could reveal bugs or false alarms due to invalid inputs. To address this challenge, we develop Centaur -- the first neurosymbolic technique to test DL library APIs using dynamically learned input constraints. Centaur leverages the key idea that formal API constraints can be learned from a small number of automatically generated seed inputs, and that the learned constraints can be solved using SMT solvers to generate valid and diverse test inputs. We develop a novel grammar that represents first-order logic formulae over API parameters and expresses tensor-related properties (e.g., shape, data types) as well as relational properties between parameters. We use the grammar to guide a Large Language Model (LLM) to enumerate syntactically correct candidate rules, validated using seed inputs. Further, we develop a custom refinement strategy to prune the set of learned rules to eliminate spurious or redundant rules. We use the learned constraints to systematically generate valid and diverse inputs by integrating SMT-based solving with randomized sampling. We evaluate Centaur for testing PyTorch and TensorFlow. Our results show that Centaur's constraints have a recall of 94.0% and a precision of 94.0% on average. In terms of coverage, Centaur covers 203, 150, and 9,608 more branches than TitanFuzz, ACETest and Pathfinder, respectively. Using Centaur, we also detect 26 new bugs in PyTorch and TensorFlow, 18 of which are confirmed.
• Abstract（参考訳）: ディープラーニング(DL)ライブラリ(例:PyTorch)は、AI開発で人気がある。 これらのライブラリは複雑で、バグを含んでいる。 研究者はこれらのライブラリに対して様々なバグフィニング手法を提案している。 しかし、改善の余地はたくさんある。 DLライブラリをテストする上で重要な課題は、API仕様の欠如である。 以前のテストアプローチでは、しばしばDL APIの入力仕様を不正確なモデルでモデル化する。 この課題に対処するため、動的に学習された入力制約を用いてDLライブラリAPIをテストする最初のニューロシンボリックテクニックであるCentaurを開発した。 Centaur氏は、フォーマルなAPI制約は、少数の自動生成されたシードインプットから学ぶことができ、学習された制約は、SMTソルバを使用して解決し、有効で多様なテストインプットを生成するというキーアイデアを活用している。 本研究では,APIパラメータ上の一階述語論理式を表現し,テンソル関連特性(例えば,形状,データ型)とパラメータ間の関係性を表現する新しい文法を開発する。 我々は,Large Language Model (LLM) を用いて,シード入力を用いて検証された構文的に正しい候補規則を列挙する。 さらに、学習ルールの集合を創り出し、余分なルールや冗長なルールを排除するためのカスタムリファインメント戦略を開発する。 学習制約を用いて,SMTに基づく解法とランダムサンプリングを統合することにより,有効かつ多様な入力を体系的に生成する。 我々は、PyTorchとTensorFlowをテストするためにCentaurを評価する。 以上の結果から,センターの制約は94.0%,精度は94.0%であった。 カバレッジに関しては、TitanFuzz、ACETest、Pathfinderよりも203、150、9,608のブランチがカバーされている。 Centaurを使用することで、PyTorchとTensorFlowの26の新たなバグを検出します。

関連論文リスト

• Constraint-Guided Unit Test Generation for Machine Learning Libraries [8.883254370291256]
  PyTorchやtensorといった機械学習(ML)ライブラリは、幅広い現代的なアプリケーションに必須である。 テストを通じてMLライブラリの正しさを保証することが重要です。 本稿では,これらの制約を活用するためにPynguinテストジェネレータを改善するアプローチであるPynguinMLを提案する。
  論文  参考訳（メタデータ） (2025-10-10T08:02:15Z)
• Your Fix Is My Exploit: Enabling Comprehensive DL Library API Fuzzing with Large Language Models [49.214291813478695]
  AIアプリケーションで広く使用されているディープラーニング(DL)ライブラリは、オーバーフローやバッファフリーエラーなどの脆弱性を含むことが多い。 従来のファジィングはDLライブラリの複雑さとAPIの多様性に悩まされている。 DLライブラリのためのLLM駆動ファジィ手法であるDFUZZを提案する。
  論文  参考訳（メタデータ） (2025-01-08T07:07:22Z)
• Subgraph-Oriented Testing for Deep Learning Libraries [9.78188667672054]
  我々は,異なるハードウェアプラットフォーム上でディープラーニング(DL)ライブラリをテストするためのSORT(Subgraph-Oriented Realistic Testing)を提案する。 SORTは、テスト対象として、しばしばモデルグラフのサブグラフとして表現される、人気のあるAPIインタラクションパターンを採用している。 SORTは100%有効な入力生成率を実現し、既存のメソッドよりも精度の高いバグを検出し、シングルAPIテストで欠落したインタラクション関連のバグを明らかにする。
  論文  参考訳（メタデータ） (2024-12-09T12:10:48Z)
• ExploraCoder: Advancing code generation for multiple unseen APIs via planning and chained exploration [70.26807758443675]
  ExploraCoderはトレーニング不要のフレームワークで、大規模な言語モデルにコードソリューションで見えないAPIを呼び出す権限を与える。 実験の結果、ExploreaCoderは、事前のAPI知識に欠けるモデルのパフォーマンスを大幅に改善することが示された。
  論文  参考訳（メタデータ） (2024-12-06T19:00:15Z)
• Enhancing Differential Testing With LLMs For Testing Deep Learning Libraries [8.779035160734523]
  本稿では,DLライブラリのためのLLM強化差分試験手法を提案する。 与えられたAPIの代替実装を見つけ、多様なテストインプットを生成するという課題に対処する。 最先端技術で見られるAPIの1.84倍の数のAPIを合成する。
  論文  参考訳（メタデータ） (2024-06-12T07:06:38Z)
• Language models scale reliably with over-training and on downstream tasks [121.69867718185125]
  スケーリング法則は、高価なトレーニング実行を引き出すための有用なガイドである。 しかし、現在の研究と言語モデルがどのように訓練されているかには差がある。 対照的に、スケーリング法則は主に推論における損失を予測するが、モデルは通常下流のタスクのパフォーマンスで比較される。
  論文  参考訳（メタデータ） (2024-03-13T13:54:00Z)
• Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
  本研究では、Boundless DASを用いて、命令に従う間、大規模言語モデルにおける解釈可能な因果構造を効率的に探索する。 私たちの発見は、成長し、最も広くデプロイされている言語モデルの内部構造を忠実に理解するための第一歩です。
  論文  参考訳（メタデータ） (2023-05-15T17:15:40Z)
• AdaNPC: Exploring Non-Parametric Classifier for Test-Time Adaptation [64.9230895853942]
  ドメインの一般化は、ターゲットのドメイン情報を活用することなく、任意に困難にすることができる。 この問題に対処するためにテスト時適応(TTA)手法が提案されている。 本研究では,テスト時間適応(AdaNPC)を行うためにNon-Parametricを採用する。
  論文  参考訳（メタデータ） (2023-04-25T04:23:13Z)

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

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