Natural language explanations play a fundamental role in Natural Language Inference (NLI) by revealing how premises logically entail hypotheses.Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations.However, TPs require translating natural language into machine-verifiable formal representations, a process that introduces the risk of semantic information loss and unfaithful interpretation, an issue compounded by LLMs' challenges in capturing critical logical structures with sufficient precision.Moreover, LLMs are still limited in their capacity for rigorous and robust proof construction within formal verification frameworks.To mitigate issues related to faithfulness and robustness, this paper investigates strategies to (1) alleviate semantic loss during autoformalisation, (2) efficiently identify and correct syntactic errors in logical representations, (3) explicitly use logical expressions to guide LLMs in generating structured proof sketches, and (4) increase LLMs' capacity of interpreting TP's feedback for iterative refinement.Our empirical results on e-SNLI, QASC and WorldTree using different LLMs demonstrate that the proposed strategies yield significant improvements in autoformalisation (+18.46%,+34.2%, +39.77%) and explanation refinement (+29.5%,+51.5%, +41.25%) over the state-of-the-art model.Moreover, we show that specific interventions on the hybrid LLM-TP architecture can substantially improve efficiency, drastically reducing the number of iterations required for successful verification.1

An assurance case provides a structured argument, supported by evidence, aiming to justify some key property of a system. Reference assurance cases can serve as standardised templates or examples for developing assurance cases across various industries, facilitating alignment with regulatory standards and supporting certification. They hold the potential to more efficiently develop the assurance case and ensure best practice is maintained. A key technique in developing a reference assurance case is the use of assurance patterns. These patterns, inspired by design patterns, enable the reuse of safety argument structures. In this paper we apply this concept to the assurance of autonomous inspection robots that operate in dynamic and uncertain environments. Given the inherent complexity that arises from the autonomy of these systems, a range of distinct verification methods (e.g., formal verification, simulation, physical experiments) will be required to foster confidence. This work-in-progress paper proposes a corroborative assurance approach, enabling engineers to leverage various verification and validation methods when constructing an assurance case. The main contributions of this paper are initial proposals for reusable assurance patterns based on mission patterns, and a high-level methodology for achieving a reference assurance case utilising these. An initial application of our approach is presented through a case study of road verge inspection using an autonomous robot.

The authors conducted a UK-based future study employing the Delphi method to explore the impact of emerging computing technologies on Critical National Infrastructure (CNI). The study engaged 22 domain experts specializing in software, cybersecurity , and CNI, whose roles all include forecasting technological trends and challenges. The findings propose making Internet Services a CNI sector, and suggested the weightiest concern to be human-centric challenges around the recovery from software disasters and cyberattacks. Other major concerns also related to human factors, such as attacks via operators, and errors stemming from poorly designed human-computer interfaces. The suggested mitigation strategies therefore concentrate on human-centred approaches. Key recommendations include promoting human-focused cyber resilience , and using legislation, regulation and standards to help establish it in CNI organizations.

Autonomous systems use independent decision-making with only limited human intervention to accomplish goals in complex and unpredictable environments. As the autonomy technologies that underpin them continue to advance, these systems will find their way into an increasing number of applications in an ever wider range of settings. If we are to deploy them to perform safety-critical or mission-critical roles, it is imperative that we have justified confidence in their safe and correct operation. Verification is a key process for establishing such confidence. However, autonomous systems pose challenges to existing verification practices. This paper highlights viewpoints of the Roadmap Working Group of the IEEE Robotics and Automation Society Technical Committee for Verification of Autonomous Systems, identifying these grand challenges, and providing a vision for future research efforts that will be needed to address them.

An increasing amount of research in Natural Language Inference (NLI) focuses on the application and evaluation of Large Language Models (LLMs) and their reasoning capabilities.Despite their success, however, LLMs are still prone to factual errors and inconsistencies in their explanations, offering limited control and interpretability for inference in complex domains.In this paper, we focus on ethical NLI, investigating how hybrid neurosymbolic techniques can enhance the logical validity and alignment of ethical explanations produced by LLMs.Specifically, we present an abductive-deductive framework named Logic-Explainer, which integrates LLMs with an external backward-chaining solver to refine step-wise natural language explanations and jointly verify their correctness, reduce incompleteness and minimise redundancy.An extensive empirical analysis demonstrates that Logic-Explainer can improve explanations generated via in-context learning methods and Chainof-Thought (CoT) on challenging ethical NLI tasks, while, at the same time, producing formal proofs describing and supporting models' reasoning.As ethical NLI requires commonsense reasoning to identify underlying moral violations, our results suggest the effectiveness of neuro-symbolic methods for multi-step NLI more broadly, opening new opportunities to enhance the logical consistency, reliability, and alignment of LLMs.

