veriFIRE: an Industrial Case Study in Verifying Consistency Properties for a DNN-Based Wildfire Detection System
2026-06-02 • Logic in Computer Science
Logic in Computer ScienceMachine LearningSoftware Engineering
AI summaryⓘ
The authors describe their work on veriFIRE, a project that checks how reliable a wildfire detection system with two deep neural networks is. They created a method to test if the system behaves consistently, like increasing confidence when the fire is stronger and responding properly when the sensors get blurry. They used existing tools to turn these tests into problems a computer can solve and ran them on real data. Some tests were solved quickly, but others were harder, showing that making complex checks is challenging. Overall, their work shows it’s possible to get useful safety guarantees for real-world systems.
neural network verificationconsistency propertiesdeep neural networkswildfire detectionsolver queriesmonotonicityblur effectsafety-critical systemsverification scalabilityoperational scenarios
Authors
Idan Refaeli, Maya Swisa, Itay Buchnik, Alon Zada, Guy Amir, Elad Mandelbaum, Ziv Freund, Guy Katz
Abstract
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.