Finding Input Characterizations for Output Properties in ReLU Neural Networks
This work addresses the problem of ensuring safety in neural networks for critical applications, representing an incremental improvement over prior methods.
The paper tackles the challenge of proving formal safety guarantees for ReLU neural networks by introducing a method to relate high-level correctness specifications to network architecture, achieving promising results by identifying a larger region of input space that guarantees output properties compared to existing approaches.
Deep Neural Networks (DNNs) have emerged as a powerful mechanism and are being increasingly deployed in real-world safety-critical domains. Despite the widespread success, their complex architecture makes proving any formal guarantees about them difficult. Identifying how logical notions of high-level correctness relate to the complex low-level network architecture is a significant challenge. In this project, we extend the ideas presented in and introduce a way to bridge the gap between the architecture and the high-level specifications. Our key insight is that instead of directly proving the safety properties that are required, we first prove properties that relate closely to the structure of the neural net and use them to reason about the safety properties. We build theoretical foundations for our approach, and empirically evaluate the performance through various experiments, achieving promising results than the existing approach by identifying a larger region of input space that guarantees a certain property on the output.