一句话：提出 PreBoxes 框架，用猜测-检验自动合成 DNN 的 Boxes 充分前置条件，并支持迭代求解更弱条件。
论文针对 DNN 在安全关键系统中缺乏形式化数据前置条件、可信度不确定的问题，提出猜测-检验框架 PreBoxes，自动为 DNN 合成关于安全性与鲁棒性等丰富后置条件的 Boxes 充分前置条件。猜测阶段用启发式方法生成候选，检验阶段以形式化保证验证；框架支持自动自适应迭代以得到更弱前置条件。所得条件可用于 DNN 屏蔽和可解释性增强。作者在 4 个基准、20 多个模型、23 个可信性质上评估，并与 3 种典型方案比较，表明 PreBoxes 通常推断出更弱的非平凡充分前置条件，且能处理复杂性质与非 ReLU 复杂结构网络。
Deep neural network (DNN) has been increasingly deployed as a key component in safety-critical systems. However, the credibility of DNN components is uncertain due to the absence of formal specifications for their data preconditions, which are essential for ensuring trustworthy postconditions.In this paper, we propose a guess-and-check-based framework PreBoxes to automatically synthesize Boxes sufficient preconditions for DNN concerning rich safety and robustness postconditions.The framework operates in two phases: the guess phase generates potentially complex candidate preconditions through heuristic methods, while the check phase verifies these candidates with formal guarantees.The entire framework supports automatic and adaptive iterative running to obtain weaker preconditions as well.Such resulting preconditions can be leveraged to shield DNN for safety and enhance the interpretability of DNN in application.PreBoxes has been evaluated on over 20 models with 23 trustworthy properties of 4 benchmarks and compared with 3 existing typical schemes.The results show that not only does PreBoxes generally infer weaker non-trivial sufficient preconditions for DNN than others, but also it expands competitive capabilities to handle both complex properties and Non-ReLU complex structured networks.