Natural language explanations represent a proxy for evaluating explanation-based and multi-step Natural Language Inference (NLI) models.However, assessing the validity of explanations for NLI is challenging as it typically involves the crowd-sourcing of apposite datasets, a process that is time-consuming and prone to logical errors.To address existing limitations, this paper investigates the verification and refinement of natural language explanations through the integration of Large Language Models (LLMs) and Theorem Provers (TPs).Specifically, we present a neuro-symbolic framework, named Explanation-Refiner, that integrates TPs with LLMs to generate and formalise explanatory sentences and suggest potential inference strategies for NLI.In turn, the TP is employed to provide formal guarantees on the logical validity of the explanations and to generate feedback for subsequent improvements.We demonstrate how Explanation-Refiner can be jointly used to evaluate explanatory reasoning, autoformalisation, and error correction mechanisms of state-of-the-art LLMs as well as to automatically enhance the quality of explanations of variable complexity in different domains. 1

Autonomous robotic systems systems are both safety- and security-critical, since a breach in system security may impact safety. In such critical systems, formal verification is used to model the system and verify that it obeys specific functional and safety properties. Independently, threat modelling is used to analyse and manage the cyber security threats that such systems may encounter. Both verification and threat analysis serve the purpose of ensuring that the system will be reliable, albeit from differing perspectives. In prior work, we argued that these analyses should be used to inform one another and, in this paper, we extend our previously defined methodology for security-minded verification by incorporating runtime verification. To illustrate our approach, we analyse an algorithm for sending Cooperative Awareness Messages between autonomous vehicles. Our analysis centres on identifying STRIDE security threats. We show how these can be formalised, and subsequently verified, using a combination of formal tools for static aspects, namely Promela/SPIN and Dafny, and generate runtime monitors for dynamic verification. Our approach allows us to focus our verification effort on those security properties that are particularly important and to consider safety and security in tandem, both statically and at runtime.

There is a growing interest in the use of robotics and AI in the nuclear industry, however it is important to ensure these systems are ethically grounded, trustworthy and safe. An emerging technique to address these concerns is the use of explainability. In this paper we present the results of an interview study with nuclear industry experts to explore the use of explainable intelligent systems within the field. We interviewed 16 participants with varying backgrounds of expertise, and presented two potential use cases for evaluation; a navigation scenario and a task scheduling scenario. Through an inductive thematic analysis we identified the aspects of a deployment that experts want to know from explainable systems and we outline how these associate with the folk conceptual theory of explanation, a framework in which people explain behaviours. We established that an intelligent system should explain its reasons for an action, its expectations of itself, changes in the environment that impact decision making, probabilities and the elements within them, safety implications and mitigation strategies, robot health and component failures during decision making in nuclear deployments. We determine that these factors could be explained with cause, reason, and enabling factor explanations.

Abstract BDI agents act in response to external inputs and their internal plan library. Understanding the root cause of BDI agent action is often difficult, and in this paper we present a dialogue based approach for explaining the behaviour of a BDI agent. We consider two dialogue participants who may have different views regarding the beliefs, plans and external events which drove agent action (encoded via traces). These participants make utterances which incrementally reveal their traces to each other, allowing them to identify divergences in the traces, or to conclude that their traces agree. In practice, we envision a human taking on the role of a dialogue participant, with the BDI agent itself acting as the other participant. The dialogue then facilitates explanation, understanding and debugging of BDI agent behaviour. After presenting our formalism and its properties, we describe our implementation of the system and provide an example of its use in a simple scenario.

Abstract The spread of information in a social network has received renewed interest as social media becomes an increasingly popular channel of communication. We are interested in the phenomenon of social diffusion of a piece of information in the presence of a contradicting information in the network. Specifically we explore the use of formal methods for verification in studying this phenomena. Using Monte Carlo simulation and the probabilistic model checker (PRISM) we are able to represent social networks and confirm an earlier conjecture that disseminating new information rapidly is resistant to the presence of contradicting information.

Many systems proposed for the implementation of ethical reasoning involve an encoding of user values as a set of rules or a model. We consider the question of how changes of context affect these encodings. We propose the use of a reasoning cycle, in which information about the ethical reasoner's context is imported in a logical form, and we propose that context-specific aspects of an ethical encoding be prefaced by a guard formula. This guard formula should evaluate to true when the reasoner is in the appropriate context and the relevant parts of the reasoner's rule set or model should be updated accordingly. This architecture allows techniques for the model-checking of agent-based autonomous systems to be used to verify that all contexts respect key stakeholder values. We implement this framework using the hybrid ethical reasoning agents system (HERA) and the model-checking agent programming languages (MCAPL) framework.

When applying formal verification to a system that interacts with the real world, we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The article discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies: an autonomous cruise control system and a simulation of the Mars Curiosity rover.

