arXiv cs.CL· Avaljot Singh, Yasmin Chandini Sarita, Aditya Mishra, Gagandeep Singh, Charith Mendis·· 11 小时前AI 评分31
Neuton：自动将神经元级抽象解释器规范编译为张量级可执行程序
Automatic Tensor-level Execution of Abstract Interpreters for Neural Networks
AI 导读
Neuton 框架可将神经元级 DNN 认证器规范自动翻译为张量级可执行程序，无需手写张量编程。它通过基于栈的 IR 与形状分析推断广播、维度扩展和归约等隐式张量操作，并用领域重写规则优化常见操作序列，还提出面向认证器稀疏性的 gBCSR 稀疏张量格式。
正文 · AI 翻译
摘要：开发新的基于抽象解释的 DNN 验证器很困难，因为其数学设计是在神经元层面表达的，而实现必须在张量层面运行。现有库如 auto_LiRPA、IVAN 和 ERAN 支持固定的验证器集合；扩展它们需要形式化方法和张量编程方面的专业知识。像 ConstraintFlow 这样的领域特定语言让研究人员可以在神经元层面指定验证器，但无法在真实 DNN 上运行它们。
我们提出 Neuton，一个将神经元层面的验证器规范自动转换为张量层面可执行文件的框架，无需手动张量编程即可实现新的 DNN 验证器。Neuton 有三项贡献。第一，基于栈的中间表示（IR）和形状分析推断正确执行所需的隐式张量操作，包括广播、维度扩展和归约。第二，领域特定的重写规则将常见的张量操作序列优化为更高效的等价形式。第三，gBCSR 是一种稀疏张量格式，使用基于非零默认值的可变大小、层对齐块，专为 DNN 验证器的稀疏性量身定制。
我们证明该转换保持了神经元层面的语义。我们在 8 个验证器和 32 个 DNN 基准上评估 Neuton。Neuton 编译了四个现有验证器，并首次为另外四个验证器生成了可执行实现：其中两个此前已被指定但从未运行，另外两个是新设计。这些实现揭示了现有库中不可用的精度-运行时权衡。例如，SkipPoly 在所有 32 个 DNN 上达到与 DeepPoly 相同的精度，同时在一半的 DNN 上运行速度相同或更快。Neuton 在现有验证器上的运行时性能与手工优化的库相比具有竞争力。代码：此 https URL
| 学科： | 计算与语言（cs.CL） |
| 引用为： | arXiv:2507.20055 [cs.CL] |
| （或 arXiv:2507.20055v2 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2507.20055 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Avaljot Singh [查看电子邮件]
[v1]
2025年7月26日星期六 20:38:29 UTC（4,660 KB）
[v2]
2026年10月16日星期五 17:43:47 UTC（852 KB）
来源：arXiv cs.CL · arxiv.org