一句话：提出神经符号约束学习技术 Centaur，从种子输入学习 DL API 约束，用 SMT 生成有效多样测试并发现新缺陷。
深度学习库（如 PyTorch、TensorFlow）API 缺少规格，现有测试方法难以准确建模输入约束，既遗漏合法输入又可能因非法输入误报。本文提出 Centaur，首个利用动态学习输入约束测试 DL 库 API 的神经符号技术。它设计一阶逻辑公式语法，表达张量形状、数据类型及参数间关系，并引导 LLM 枚举候选规则，再用种子输入验证和精化以剔除虚假或冗余规则。随后结合 SMT 求解与随机采样生成合法且多样的测试输入。在 PyTorch 和 TensorFlow 上，学得约束平均召回率与精确率均达 94.0%；分支覆盖较 TitanFuzz、ACETest、Pathfinder 分别多 203、150、9608 个，并发现 26 个新缺陷，18 个已确认。
Deep Learning (DL) libraries (e.g., Pytorch) are popular in the development of AI applications. 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 constraint s. 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 to test the API. We develop a novel grammar that represents first-order logic formulae over API parameters and expresses tensor-related properties (e.g., shape, tensor data types, etc.) as well as relational properties between parameters. We use the grammar to guide a Large Language Model (LLM) to enumerate syntactically correct candidate rules, which we then validate using the 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 for the API 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.
@inproceedings{abs-2601-15493,
title = {Testing Deep Learning Libraries via Neurosymbolic Constraint Learning},
author = {M M Abid Naziri and Shinhae Kim and Feiran (Alex) Qin and Saikat Dutta and Marcelo d'Amorim},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787800}
}