ProCerDCL: 深度学习编译器优化的查询高效黑盒概率验证
ProCerDCL: Query-Efficient Black-Box Probabilistic Verification of Deep Learning Compiler Optimization
Zexin Li · Weibo Zhang · Linyi Li · Arvind Easwaran · Simin Chen
中文摘要
ProCerDCL 是一个用于黑盒概率验证的查询高效框架。在给定可采样输入分布和二元属性预言机时，该框架评估属性违反概率 p 是否超过阈值 θ。在独立采样和无状态预言机行为下，接受断言 p≤θ，拒绝断言 p>θ+η（η 为用户指定的分离裕度），不确定结论表示证据不足。每类错误结论的概率均受指定错误预算限制。为高效支持这一三值契约，ProCerDCL 采用单一顺序测试，消除了基线所需的区间族。该测试通过修正的精确二项置信区间或任意时有效置信序列来处理重复采样检查。ProCerDCL 应用于概率局部模型语义一致性，其中属性预言机检测指定扰动分布下参考执行与编译执行间的决策级不一致。评估涵盖 TorchInductor 和 TensorRT 的 24 个任务，考察采样效率、确定性和诊断行为。在采样效率方面，使用配对单模型干净标签半径搜索：在匹配数值参数下，基线需要多 3.6-4.2 倍的唯一样本，且提供较弱的决策契约。在模型语义一致性方面，θ=10^-3 的检查在来自 21 个任务的 840 个输入-后端实例中产生 817 次接受、19 次不确定结论和 4 次拒绝。两个已记录的编译器故障案例研究进一步展示了这些局部结论的诊断能力。
关键要点
- 01提出 ProCerDCL 框架，通过单一顺序测试实现黑盒概率验证，消除基线所需的区间族。
- 02采用修正精确二项置信区间或任意时有效置信序列处理重复采样，确保错误结论概率受控。
- 03应用于深度学习编译器语义一致性验证，检测参考与编译执行在扰动下的决策级不一致。
- 04评估显示基线需多 3.6-4.2 倍样本且契约较弱；θ=10^-3 时 840 实例中 817 次接受、4 次拒绝。
解读
尚无解读。
原始英文摘要
arXiv:2610.36499v1 Announce Type: cross Abstract: We present \tool, a query-efficient framework for black-box probabilistic verification. Given a fixed, sampleable input distribution and a binary property oracle, \tool assesses the property's violation probability $p$ against a threshold $\theta$. Under independent sampling and stateless oracle behavior, acceptance asserts $p\le\theta$, rejection asserts $p>\theta+\eta$ for a user-specified separation margin, and an inconclusive verdict indicates insufficient evidence for either conclusion. The probability of each type of erroneous verdict is bounded by its specified error budget. To support this three-valued contract efficiently, \tool uses a single sequential test, eliminating the interval family required by the baseline. The test accounts for repeated sampling checks through either corrected exact binomial confidence intervals or an anytime-valid confidence sequence. We apply \tool to probabilistic local model semantic consistency, where the property oracle detects decision-level inconsistencies between reference and compiled executions under a specified perturbation distribution. Our evaluation covers 24 tasks across TorchInductor and TensorRT and examines sampling efficiency, conclusiveness, and diagnostic behavior. For sampling efficiency, we use paired one-model clean-label radius searches: the baseline requires 3.6-4.2 times as many unique samples under matched numerical parameters while providing a weaker decision contract. For model semantic consistency, checks at $\theta=10^{-3}$ yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections across 840 input--backend instances from 21 tasks. Case studies of two documented compiler faults further demonstrate what these local verdicts can diagnose.