Towards Formal Verification of Deep Neural Networks for Object Detection

arXiv:2407.01295 · cs.CV · Submitted 2024-07-01 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: I'm Tom, and with me are Jane, Lu, senior AI researcher at Tsinghua, Meng, lead engineer at a mysterious AI startup and Lalam, the in-house Large Language Model.

Jane: Today's paper: "Towards Formal Verification of Deep Neural Networks for Object Detection".

Tom: Deep neural networks (DNNs) are increasingly deployed in safety-critical applications, yet their statistical nature makes them vulnerable to errors and adversarial attacks, necessitating robust defense mechanisms.

Jane: First, who's behind it and why it matters.

Title and authors: Tom: We've just covered the core ideas behind "Towards Formal Verification of Deep Neural Networks for Object Detection," and now let's talk about who wrote this paper and what that means for the research community. The authors are Yizhak Y. Elboher, Avraham Raviv, Yael Leibovich Weiss, Omer Cohen, Roy Assa, Guy Katz, and Hillel Kugler from Hebrew University of Jerusalem and Bar-Ilan University.

Jane: It’s interesting to see a team from different institutions collaborating on this; it shows that this kind of challenging research isn't confined to one lab or university. It highlights the interdisciplinary nature of tackling these complex AI problems.

Lu: I think the collaboration itself is significant because object detection has traditionally been overlooked in formal verification, so having experts from different backgrounds focusing on this specific gap is really valuable for pushing the boundaries of what we know about DNN reliability.

Meng: I wonder if the diversity in background influences how they approach these mathematical modeling challenges; do some of these researchers bring a different perspective to solving those tricky IoU encoding problems?

Lalam: I think having diverse perspectives helps because you get different ways of looking at the problem, which is essential when you’re trying to find novel solutions for something as complex as verifying object detection.

Tom: It certainly does. And it connects directly to the paper's goal, which is bridging that gap between classification verification and object detection verification by showing how existing tools can be adapted for these new formulations.

Jane: That adaptation aspect is key; they aren't inventing entirely new math from scratch, but rather showing practical insights into repurposing current verification software for this specific task.

Lu: That approach of adaptation is what makes the work accessible to other researchers because it provides a roadmap on how to leverage existing methodologies without having to reinvent the wheel entirely.

Meng: From an engineering standpoint, I appreciate that they are focusing on practical insights into utilizing current tools with minimal changes, rather than just proposing some theoretical framework that would require massive infrastructure overhaul.

Lalam: It’s about making the technology accessible; if we can show how to use existing tools with minor adjustments, then more researchers in the field can start applying formal verification to object detection sooner.

The paper's summary: Tom: Moving on from the authors, let’s look at what they actually said in the summary of "Towards Formal Verification of Deep Neural Networks for Object Detection." Essentially, this paper lays out a clear plan: they systematically explore attacks and validate DNN robustness for object detection.

Jane: They are setting up clear definitions for assessing model robustness against different attack vectors, which establishes the necessary groundwork before they start running any actual verification tests.

Lu: The summary emphasizes that their contributions include casting various object detection attacks as formal verification problems by establishing clear definitions so we know exactly what we're testing.

Meng: So, they define the specific logical conditions for misdetection, misclassification, and overdetection that need to be refuted for the model to be considered safe.

Lalam: They also show how existing verification tools can handle these new formulations by developing an adaptation that offers practical insights into utilizing current tools with minimal changes.

Tom: And they don't just stop at defining the problem; they implement the proposed verification method and adapt a state-of-the-art tool to verify multiple object detection models on multiple datasets.

Jane: That means they’ve moved beyond theory and shown that their proposed verification technique actually works in practice across several real scenarios.

Lu: They are providing concrete examples of several attacks on object detectors and robust analysis of multiple object detection models and datasets, which really solidifies the need to extend formal methods to broader computer vision tasks.

Meng: It sounds like they've put together a complete pipeline: definition, adaptation, implementation, and testing across different networks and data.

