1,721,017 research outputs found
Verification and Repair of Neural Networks
No full textNeural Networks (NNs) are popular machine learning models which have found successful application in many different domains across computer science. However it is hard to provide any formal guarantee on the behaviour of neural networks and therefore their reliability is still in doubt, especially concerning their deployment in safety and security-critical applications. Verification emerged as a promising solution to address some of these problems. In the following I will present some of my recent efforts in verifying NNs
Safety Analysis of Deep Neural Networks
No full textDeep Neural Networks (DNNs) are popular machine learning models which have found successful application in many different domains across computer science. Nevertheless, providing formal guarantees on the behavior of neural networks is hard and therefore their reliability in safety-critical domains is still a concern. Verification and repair emerged as promising solutions to address this issue. In the following I will present some of my recent efforts in this area
Verification of Neural Networks for Safety and Security-critical Domains
No full textIn recent times, machine learning has gained incredible traction in the artificial intelligence community, and neural networks in particular have been leveraged in many successful applications originating from various domains. However, it is hard to provide any formal guarantee on the behavior of this kind of models, and therefore their reliability is still in doubt, especially concerning their deployment in safety and security-critical applications. In this work, we will present our contributions on the topic of formal verification, which recently emerged as a promising solution to address some of these problems. We will also present two novel use cases originating from real-world applications we are working on and the related challenges and perspectives
Counter-Example Guided Abstract Refinement for Verification of Neural Networks
No full textIn the last few decades, the employment of machine learning (ML) models has been increasingly common in the Artificial Intelligence community, with a particular focus on neural networks (NNs). However, even though they are widely adopted, the lack of formal guarantees on their behavior still restrain their use in safety-critical applications, such as avionics and self-driving vehicles. Formal Verification has been proposed to tackle the reliability issues of NNs, but its complexity and the sheer size of the models of interest have been proven to be hard challenges. In this paper we present an enhancement of our verification algorithm based on counter-example guided abstraction refinement (CEGAR) and show how it performs with respect to other approximate star-based methods
Verifying Neural Networks with Non-Linear SMT Solvers: a Short Status Report
No full textIn the last couple of decades, the popularity of neural networks has soared and they have been successfully utilized in many different domains across computer science. However, their application in safety and security-critical domains has been limited due to concerns regarding their reliability. Traditional methods for verifying neural networks (NNs) often uses linear Satisfiability Modulo Theory (SMT) solvers. These solvers work well for simple and shallow NN architectures but face limitations regarding their inability to handle non-linear activations, pooling layers, and complex activation functions, commonly used in modern deep neural networks.In this paper, we explore the potential of non-linear SMT solvers to verify intricate neural network architectures. By leveraging non-linear SMT solvers, a wider range of activation functions can be considered, leading to more accurate reasoning about the behavior of complex deep neural networks. The focus is on using recent advancements in SMT solver development to verify NNs with non-linear activation functions, particularly in the context of Computer Vision tasks. To test this idea, we conducted an experimental analysis to assess whether current nonlinear SMT solvers can efficiently handle NNs with transcendent activation functions
Constructing a Knowledge Graph for Italian Cinema Divas' Autobiographies
No full textAutobiographical writings are invaluable for research, offering relevant insights into personal experiences and cultural contexts. This is particularly true for Italian actresses, whose autobiographies, while rich with information, have been relatively underexplored in academic research. The Women Writing around the Camera (WOW) project addresses this gap by developing a semantic portal dedicated to these autobiographical texts. The WOW portal will reveal the dynamics between the actresses' writings, their private lives, their artistic careers, and the cultivation of the diva image. As a first step towards this goal, this paper presents the WOW knowledge graph (KG), which maps the personal and professional networks related to the divas' lives. The KG was built starting from the actresses' autobiographies, guided by a taxonomy of themes curated by domain experts. Although still under development and expansion, the KG provides a solid foundation for future enhancements
Participatory development of a soil health monitoring platform with organic farmers communities
No full textpyNeVer: A Framework for Learning and Verification of Neural Networks
No full textAutomated verification of neural networks (NNs) was first propose
- …
