arXiv cs.AI· Zexin Li, Weibo Zhang, Linyi Li, Arvind Easwaran, Simin Chen·· 12 小时前AI 评分27
ProCerDCL：深度学习编译器优化的查询高效黑盒概率验证框架
ProCerDCL: Query-Efficient Black-Box Probabilistic Verification of Deep Learning Compiler Optimization
AI 导读
ProCerDCL 是一个查询高效的黑盒概率验证框架，在给定可采样输入分布和二元性质预言机下，判断性质违反概率 p 是否超过阈值 θ，并给出接受、拒绝或不确定的三值结论。
正文 · AI 翻译
摘要：我们提出 \tool，一个面向黑盒概率验证的查询高效框架。给定固定的、可采样的输入分布以及一个二值性质预言机，\tool 评估该性质被违反的概率 $p$ 是否超过阈值 $\theta$。在独立采样和无状态预言机行为下，接受表示 $p\le\theta$，拒绝表示 $p>\theta+\eta$（$\eta$ 为用户指定的分离裕度），而不确定结论表示对任一结论证据不足。每种错误结论的概率均以其指定的错误预算为界。为高效支持这一三值契约，\tool 使用单个序贯检验，消除了基线所需的区间族。该检验通过校正的精确二项置信区间或随时有效的置信序列来处理重复采样检查。我们将 \tool 应用于概率局部模型语义一致性，其中性质预言机在指定扰动分布下检测参考执行与编译执行之间的决策级不一致。我们的评估涵盖 TorchInductor 和 TensorRT 上的 24 个任务，并考察采样效率、结论确定性和诊断行为。在采样效率方面，我们使用配对单模型干净标签半径搜索：在匹配的数值参数下，基线所需的唯一样本数是我们的 3.6-4.2 倍，同时提供的决策契约更弱。在模型语义一致性方面，在 $\theta=10^{-3}$ 下进行检查，来自 21 个任务的 840 个输入-后端实例中产生 817 个接受、19 个不确定结论和 4 个拒绝。对两个已记录编译器故障的案例研究进一步展示了这些局部结论能够诊断什么。
| 学科： | 软件工程（cs.SE）；人工智能（cs.AI）；编程语言（cs.PL） |
| 引用为： | arXiv:2610.36499 [cs.SE] |
| （或 arXiv:2610.36499v1 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.36499 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Simin Chen [查看邮箱]
[v1]
2026年10月27日星期二 01:57:08 UTC（840 KB）
来源：arXiv cs.AI · arxiv.org