In this paper, we present the SECURED project11Funded in part by the European Union (EU), Grant Agreement no. 10109571. Views and opinions expressed are those of the authors and do not necessarily reflect those of the EU or the Health and Digital Executive Agency. Neither the EU nor the granting authority are responsible for them., aimed at improving privacy-preserving processing of data in the health domain. The technologies developed in the project will be demonstrated in four health-related use cases and with the involvement of SME's selected through an open funding call.

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.

Using semantic web technologies is becoming an efficient way to overcome metadata storage and data integration problems in digital archives, thus enhancing the accuracy of the search process and leading to the retrieval of more relevant results. In this paper, the results of the implementation of the semantic layer of the Józef Piłsudski Institute of America digital archive are presented. In order to represent and integrate data about the archival collections housed by the institute, the authors developed arkivo, an ontology that accommodates the archival description of records but also provides a reference schema for publishing linked data. The authors describe the application of arkivo to the digitized archival collections of the institute, with emphasis on how these resources have been linked to external datasets in the linked data cloud. They also show the results of an experiment focused on the query answering task involving a state-of-the-art triple store system. The dataset related to the Piłsudski Institute archival collections has been made available for ontology benchmarking purposes.

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.

Cyber-Physical Systems (CPS) are embedded computational collaborating devices, capable of sensing and controlling physical elements and, often, responding to humans. Designing and managing systems able to respond to different, concurrent requirements during operation is not straightforward, and introduce the need of proper support at design-time and run-time. The Cross-layer modEl-based fRamework for multi-oBjective dEsign of Reconfigurable systems in unceRtain hybRid envirOnments (CERBERO) EU project has developed a design environment for adaptive CPS. CERBERO approach leverages on model-based methodologies including different technologies and tools developed to cover design and operation from user interactions down to low level computing layer implementation.

In the context of Requirements Engineering, checking the consistency of functional requirements is an important and still mostly open problem. In case of requirements written in natural language, the corresponding manual review is time consuming and error prone. On the other hand, automated consistency checking most often requires overburdening formalizations. In this paper we introduce ReqV, a tool for formal consistency checking of requirements. The main goal of the tool is to provide an easy-to-use environment for the verification of requirements in Cyber-Physical Systems (CPS). ReqV takes as input a set of requirements expressed in a structured natural language, translates them in a formal language and it checks their inner consistency. In case of failure, ReqV can also extracts a minimal set of conflicting requirements to help designers in correcting the specification.

The decision problem of quantified Boolean formulas (QBFs) is the archetypical problem for the complexity class PSPACE. Beside such theoretical aspects QBF also provides an attractive framework for encoding and solving various application problems ranging from symbolic reasoning in artificial intelligence to the formal verification and synthesis of computing systems. In this paper, we survey the different application areas that exploit QBF technology for solving their specific problems.

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

The recent application of Machine Learning techniques to the Answer Set Programming (ASP) field proved to be effective. In particular, the multi-engine ASP solver me-asp is efficient: it is able to solve more instances than any other ASP system that participated to the 3rd ASP Competition on the ‘System Track’ benchmarks. In the me-asp approach, classification methods inductively learn offline algorithm selection policies starting from both a set of features of instances in a training set, and the solvers performance on such instances. In this article we present an improvement to the multi-engine framework of me-asp, in which we add the capability of updating the learned policies when the original approach fails to give good predictions. An experimental analysis, conducted on training and test sets of ground instances obtained from the ones submitted to the ‘System Track’ of the 3rd ASP Competition, shows that the policy adaptation improves the performance of me-asp when applied to test sets containing domains of instances that were not considered for training.

Abstract Answer-set programming (ASP) is a truly declarative programming paradigm proposed in the area of non-monotonic reasoning and logic programming, which has been recently employed in many applications. The development of efficient ASP systems is, thus, crucial. Having in mind the task of improving the solving methods for ASP, there are two usual ways to reach this goal: (i) extending state-of-the-art techniques and ASP solvers or (ii) designing a new ASP solver from scratch. An alternative to these trends is to build on top of state-of-the-art solvers, and to apply machine learning techniques for choosing automatically the “best” available solver on a per-instance basis. In this paper, we pursue this latter direction. We first define a set of cheap-to-compute syntactic features that characterize several aspects of ASP programs. Then, we apply classification methods that, given the features of the instances in atrainingset and the solvers' performance on these instances, inductively learn algorithm selection strategies to be applied to atestset. We report the results of a number of experiments considering solvers and different training and test sets of instances taken from the ones submitted to the “System Track” of the Third ASP Competition. Our analysis shows that by applying machine learning techniques to ASP solving, it is possible to obtain very robust performance: our approach can solve more instances compared with any solver that entered the Third ASP Competition.

Given a stochastic policy learned by reinforcement, we wish to ensure that it can be deployed on a robot with demonstrably low probability of unsafe behavior. Our case study is about learning to reach target objects positioned close to obstacles, and ensuring a reasonably low collision probability. Learning is carried out in a simulator to avoid physical damage in the trial-and-error phase. Once a policy is learned, we analyze it with probabilistic model checking tools to identify and correct potential unsafe behaviors. The whole process is automated and, in principle, it can be integrated step-by-step with routine task-learning. As our results demonstrate, automated fixing of policies is both feasible and highly effective in bounding the probability of unsafe behaviors.

We consider the task of assigning experts from a portfolio of specialists in order to solve a set of tasks. We apply a Bayesian model which combines collaborative filtering with a feature-based description of tasks and experts to yield a general framework for managing a portfolio of experts. The model learns an embedding of tasks and problems into a latent space in which affinity is measured by the inner product. The model can be trained incrementally and can track non-stationary data, tracking potentially changing expert and task characteristics. The approach allows us to use a principled decision theoretic framework for expert selection, allowing the user to choose a utility function that best suits their objectives. The model component for taking into account the performance feedback data is pluggable, allowing flexibility. We apply the model to manage a portfolio of algorithms to solve hard combinatorial problems. This is a well studied area and we demonstrate a large improvement on the state of the art in one domain (constraint solving) and in a second domain (combinatorial auctions) created a portfolio that performed significantly better than any single algorithm.

In this paper we consider the problem of ensuring that a multi-agent robot control system is both safe and effective in the presence of learning components. Safety, i.e., proving that a potentially dangerous configuration is never reached in the control system, usually competes with effectiveness, i.e., ensuring that tasks are performed at an acceptable level of quality. In particular, we focus on a robot playing the air hockey game against a human opponent, where the robot has to learn how to minimize opponent's goals (defense play). This setup is paradigmatic since the robot must see, decide and move fastly, but, at the same time, it must learn and guarantee that the control system is safe throughout the process. We attack this problem using automata-theoretic formalisms and associated verification tools, showing experimentally that our approach can yield safety without heavily compromising effectiveness.

From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preprocessors, in that some QBF solvers benefit from a preprocessing phase when it reduces the treewidth of their input. Our experiments suggest that structural simplifications reducing treewidth are a potential enabler for the solution of hard QBF encodings.