Lalam: That comprehensive approach is what makes this paper significant; it shows that the proposed framework isn't just a theoretical idea but something functional for object detection robustness analysis.

The paper's improvements: Tom: Now let’s get into the specific suggested improvements in "Towards Formal Verification of Deep Neural Networks for Object Detection." They highlight several areas where they can make the verification more powerful and comprehensive.

Jane: One big suggestion is to improve the model architecture by adding specialized layers that explicitly model Intersection over Union calculations, rather than relying on post-hoc calculation outside the verification loop.

Lu: This is a crucial architectural change because it means you’re baking the IoU logic directly into the network structure so that it behaves predictably under verification constraints.

Meng: So, instead of calculating IoU as an external step, you have layers that model those geometric relationships using only subtraction and multiplication to keep things contained within the verification process.

Lalam: That’s a very practical suggestion because it addresses the core difficulty they face with verifying division by replacing it with something more manageable.

Tom: They also suggest developing an adaptive verification algorithm, Algorithm two which sequentially checks both conditions for misdetection and misclassification before falling back to a complete verification process.

Jane: That hybrid approach sounds very smart because it allows the system to be efficient; you can try targeted checks first for speed and then use the full verification process if needed.

Lu: It’s about creating a tiered strategy, where you prioritize checking specific failure modes before running the most computationally expensive checks.

Meng: From an engineering view, that tiered strategy makes sense because it allows us to manage the computational load on our systems when we need to run deep verification on production models.

Lalam: That layered approach gives us a clear path forward for improving the system, showing exactly how to make it more efficient while maintaining thoroughness.

Conclusion: Tom: We’re wrapping up with the conclusion of "Towards Formal Verification of Deep Neural Networks for Object Detection." In short, this paper successfully introduces a framework to formalize multiple attack types—misdetection, misclassification, and overdetection as formal verification problems for object detection.

Jane: They demonstrated how to adapt classification tools to handle these new formulations by showing that they can effectively verify these complex vision tasks.

Lu: The implication is that we now have a formalized way to assess the robustness of object detection models against specific adversarial attacks, which was previously unexplored territory.

Meng: This means we can start building more reliable object detection components with a formal layer of assurance built in before they even go into production environments.

Lalam: It’s about moving toward systems where the behavior is formally proven to be consistent across all inputs within the specified threat model, which is a big step for user trust.

Tom: We’re concluding that "Towards Formal Verification of Deep Neural Networks for Object Detection" gives us a framework to systematically address vulnerabilities in these critical computer vision tasks by casting attacks as formal verification problems.

Jane: It’s a significant piece of research because it shows how formal methods can be applied to complex vision tasks with the right mathematical tools.

Lu: This opens up exciting avenues for future work, especially extending this concept to other areas beyond object detection where we can apply this structured approach.

Meng: I think the next step is taking this robust framework and integrating it into actual deployment pipelines so that verification becomes a standard part of the workflow, not just an academic exercise.

Lalam: I’m excited to see what this means for how we design AI systems moving forward because it moves us toward building AI that is inherently more dependable.

Yizhak Y. Elboher, Avraham Raviv, Yael Leibovich Weiss, Omer Cohen, Roy Assa, Guy Katz

The Hebrew University of Jerusalem · Bar-Ilan University

cs.CV

Submitted: 2024-07-01

Updated: 2026-09-30

Comments: NASA Formal Methods (NFM) 2026

License: http://creativecommons.org/licenses/by-nc-sa/4.0/

Importance score: 78/100

The gist: Deep neural networks (DNNs) are increasingly deployed in safety-critical applications, yet their statistical nature makes them vulnerable to errors and adversarial attacks, necessitating robust

Key concepts

