This paper investigates the utility of open source Large Language Models for sentiment analysis in tourism reviews, with particular focus on the hospitality sector. By harnessing the power of Large Language Models and zero-shot classification techniques, we propose a resource-efficient solution that enables firms to analyse sentiments and extract keywords from reviews without the need for extensive model customisation. Through a comprehensive analysis of various open source models, experimentation, and validation on real-world tourism datasets, we demonstrate the viability and effectiveness of our approach. Our findings highlight the potential of these models as accessible tools for enhancing decision-making processes in the tourism sector, enabling firms in the hospitality domain to leverage cutting-edge technology for competitive advantage.

Abstract NeVer2 is an open-source, cross-platform tool aimed at designing, training, and verifying neural networks. It seamlessly integrates popular learning libraries with our verification backend, offering their functionalities via a graphical interface. Users can design the structure of a neural network by intuitively arranging blocks on a canvas. Subsequently, network training involves specifying dataset sources and hyperparameters through dialog boxes. After training, the verification process entails two steps: (i) incorporating input preconditions and output postconditions via dedicated blocks, and (ii) initiating verification with a simple “push-button” action. To our knowledge, there is currently no other publicly available tool that encompasses all these features. In this paper, we present a comprehensive description of NeVer2 , illustrating its complete integration of design, training, and verification through examples. Additionally, we conduct experimental analyses on various verification benchmarks to illustrate the trade-off between completeness and computability using different algorithms. We also include a comparison with state-of-the-art tools such as $$\alpha $$ α , $$\beta $$ β -CROWN and NNV for reference.

The popularity of neural networks has grown significantly in various domains, however their use in safety-critical areas has been restricted due to reliability concerns. The AIDOaRt project, an H2020-ECSEL European initiative, aims to develop dependable neural networks for safety-critical contexts. This work investigates the application of Satisfiability Modulo Theory technologies to verify neural networks with non-linear activation functions in computer vision tasks.

In the realm of predictive maintenance, the incorporation of artificial intelligence (AI) methods has revolutionized the field by empowering businesses to actively monitor and preemptively address equipment malfunctions. Detecting anomalies plays a crucial role in predictive maintenance as it serves as an early indicator of potential faults or failures. This paper introduces initial findings from the use of autoencoders and their associated vector reconstruction error within the context of the IMOCO4.E project.

In recent years, the integration of artificial intelligence (AI) techniques has significantly transformed the field of predictive maintenance, enabling businesses to proactively monitor and address potential equipment failures before they occur. One critical aspect of predictive maintenance is the detection of anomalies, which can serve as early warning signs for impending faults or failures. In this paper we present some preliminary results obtained by leveraging autoencoders and the related vector reconstruction error in the scope of the IMOCO4.E Project.

In recent years, there has been growing interest in machine learning and neural networks within research and industrial communities. While neural networks have shown impressive capabilities across various domains, their practical applications are still limited in safety-critical contexts due to a lack of formal guarantees regarding their reliability and behavior. This paper explores the latest advancements in Satisfiability Modulo Theory (SMT) technologies for verifying neural networks with piece-wise linear and transcendent activation functions. Through experimental analysis, we evaluate these technologies using neural networks trained on a real-world predictive maintenance dataset. This research contributes to the ongoing efforts to enhance the safety and reliability of neural networks through formal verification, enabling their deployment in safety-critical domains.

In 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.

Formal verification of neural networks is a promising technique to improve their dependability for safety critical applications. Autonomous driving is one such application where the controllers supervising different functions in a car should undergo a rigorous certification process. In this paper we present an example about learning and verification of an adaptive cruise control function on an autonomous car. We detail the learning process as well as the attempts to verify various safety properties using the tool NeVer2 a new framework that integrates learning and verification in a single easy-to-use package intended for practictioners rather than experts in formal methods and/or machine learning.

Neural 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.

We investigate the application of methodologies for the analysis of complex networks to understand the properties of systems of systems in a cybersecurity context. We are interested to resilience and attribution: the first relates to the behavior of the system in case of faults/attacks, namely to its capacity to recover full or partial functionality after a fault/attack; the second corresponds to the capability to tell faults from attacks, namely to trace the cause of an observed malfunction back to its originating cause(s). We present experiments to witness the effectiveness of our methodology considering a discrete event simulation of a multimodal logistic network featuring 40 nodes distributed across Italy and a daily traffic roughly corresponding to the number of containers shipped through in Italian ports yearly, averaged on a daily basis.

Deep 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 behaviour 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 deep neural networks has witnessed a recent surge of interest, fueled by success stories in diverse domains and by abreast concerns about safety and security in envisaged applications. Complexity and sheer size of such networks are challenging for automated formal verification techniques which, on the other hand, could ease the adoption of deep networks in safety- and security-critical contexts. In this paper we focus on enabling state-of-the-art verification tools to deal with neural networks of some practical interest. We propose a new training pipeline based on network pruning with the goal of striking a balance between maintaining accuracy and robustness, while also making the resulting networks amenable to formal analysis. The results of our experiments with a portfolio of pruning algorithms and verification tools show that our approach is successful for the kind of networks we consider and for some combinations of pruning and verification techniques, thus bringing deep neural networks closer to the reach of formally-grounded methods.