Testing Deep Learning Libraries via Neurosymbolic Constraint Learning

TL;DR

Centaur tackles the insufficiency of formal API input specifications in DL libraries by introducing a neurosymbolic fuzzer that learns API input constraints with an LLM-guided grammar and then generates valid, diverse test inputs via SMT-based modeling. It demonstrates high constraint accuracy (near-perfect recall/precision on many APIs) and superior coverage and validity compared with state-of-the-art fuzzers, uncovering 26 new bugs (18 confirmed). The approach decomposes rule generation, constraint learning, and fuzzing into offline and online phases, enabling efficient, scalable testing of PyTorch and TensorFlow. This work advances practical DL library testing by capturing relational, multi-parameter constraints (e.g., broadcasting semantics) that prior methods struggle to express, with potential applicability to other domains where input specifications are sparse.

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.

Figures (11)

• Figure 1: Documentation for PyTorch API and broadcasting semantics.
• Figure 2: Native code for torch.add API.
• Figure 3: Formal rules Centaur learned for broadcasting semantics.
• Figure 4: Centaur's workflow.
• Figure 5: Grammar and typing rules of Centaur.

Theorems & Definitions (2)

• definition 1: Constraint
• definition 2: Abstract Input