Object Detection Attacks
These are specific ways an input image can be subtly altered (perturbed) to cause the detection model to fail. The paper focuses on defining constraints for these attacks, such as making the model miss a target object or detect too many objects, based on how close the perturbed image is to the original.
IoU Modeling
Intersection over Union (IoU) measures how well a predicted bounding box overlaps with the ground truth. Since IoU involves division, it cannot be directly verified. The authors solve this by adding a neural layer that transforms the IoU constraint into a simple linear inequality, allowing verification tools to process it.
Formal Verification Adaptation
This is the process of taking existing verification tools designed for simpler tasks (like classification) and modifying them to handle the new, more complex requirements of object detection. The authors adapted Alpha-Beta-CROWN to verify these new attack scenarios, showing how current tools can be used with minimal changes.
Robustness Property
This is a logical statement that defines what makes a model robust against an attack. For example, the robustness property for misdetection means: if the input is close to the original image, then it must not be possible to cause a misdetection.

Terminology

Summary

Deep neural networks (DNNs) are increasingly deployed in safety-critical applications, yet their statistical nature makes them vulnerable to errors and adversarial attacks, necessitating robust defense mechanisms. This paper addresses this vulnerability by extending formal verification methods, traditionally focused on image classification models, to the more complex domain of object detection models. By systematically casting various object detection attacks as formal verification problems and adapting state-of-the-art tools like Alpha-Beta-CROWN, the authors demonstrate how to uncover vulnerabilities in these critical computer vision tasks.

Contributions

The research makes several key contributions aimed at bridging the gap between object detection and formal verification:

  1. Cast various object detection attacks as formal verification problems by establishing clear definitions for assessing model robustness against different attack vectors.

  2. Show how existing verification tools, primarily designed for classification tasks, can be adjusted to handle these new formulations, developing an adaptation that offers practical insights into utilizing current tools with minimal changes.

  3. Implement the proposed verification method and adapt a state-of-the-art verification tool to verify multiple object detection models on multiple datasets.

  4. Provide (i) examples of several attacks on object detectors and (ii) robustness analysis of multiple object detection models and datasets, underscoring the need for extending formal methods to broader computer vision tasks.

  5. Compare the complete method against other verification methods, such as Interval Bound Propagation (IBP), demonstrating that their approach is able to solve a significantly higher number of queries.

Formalization of Object Detection Attacks

The paper defines an input constraint based on a small perturbation from the original image: "P:= x − x0 < ϵ," which limits the adversarial image to be sufficiently close to the original. The output constraints are formulated by defining specific attack vectors as logical conditions that must be refuted. For instance, for misdetection, the condition Q1 is defined as: "og > od) ∨ ∃i ∈ [og] ∀j ∈ [od]: IoU(Gi, Dj) < τ. The robustness to misdetection is then represented by the property P ⇒ ¬Q1, which translates to: ¬Q1:= (og ≤ od) ∧ ∀i ∈ [og] ∃j ∈ [od]: IoU(Gi, Dj) > τ." Similar formal definitions are provided for misclassification (Q2) and overdetection (Q3).

Modeling IoU-related Conditions with Neural Layers

