验证深度神经网络在野火探测中的稳定性,提升航空系统可靠性。
veriFIRE: an Industrial Case Study in Verifying Consistency Properties for a DNN-Based Wildfire Detection System

- 将实际需求转化为可验证的逻辑查询,用于检测模型行为一致性。
- 在真实背景样本上验证:信心随目标强度单调上升,响应在合理模糊下有界。
- 证明工业级系统可获得有意义的形式化保证,适合安全关键领域研究者。
我们介绍veriFIRE项目:产业与学术界合作,旨在通过形式化验证提升真实世界安全关键系统的可靠性。具体针对搭载两个深度神经网络的机载野火探测平台,提出端到端方法以验证其一致性性质。将应用相关的约束编码为现有神经网络验证器兼容的查询,针对关键操作场景分析两类性质:(i)探测器置信度随目标强度增加时的单调性;(ii)传感器在物理合理模糊下的响应边界。使用先进的神经网络验证后端实例化并大规模测试真实背景样本。第一类性质所有查询均在五分钟内完成验证;第二类性质验证难度显著更高,凸显更复杂高维规范的可扩展性挑战。总体表明,可为工业系统提供有意义且领域特定的形式化保障。
原文摘要 · Abstract (English)
We present our ongoing work on the veriFIRE project: a collaboration between industry and academia, aimed at applying verification to increase the reliability of a real-world, safety-critical system. Specifically, we target an airborne platform for wildfire detection, which incorporates two deep neural networks. We present an end-to-end methodology for verifying \textit{consistency properties} in this system. Our approach encodes application-grounded requirements into solver-compatible queries for existing neural network verifiers. We study properties of interest over critical operational scenarios: (i) monotonicity of detector confidence as target intensity increases; and (ii) bounded detector response under physically plausible blur over the sensor. We instantiate these encodings using state-of-the-art neural network verification backends and evaluate them at scale on real background samples. For the first property, all verification queries are solved in under five minutes. For the second property, verification is substantially harder, highlighting key scalability challenges for richer, higher-dimensional specifications. Overall, the results demonstrate that meaningful, domain-specific guarantees can be obtained for industrial systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。