Technical Summary: Testing Deep Learning Libraries via Neurosymbolic Constraint Learning

Problem Statement

Deep Learning (DL) libraries, such as PyTorch and TensorFlow, are critical infrastructure for AI applications but are complex and prone to bugs. A significant challenge in testing these libraries is the lack of formal input specifications for their APIs. Existing testing techniques often fail to accurately model input constraints, leading to two primary issues:

1. Missed Valid Inputs: Techniques that ignore constraints fail to generate valid inputs that could trigger deep semantic bugs.
2. False Alarms: Techniques that imprecisely model constraints generate invalid inputs, resulting in false positives or shallow bugs (e.g., simple type errors) rather than deep functional defects.

Prior approaches rely on either API documentation (which is often incomplete, scattered, or informal) or symbolic code analysis (which can be costly and imprecise due to path explosion). Consequently, current tools struggle to reveal deep bugs associated with the core functionality of DL APIs.

Methodology: Centaur

The authors propose Centaur, the first neurosymbolic technique for testing DL library APIs. Centaur combines the domain knowledge of Large Language Models (LLMs) with the rigor of Satisfiability Modulo Theories (SMT) solvers. The workflow consists of three distinct stages:

1. Rule Generation (The Neural Part)

Centaur addresses the challenge of the prohibitively large space of candidate constraints by leveraging an LLM.

• Novel Grammar: The authors designed a specific grammar representing first-order logic formulae over API parameters. This grammar supports tensor-related properties (shape, dimensions, data types) and relational properties between parameters (e.g., broadcasting semantics).
• LLM Guidance: The LLM is prompted with the grammar, API documentation, error messages, and few-shot examples to generate syntactically correct candidate rules.
• Validation: A custom parser and type checker (based on Lark) validate the syntactic and type correctness of the generated rules, filtering out invalid candidates before further processing.

2. Constraint Learning

Once candidate rules are generated, Centaur validates them against a set of valid inputs to determine which rules are actual constraints.

• Input Generation: Centaur uses the LLM to generate a small set of valid seed inputs, which are then diversified using custom mutators.
• SMT Integration: The candidate rules are translated into Python code and encoded as Z3 (SMT solver) formulae.
• Refinement Strategy: To eliminate spurious or redundant rules, Centaur employs a heuristic refinement strategy. It iteratively removes constraints and checks if the validity ratio of generated inputs decreases. If removing a constraint does not significantly impact the ability to generate valid inputs, the constraint is deemed redundant and discarded.

3. Fuzzing (The Symbolic Part)

With a refined set of constraints, Centaur generates diverse, valid test inputs.

• Abstract Input Generation: Instead of generating concrete values directly, Centaur uses the SMT solver to generate abstract inputs (models) that satisfy the learned constraints. These abstract inputs represent valid sub-spaces of the input domain.
• Optimizations for Diversity: To prevent the SMT solver from returning the same solution repeatedly, Centaur employs two tactics:
  • Blocking: Adds constraints to prevent previously generated values from being selected again.
  • Bucketing: Partitions the input space (e.g., for integers or tensor shapes) into ranges and forces the solver to explore different buckets, ensuring uniform exploration of the input space.
• Concrete Generation: Abstract inputs are concretized into specific values and executed against the target API to detect crashes or inconsistencies.

Key Contributions

1. Centaur Framework: The first neurosymbolic API-level fuzzer for DL libraries, integrating grammar-driven LLM-assisted constraint learning with SMT-based test input generation.
2. Novel Grammar: A domain-specific grammar capable of expressing complex relational properties (like broadcasting semantics) across multiple tensor parameters, which previous tools could not capture effectively.
3. Refinement Strategy: An automated heuristic to prune spurious and redundant rules learned from the LLM, ensuring high precision in the final constraint set.
4. Bug Discovery: The identification of 26 new bugs in PyTorch and TensorFlow, with 18 confirmed by developers.

Results

The authors evaluated Centaur on PyTorch and TensorFlow, comparing it against state-of-the-art baselines: ACETest, Pathfinder, and TitanFuzz.

• Constraint Quality: Centaur achieved an average recall of 94.0% and precision of 94.0% against manually curated ground truth constraints.
• Validity Ratio: Centaur generated inputs with a validity ratio of 97.87% for PyTorch and 96.13% for TensorFlow. This significantly outperforms baselines (e.g., TitanFuzz achieved only 43.21% for PyTorch).
• Coverage: Centaur covered significantly more branches than baselines. Specifically, it covered 203, 150, and 9,608 more branches than TitanFuzz, ACETest, and Pathfinder, respectively, on average.
• Efficiency: The offline constraint learning phase is efficient (averaging a few seconds per API), and the online fuzzing phase generates valid inputs in approximately 8.9 milliseconds per input.

Significance and Claims

The paper claims that Centaur represents a significant advancement in DL library testing by addressing the "specification gap." By dynamically learning input constraints rather than relying on static documentation or expensive path analysis, Centaur can:

• Reveal Deep Bugs: It successfully identifies semantic bugs (e.g., broadcasting errors, CPU/GPU inconsistencies) that prior tools missed.
• Scale Effectively: The neurosymbolic approach allows for the generation of millions of valid, diverse inputs, overcoming the limitations of both pure fuzzing (low validity) and pure symbolic execution (path explosion).
• Generalize: The technique is presented as a general approach for domains where input specifications are sparse or informal, suggesting applicability beyond just DL libraries.

The authors emphasize that their approach does not require access to internal source code for constraint extraction (unlike ACETest), making it a black-box solution that is nonetheless highly precise due to the LLM's implicit knowledge of API semantics.