Panagiotis Kouvaros and Francesco Leofante from the SAIL (formerly VAS) Group have had a joint paper with researchers from Boeing accepted at the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR2023):

P. Kouvaros, F. Leofante, B. Edwards, C. Chung, D. Margineantu, A. Lomuscio. Verification of Semantic Key Point Detection for Aircraft Pose Estimation. Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR2023). Rhodes, Greece. AAAI Press.

We caught up with Panagiotis to get some more insights into the work.

Can you summarise what the paper is about?

The paper presents an analysis of the robustness of Semantic Segmentation Neural Networks developed by Boeing to estimate the pose of autonomous aircraft during landing. It discusses the extensions of the neural network verifier Venus that were put forward to tackle the increased architectural complexity of these models. Venus has been successful in providing safety certificates for these models and generating counterexamples whenever safety was not satisfied.

What are the main contributions that are made?

  • The paper extends the neural network verifier Venus to support the verification of models that:
    1. differently from previous work operate on large input and output spaces, thus dramatically increasing the computational requirements of verification
    2. feature complex layers that are not supported by other techniques at the moment
  • As opposed to much of related work which is concerned with academic benchmarks, our contribution evaluates the robustness of a concrete model from the industry which is are significantly larger than those usually used for benchmarks (75 layers with around 2 million trainable parameters and 1.6 million non-linear elements)
  • The verification studies put forward identified areas of robustness to noise and photometric perturbations and also found concrete fragilities which can be mitigated before any deployment

Why is this an important topic? The paper advances the state-of-the-art verification capabilities thereby strengthening the industrial relevance of formal verification for neural networks. This is an important contribution towards ensuring the safety of AI systems before deployment.

What’s next and what are future projects you want to pursue? Although significant progress has been made in neural network verification over the past five years, scalability remains a challenge in order to analyse large and larger systems as they are being gradually adopted in the industry. The application of formal methods to these systems needs to also account for specifications beyond noise and photometric perturbations, including robustness to semantic perturbations and system-level specifications. In future work we will focus on conquering the scalability of formal verification and extending the specification repertoire that can be analysed.