arXiv subjects

John Rushby

Publications and source records attributed to John Rushby.

15 recordsLinked to original sources

arXiv2026

Quantifying Confidence in Assurance 2.0 Arguments

Confidence is central to safety and assurance cases: how much confidence a decision requires and how much the argument actually provides are both important questions. We present a new method for assessing probabilistic confidence in assurance case arguments that is simple, systematic and sound. It exploits the ways claims are decomposed in a structured argument and provides different approaches according to the different degrees of (in)dependence and diversity among subclaims and the way they eliminate concerns that undermine confidence in their parent claims. The method uses only elementary probabilistic constructions that are well-known in other contexts (e.g., Frechet bounds) but we interpret and apply them in a manner that is specifically focused on assurance arguments and requires no background in probabilistic analysis. We show that the method is not susceptible to the counterexamples that Graydon and Holloway exhibit for other approaches to confidence and we recommend it as an additional tool in evaluation of Assurance 2.0 arguments. The primary evaluation criteria for Assurance 2.0 remain logical indefeasibility and dialectical examination, but probabilistic assessment can be useful in evaluating cost/confidence tradeoffs for different risk levels, and the overall balance of confidence across a structured argument.

cs.SE↗

arXiv2025

Where AI Assurance Might Go Wrong: Initial lessons from engineering of critical systems

We draw on our experience working on system and software assurance and evaluation for systems important to society to summarise how safety engineering is performed in traditional critical systems, such as aircraft flight control. We analyse how this critical systems perspective might support the development and implementation of AI Safety Frameworks. We present the analysis in terms of: system engineering, safety and risk analysis, and decision analysis and support. We consider four key questions: What is the system? How good does it have to be? What is the impact of criticality on system development? and How much should we trust it? We identify topics worthy of further discussion. In particular, we are concerned that system boundaries are not broad enough, that the tolerability and nature of the risks are not sufficiently elaborated, and that the assurance methods lack theories that would allow behaviours to be adequately assured. We advocate the use of assurance cases based on Assurance 2.0 to support decision making in which the criticality of the decision as well as the criticality of the system are evaluated. We point out the orders of magnitude difference in confidence needed in critical rather than everyday systems and how everyday techniques do not scale in rigour. Finally we map our findings in detail to two of the questions posed by the FAISC organisers and we note that the engineering of critical systems has evolved through open and diverse discussion. We hope that topics identified here will support the post-FAISC dialogues.

cs.CY↗

arXiv2024

Confidence in Assurance 2.0 Cases

An assurance case should provide justifiable confidence in the truth of a claim about some critical property of a system or procedure, such as safety or security. We consider how confidence can be assessed in the rigorous approach we call Assurance 2.0. Our goal is indefeasible confidence and we approach it from four different perspectives: logical soundness, probabilistic assessment, dialectical examination, and residual risks.

cs.SE↗

arXiv2024

Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP

Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance arguments. In prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case.

cs.LO↗

arXiv2024

Assurance of AI Systems From a Dependability Perspective

We outline the principles of classical assurance for computer-based systems that pose significant risks. We then consider application of these principles to systems that employ Artificial Intelligence (AI) and Machine Learning (ML). A key element in this "dependability" perspective is a requirement for thorough understanding of the behavior of critical components, and this is considered infeasible for AI and ML. Hence the dependability perspective aims to minimize trust in AI and ML elements by using "defense in depth" with a hierarchy of less complex systems, some of which may be highly assured conventionally engineered components, to "guard" them. This may be contrasted with the "trustworthy" perspective that seeks to apply assurance to the AI and ML elements themselves. In cyber-physical and many other systems, it is difficult to provide guards that do not depend on AI and ML to perceive their environment (e.g., vehicles sharing the road with a self-driving car), so both perspectives are needed and there is a continuum or spectrum between them. We focus on architectures toward the dependability end of the continuum and invite others to consider additional points along the spectrum. For guards that require perception using AI and ML, we examine ways to minimize the trust placed in these elements; they include diversity, defense in depth, explanations, and micro-ODDs. We also examine methods to enforce acceptable behavior, given a model of the world. These include classical cyber-physical calculations and envelopes, and normative rules based on overarching principles, constitutions, ethics, or reputation. We apply our perspective to autonomous systems, AI systems for specific functions, general-purpose AI such as Large Language Models (LLMs), and Artificial General Intelligence (AGI), and we propose current best practice and conclude with a fourfold agenda for research.