A central challenge is that the Intersection over Union (IoU) value, which is a result of division, cannot be directly verified by most verifiers. To overcome this, the authors propose extending the network architecture by adding layers to model equivalent conditions using only subtraction and multiplication operators. The calculation involves:

  1. Computing the area of intersection (AI) and union (AU) from ground truth bounding box Bgt and predicted bounding box Bdt using max, min, add and subtract operations.

  2. Encoding the IoU constraint ("IoU > τ) into an equivalent linear constraint: AI − τ · AU > 0."

  3. This equivalent condition is then encoded using a single neural layer, resulting in a variable 'z' whose result is positive if and only if the original IoU condition holds.

Verification Queries and Algorithm Design

The paper details how to convert the original query (f, P, ¬Qi) into an equivalent query (f′, P, ¬Q′i) by extending the network with a neuron representing ¬Qi. For misdetection, this results in the query "(f′, P, z > 0). For misclassification and overdetection robustness checks, Algorithm 1 is presented as an anytime verification method that iteratively checks both conditions for misdetection and misclassification, returning Unsafe if at least one of the answers returned by the underlying sound verification tool is Unsafe."

Evaluation and Comparison to IBP

The effectiveness of the approach was tested on three datasets: MNIST-OD, LARD, and GTSRB. The results show that as epsilon decreases (i.e., perturbation size gets smaller), more robustness properties can be verified. The comparison against Interval Bound Propagation (IBP) methods indicates that the proposed method stands out as the only approach that successfully identifies Unsafe instances across both datasets, solving a total of 423 instances for MNIST-OD and 434 for LARD, which is about 70% more instances compared to the runner-up. While the proposed method has a higher average runtime (e.g., 2.73 seconds on MNIST-OD), it is noted that this increase in computation time results in a more comprehensive verification, particularly in identifying unsafe scenarios, as it returns both Safe and Unsafe results.

Conclusion

This work successfully introduces a framework to formalize multiple attack types—misdetection, misclassification, and overdetection—as formal verification problems for object detection.

Improvements for AI systems

Based on the provided scientific paper, here are specific improvements that can be made to existing AI systems, along with what those improved systems could achieve:

I will focus on improving object detection models by integrating formal verification techniques into their design and deployment pipeline. The core capability gained is a mathematically guaranteed level of robustness against adversarial attacks.

The proposed system involves three main pillars:

  1. Formalization of Attacks (Misdetection, Misclassification, Overdetection) as logical constraints.

  2. Architectural Extension to Model IoU Calculation using Neural Layers (Encoding IoU).

  3. Adaptive Verification Algorithm (Algorithm 2) combining Attack Refutation and Incomplete Verification phases efficiently.

Here are the specific improvements:

  1. Improve the Object Detection model architecture by adding specialized layers that explicitly model Intersection over Union (IoU) calculations, rather than relying on post-hoc IoU calculation outside the verification loop.

  2. Implement a formal verification framework that systematically checks if an object detector satisfies robust properties (e.g., for any input within perturbation range, the IoU of detected objects with ground truth objects must be above threshold).

  3. Develop a Hybrid Verification Engine (Algorithm 2) that sequentially attempts to refute specific attack types (misdetection, misclassification) using targeted verification queries before falling back to a complete verification process, ensuring both soundness and completeness efficiently.

The improved AI system can achieve the following:

  1. Can detect objects reliably even when subjected to small, imperceptible adversarial perturbations (e.g., noise added by an attacker).

  2. Is guaranteed not to suffer from Misdetection (missing a real object) or Overdetection (detecting phantom objects) under defined perturbation budgets, as the system will fail verification if these conditions are met within the input constraint set.

  3. Is guaranteed not to suffer from Misclassification by ensuring that any detected object maintains its correct class label, even when its bounding box is slightly perturbed or when a different class is incorrectly assigned.

  4. Can operate with high confidence in safety-critical domains (e.g., autonomous driving, medical imaging) because the system's behavior is formally proven to be consistent across all inputs within the specified threat model, mitigating vulnerabilities that plague standard deep learning models.

Abstract

Deep neural networks (DNNs) are widely used in real-world computer vision applications, yet they remain vulnerable to errors and adversarial attacks. Formal verification offers a systematic approach to identify and mitigate these vulnerabilities, enhancing model robustness and reliability. While most existing verification methods focus on image classification models, this work extends formal verification to the more complex domain of object detection models. We propose a formulation for verifying the robustness of such models and demonstrate how state-of-the-art verification tools, originally developed for classification, can be adapted for this purpose. Through a comprehensive evaluation, we highlight the ability of formal verification to uncover vulnerabilities in object detection models, and derive formal robustness guarantees, underscoring the potential and need to further extend verification efforts in this domain. This work lays the foundation for further research into formal verification of object detection models across a broader range of computer vision applications. Our source code is publicly available online.

Sources

Related papers