In this article, we describe an approach to autonomous system construction that not only supports self-awareness but also formal verification. This is based on modular construction where the key autonomous decision making is captured within a symbolically described “agent.” So, this article leads us from traditional systems architectures, via agent-based computing, to explainability, reconfigurability, and verifiability, and on to applications in robotics, autonomous vehicles, and machine ethics. Fundamentally, we consider self-awareness from an agent-based perspective. Agents are an important abstraction capturing autonomy, and we are particularly concerned with intentional, or rational, agents that expose the “intentions” of the autonomous system. Beyond being a useful abstract concept, agents also provide a practical engineering approach for building the core software in autonomous systems such as robots and vehicles. In a modular autonomous system architecture, agents of this form capture important decision making elements. Furthermore, this ability to transparently capture such decision making processes, and especially being able to expose their intentions, within an agent allows us to apply strong (formal) agent verification techniques to these systems.

Previous work on ethical machine reasoning has largely been theoretical, and where such systems have been implemented, it has, in general, been only initial proofs of principle. Here, we address the question of desirable attributes for such systems to improve their real world utility, and how controllers with these attributes might be implemented. We propose that ethically critical machine reasoning should be proactive, transparent, and verifiable. We describe an architecture where the ethical reasoning is handled by a separate layer, augmenting a typical layered control architecture, ethically moderating the robot actions. It makes use of a simulation-based internal model and supports proactive, transparent, and verifiable ethical reasoning. To do so, the reasoning component of the ethical layer uses our Python-based belief-desire-intention (BDI) implementation. The declarative logic structure of BDI facilitates both transparency, through logging of the reasoning cycle, and formal verification methods. To prove the principles of our approach, we use a case study implementation to experimentally demonstrate its operation. Importantly, it is the first such robot controller where the ethical machine reasoning has been formally verified.

Artificial intelligence (AI) systems are becoming part of our lives and societies. The more decisions such systems make for us, the more we need to ensure that the decisions they make have a positive individual and societal ethical impact. How can we estimate how good a system is at making ethical decisions? Benchmarking is used to evaluate how good a machine or a process performs with respect to industry bests. In this paper we argue that (some) ethical dilemmas can be used as benchmarks for estimating the ethical performance of an autonomous system. We advocate that an open source repository of such dilemmas should be maintained. We present a prototype of such a repository available at https://imdb. uib.no/dilemmaz/articles/all1.

Ethics by Design concerns the methods, algorithms and tools needed to endow autonomous agents with the capability to reason about the ethical aspects of their decisions, and the methods, tools and formalisms to guarantee that an agent's behavior remains within given moral bounds. In this context some questions arise: How and to what extent can agents understand the social reality in which they operate, and the other intelligences (AI, animals and humans) with which they co-exist? What are the ethical concerns in the emerging new forms of society, and how do we ensure the human dimension is upheld in interactions and decisions by autonomous agents?. But overall, the central question is: "Can we, and should we, build ethically-aware agents?" This paper presents initial conclusions from the thematic day of the same name held at PRIMA2017, on October 2017.

We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and P rism model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.

The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the behaviours of the vehicles in these platoons must be certified. This is non-trivial and goes beyond current certification requirements, for human-controlled vehicles, in that these vehicles can act autonomously . In this paper, we show how formal verification can contribute to the analysis of these new, and increasingly autonomous, systems. An appropriate overall representation for vehicle platooning is as a multi-agent system in which each agent captures the “autonomous decisions” carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the individual agent's code does not scale to the full system, and as the global system verification technique does not capture the essential verification of autonomous behaviour, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.

We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.

Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysing the behavior of a digital crowd. More precisely, we provide a formal description language for specifying digital crowds. We represent digital crowds in which the agents do not directly communicate with each other. We further show how this specification can provide the basis for sophisticated formal methods, in particular formal verification.

BDI programming languages provide a well developed route to implementing intelligent agents. However, as such agents are increasingly being used in physical environments their treatment of external actions needs to be improved. In this paper we outline a mechanism for handling actions which have durations and failures.

In this paper, we show that the flexible model-checking of multi-agent systems, implemented using agent-oriented programming languages, is viable thus paving the way for the construction of verifiably correct applications of autonomous agents and multi-agent systems. Model checking experiments were carried out on AJPF (agent JPF), our extension of Java PathFinder that incorporates the agent infrastructure layer, our unifying framework for agent programming languages. In our approach, properties are specified in a temporal language extended with (shallow) agent-related modalities. The framework then allows the verification of programs written in a variety of agent programming languages, thus removing the need for individual languages to implement their own verification framework. It even allows the verification of multi-agent systems comprised of agents developed in a variety of different (agent) programming languages. As an example, we also provide model checking results for the verification of a multi-agent system implementing a well-known task sharing protocol.