cs.AI↗

arXiv2024

Defeaters and Eliminative Argumentation in Assurance 2.0

A traditional assurance case employs a positive argument in which reasoning steps, grounded on evidence and assumptions, sustain a top claim that has external significance. Human judgement is required to check the evidence, the assumptions, and the narrative justifications for the reasoning steps; if all are assessed good, then the top claim can be accepted. A valid concern about this process is that human judgement is fallible and prone to confirmation bias. The best defense against this concern is vigorous and skeptical debate and discussion in the manner of a dialectic or Socratic dialog. There is merit in recording aspects of this discussion for the benefit of subsequent developers and assessors. Defeaters are a means doing this: they express doubts about aspects of the argument and can be developed into subcases that confirm or refute the doubts, and can record them as documentation to assist future consideration. This report describes how defeaters, and multiple levels of defeaters, should be represented and assessed in Assurance 2.0 and its Clarissa/ASCE tool support. These mechanisms also support eliminative argumentation, which is a contrary approach to assurance, favored by some, that uses a negative argument to refute all reasons why the top claim could be false.

cs.AI↗

arXiv2023

On Computational Mechanisms for Shared Intentionality, and Speculation on Rationality and Consciousness

A singular attribute of humankind is our ability to undertake novel, cooperative behavior, or teamwork. This requires that we can communicate goals, plans, and ideas between the brains of individuals to create shared intentionality. Using the information processing model of David Marr, I derive necessary characteristics of basic mechanisms to enable shared intentionality between prelinguistic computational agents and indicate how these could be implemented in present-day AI-based robots. More speculatively, I suggest the mechanisms derived by this thought experiment apply to humans and extend to provide explanations for human rationality and aspects of intentional and phenomenal consciousness that accord with observation. This yields what I call the Shared Intentionality First Theory (SIFT) for rationality and consciousness. The significance of shared intentionality has been recognized and advocated previously, but typically from a sociological or behavioral point of view. SIFT complements prior work by applying a computer science perspective to the underlying mechanisms.

cs.AI↗

arXiv2022

Technology and Consciousness

We report on a series of eight workshops held in the summer of 2017 on the topic "technology and consciousness." The workshops covered many subjects but the overall goal was to assess the possibility of machine consciousness, and its potential implications. In the body of the report, we summarize most of the basic themes that were discussed: the structure and function of the brain, theories of consciousness, explicit attempts to construct conscious machines, detection and measurement of consciousness, possible emergence of a conscious technology, methods for control of such a technology and ethical considerations that might be owed to it. An appendix outlines the topics of each workshop and provides abstracts of the talks delivered. Update: Although this report was published in 2018 and the workshops it is based on were held in 2017, recent events suggest that it is worth bringing forward. In particular, in the Spring of 2022, a Google engineer claimed that LaMDA, one of their "large language models" is sentient or even conscious. This provoked a flurry of commentary in both the scientific and popular press, some of it interesting and insightful, but almost all of it ignorant of the prior consideration given to these topics and the history of research into machine consciousness. Thus, we are making a lightly refreshed version of this report available in the hope that it will provide useful background to the current debate and will enable more informed commentary. Although this material is five years old, its technical points remain valid and up to date, but we have "refreshed" it by adding a few footnotes highlighting recent developments.

q-bio.NC↗

arXiv2022

Inferring and Conveying Intentionality: Beyond Numerical Rewards to Logical Intentions

Shared intentionality is a critical component in developing conscious AI agents capable of collaboration, self-reflection, deliberation, and reasoning. We formulate inference of shared intentionality as an inverse reinforcement learning problem with logical reward specifications. We show how the approach can infer task descriptions from demonstrations. We also extend our approach to actively convey intentionality. We demonstrate the approach on a simple grid-world example.

cs.AI↗

arXiv2022

A Mechanically Assisted Examination of Vacuity and Question Begging in Anselm's Ontological Argument

I use mechanized verification to examine several first- and higher-order formalizations of Anselm's Ontological Argument against the charge of begging the question. I propose three different but related criteria for a premise to beg the question in fully formal proofs and find that one or another applies to all the formalizations examined. I also show that all these formalizations entail variants that are vacuous, in the sense that they apply no interpretation to "than which there is no greater" and are therefore vulnerable to Gaunilo's refutation. My purpose is to demonstrate that mechanized verification provides an effective and reliable technique to perform these analyses; readers may decide whether the forms of question begging and vacuity so identified affect their interest in the Argument or its various formalizations. This version updates the paper that originally appeared as Chapter 13 in "Beyond Faith and Rationality: Essays on Logic, Religion and Philosophy" published by Springer to respond to criticisms by Oppenheimer and Zalta.

cs.LO↗

arXiv2022

Mechanized Analysis of Anselm's Modal Ontological Argument

We use a mechanized verification system, PVS, to examine the argument from Anselm's Proslogion Chapter III, the so-called "Modal Ontological Argument." We consider several published formalizations for the argument and show they are all essentially similar. Furthermore, we show that the argument is trivial once the modal axioms are taken into account. This work is an illustration of computational philosophy and, in addition, shows how these methods can help detect and rectify errors in modal reasoning. This is a minor update with better typesetting and some small addenda to a paper published in the International Journal for Philosophy of Religion, vol. 89, pp. 135--152, April 2021.

cs.LO↗

arXiv2022

PVS Embeddings of Propositional and Quantified Modal Logic

Modal logics allow reasoning about various modes of truth: for example, what it means for something to be possibly true, or to know that something is true as opposed to merely believing it. This report describes embeddings of propositional and quantified modal logic in the PVS verification system. The resources of PVS allow this to be done in an attractive way that supports much of the standard syntax of modal logic, while providing effective automation. The report introduces and formally specifies and verifies several standard topics in modal logic such as relationships between the standard modal axioms and properties of the accessibility relation, and attributes of the Barcan Formula and its converse in both constant and varying domains.

cs.LO↗

arXiv2022

Assessing Confidence with Assurance 2.0

An assurance case is intended to provide justifiable confidence in the truth of its top claim, which typically concerns safety or security. A natural question is then "how much" confidence does the case provide? We argue that confidence cannot be reduced to a single attribute or measurement. Instead, we suggest it should be based on attributes that draw on three different perspectives: positive, negative, and residual doubts. Positive Perspectives consider the extent to which the evidence and overall argument of the case combine to make a positive statement justifying belief in its claims. We set a high bar for justification, requiring it to be indefeasible. The primary positive measure for this is soundness, which interprets the argument as a logical proof. Confidence in evidence can be expressed probabilistically and we use confirmation measures to ensure that the "weight" of evidence crosses some threshold. In addition, probabilities can be aggregated from evidence through the steps of the argument using probability logics to yield what we call probabilistic valuations for the claims. Negative Perspectives record doubts and challenges to the case, typically expressed as defeaters, and their exploration and resolution. Assurance developers must guard against confirmation bias and should vigorously explore potential defeaters as they develop the case, and should record them and their resolution to avoid rework and to aid reviewers. Residual Doubts: the world is uncertain so not all potential defeaters can be resolved. We explore risks and may deem them acceptable or unavoidable. It is crucial however that these judgments are conscious ones and that they are recorded in the assurance case. This report examines the perspectives in detail and indicates how Clarissa, our prototype toolset for Assurance 2.0, assists in their evaluation.

cs.AI↗

arXiv2021

Assurance 2.0: A Manifesto

System assurance is confronted by significant challenges. Some of these are new, for example, autonomous systems with major functions driven by machine learning and AI, and ultra-rapid system development, while others are the familiar, persistent issues of the need for efficient, effective and timely assurance. Traditional assurance is seen as a brake on innovation and often costly and time consuming. We therefore propose a modernized framework, Assurance 2.0, as an enabler that supports innovation and continuous incremental assurance. Perhaps unexpectedly, it does so by making assurance more rigorous, with increased focus on the reasoning and evidence employed, and explicit identification of defeaters and counterevidence.

cs.SE↗

arXiv2014

Evaluating the Assessment of Software Fault-Freeness

We propose to validate experimentally a theory of software certification that proceeds from assessment of confidence in fault-freeness (due to standards) to conservative prediction of failure-free operation.

cs.SE↗