-
The Technology of Outrage: Bias in Artificial Intelligence
Authors:
Will Bridewell,
Paul F. Bello,
Selmer Bringsjord
Abstract:
Artificial intelligence and machine learning are increasingly used to offload decision making from people. In the past, one of the rationales for this replacement was that machines, unlike people, can be fair and unbiased. Evidence suggests otherwise. We begin by entertaining the ideas that algorithms can replace people and that algorithms cannot be biased. Taken as axioms, these statements quickl…
▽ More
Artificial intelligence and machine learning are increasingly used to offload decision making from people. In the past, one of the rationales for this replacement was that machines, unlike people, can be fair and unbiased. Evidence suggests otherwise. We begin by entertaining the ideas that algorithms can replace people and that algorithms cannot be biased. Taken as axioms, these statements quickly lead to absurdity. Spurred on by this result, we investigate the slogans more closely and identify equivocation surrounding the word 'bias.' We diagnose three forms of outrage-intellectual, moral, and political-that are at play when people react emotionally to algorithmic bias. Then we suggest three practical approaches to addressing bias that the AI community could take, which include clarifying the language around bias, developing new auditing methods for intelligent systems, and building certain capabilities into these systems. We conclude by offering a moral regarding the conversations about algorithmic bias that may transfer to other areas of artificial intelligence.
△ Less
Submitted 25 September, 2024;
originally announced September 2024.
-
AI Can Stop Mass Shootings, and More
Authors:
Selmer Bringsjord,
Naveen Sundar Govindarajulu,
Michael Giancola
Abstract:
We propose to build directly upon our longstanding, prior r&d in AI/machine ethics in order to attempt to make real the blue-sky idea of AI that can thwart mass shootings, by bringing to bear its ethical reasoning. The r&d in question is overtly and avowedly logicist in form, and since we are hardly the only ones who have established a firm foundation in the attempt to imbue AI's with their own et…
▽ More
We propose to build directly upon our longstanding, prior r&d in AI/machine ethics in order to attempt to make real the blue-sky idea of AI that can thwart mass shootings, by bringing to bear its ethical reasoning. The r&d in question is overtly and avowedly logicist in form, and since we are hardly the only ones who have established a firm foundation in the attempt to imbue AI's with their own ethical sensibility, the pursuit of our proposal by those in different methodological camps should, we believe, be considered as well. We seek herein to make our vision at least somewhat concrete by anchoring our exposition to two simulations, one in which the AI saves the lives of innocents by locking out a malevolent human's gun, and a second in which this malevolent agent is allowed by the AI to be neutralized by law enforcement. Along the way, some objections are anticipated, and rebutted.
△ Less
Submitted 5 February, 2021;
originally announced February 2021.
-
On Quantified Modal Theorem Proving for Modeling Ethics
Authors:
Naveen Sundar Govindarajulu,
Selmer Bringsjord,
Matthew Peveler
Abstract:
In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Meeting these requirements necessitates investigation…
▽ More
In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Meeting these requirements necessitates investigation of new approaches for proof automation. Particularly, a quantified modal logic, the deontic cognitive event calculus (DCEC), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DCEC, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation for DCEC.
△ Less
Submitted 30 December, 2019;
originally announced December 2019.
-
Learning $\textit{Ex Nihilo}$
Authors:
Selmer Bringsjord,
Naveen Sundar Govindarajulu
Abstract:
This paper introduces, philosophically and to a degree formally, the novel concept of learning $\textit{ex nihilo}$, intended (obviously) to be analogous to the concept of creation $\textit{ex nihilo}$. Learning $\textit{ex nihilo}$ is an agent's learning "from nothing," by the suitable employment of schemata for deductive and inductive reasoning. This reasoning must be in machine-verifiable acco…
▽ More
This paper introduces, philosophically and to a degree formally, the novel concept of learning $\textit{ex nihilo}$, intended (obviously) to be analogous to the concept of creation $\textit{ex nihilo}$. Learning $\textit{ex nihilo}$ is an agent's learning "from nothing," by the suitable employment of schemata for deductive and inductive reasoning. This reasoning must be in machine-verifiable accord with a formal proof/argument theory in a $\textit{cognitive calculus}$ (i.e., roughly, an intensional higher-order multi-operator quantified logic), and this reasoning is applied to percepts received by the agent, in the context of both some prior knowledge, and some prior and current interests. Learning $\textit{ex nihilo}$ is a challenge to contemporary forms of ML, indeed a severe one, but the challenge is offered in the spirt of seeking to stimulate attempts, on the part of non-logicist ML researchers and engineers, to collaborate with those in possession of learning-$\textit{ex nihilo}$ frameworks, and eventually attempts to integrate directly with such frameworks at the implementation level. Such integration will require, among other things, the symbiotic interoperation of state-of-the-art automated reasoners and high-expressivity planners, with statistical/connectionist ML technology.
△ Less
Submitted 21 April, 2019; v1 submitted 4 March, 2019;
originally announced March 2019.
-
Toward the Engineering of Virtuous Machines
Authors:
Naveen Sundar Govindarajulu,
Selmer Bringsjord,
Rikhiya Ghosh
Abstract:
While various traditions under the 'virtue ethics' umbrella have been studied extensively and advocated by ethicists, it has not been clear that there exists a version of virtue ethics rigorous enough to be a target for machine ethics (which we take to include the engineering of an ethical sensibility in a machine or robot itself, not only the study of ethics in the humans who might create artific…
▽ More
While various traditions under the 'virtue ethics' umbrella have been studied extensively and advocated by ethicists, it has not been clear that there exists a version of virtue ethics rigorous enough to be a target for machine ethics (which we take to include the engineering of an ethical sensibility in a machine or robot itself, not only the study of ethics in the humans who might create artificial agents). We begin to address this by presenting an embryonic formalization of a key part of any virtue-ethics theory: namely, the learning of virtue by a focus on exemplars of moral virtue. Our work is based in part on a computational formal logic previously used to formally model other ethical theories and principles therein, and to implement these models in artificial agents.
△ Less
Submitted 30 December, 2018; v1 submitted 7 December, 2018;
originally announced December 2018.
-
Tentacular Artificial Intelligence, and the Architecture Thereof, Introduced
Authors:
Selmer Bringsjord,
Naveen Sundar Govindarajulu,
Atriya Sen,
Matthew Peveler,
Biplav Srivastava,
Kartik Talamadupula
Abstract:
We briefly introduce herein a new form of distributed, multi-agent artificial intelligence, which we refer to as "tentacular." Tentacular AI is distinguished by six attributes, which among other things entail a capacity for reasoning and planning based in highly expressive calculi (logics), and which enlists subsidiary agents across distances circumscribed only by the reach of one or more given ne…
▽ More
We briefly introduce herein a new form of distributed, multi-agent artificial intelligence, which we refer to as "tentacular." Tentacular AI is distinguished by six attributes, which among other things entail a capacity for reasoning and planning based in highly expressive calculi (logics), and which enlists subsidiary agents across distances circumscribed only by the reach of one or more given networks.
△ Less
Submitted 13 October, 2018;
originally announced October 2018.
-
Toward Formalizing Teleportation of Pedagogical Artificial Agents
Authors:
John Angel,
Naveen Sundar Govindarajulu,
Selmer Bringsjord
Abstract:
Our paradigm for the use of artificial agents to teach requires among other things that they persist through time in their interaction with human students, in such a way that they "teleport" or "migrate" from an embodiment at one time t to a different embodiment at later time t'. In this short paper, we report on initial steps toward the formalization of such teleportation, in order to enable an o…
▽ More
Our paradigm for the use of artificial agents to teach requires among other things that they persist through time in their interaction with human students, in such a way that they "teleport" or "migrate" from an embodiment at one time t to a different embodiment at later time t'. In this short paper, we report on initial steps toward the formalization of such teleportation, in order to enable an overseeing AI system to establish, mechanically, and verifiably, that the human students in question will likely believe that the very same artificial agent has persisted across such times despite the different embodiments.
△ Less
Submitted 10 April, 2018;
originally announced April 2018.
-
Counterfactual Conditionals in Quantified Modal Logic
Authors:
Naveen Sundar Govindarajulu,
Selmer Bringsjord
Abstract:
We present a novel formalization of counterfactual conditionals in a quantified modal logic. Counterfactual conditionals play a vital role in ethical and moral reasoning. Prior work has shown that moral reasoning systems (and more generally, theory-of-mind reasoning systems) should be at least as expressive as first-order (quantified) modal logic (QML) to be well-behaved. While existing work on mo…
▽ More
We present a novel formalization of counterfactual conditionals in a quantified modal logic. Counterfactual conditionals play a vital role in ethical and moral reasoning. Prior work has shown that moral reasoning systems (and more generally, theory-of-mind reasoning systems) should be at least as expressive as first-order (quantified) modal logic (QML) to be well-behaved. While existing work on moral reasoning has focused on counterfactual-free QML moral reasoning, we present a fully specified and implemented formal system that includes counterfactual conditionals. We validate our model with two projects. In the first project, we demonstrate that our system can be used to model a complex moral principle, the doctrine of double effect. In the second project, we use the system to build a data-set with true and false counterfactuals as licensed by our theory, which we believe can be useful for other researchers. This project also shows that our model can be computationally feasible.
△ Less
Submitted 2 November, 2017; v1 submitted 11 October, 2017;
originally announced October 2017.
-
Toward Cognitive and Immersive Systems: Experiments in a Cognitive Microworld
Authors:
Matthew Peveler,
Naveen Sundar Govindarajulu,
Selmer Bringsjord,
Atriya Sen,
Biplav Srivastava,
Kartik Talamadupula,
Hui Su
Abstract:
As computational power has continued to increase, and sensors have become more accurate, the corresponding advent of systems that are at once cognitive and immersive has arrived. These \textit{cognitive and immersive systems} (CAISs) fall squarely into the intersection of AI with HCI/HRI: such systems interact with and assist the human agents that enter them, in no small part because such systems…
▽ More
As computational power has continued to increase, and sensors have become more accurate, the corresponding advent of systems that are at once cognitive and immersive has arrived. These \textit{cognitive and immersive systems} (CAISs) fall squarely into the intersection of AI with HCI/HRI: such systems interact with and assist the human agents that enter them, in no small part because such systems are infused with AI able to understand and reason about these humans and their knowledge, beliefs, goals, communications, plans, etc. We herein explain our approach to engineering CAISs. We emphasize the capacity of a CAIS to develop and reason over a `theory of the mind' of its human partners. This capacity entails that the AI in question has a sophisticated model of the beliefs, knowledge, goals, desires, emotions, etc.\ of these humans. To accomplish this engineering, a formal framework of very high expressivity is needed. In our case, this framework is a \textit{cognitive event calculus}, a particular kind of quantified multi-operator modal logic, and a matching high-expressivity automated reasoner and planner. To explain, advance, and to a degree validate our approach, we show that a calculus of this type satisfies a set of formal requirements, and can enable a CAIS to understand a psychologically tricky scenario couched in what we call the \textit{cognitive polysolid framework} (CPF). We also formally show that a room that satisfies these requirements can have a useful property we term \emph{expectation of usefulness}. CPF, a sub-class of \textit{cognitive microworlds}, includes machinery able to represent and plan over not merely blocks and actions (such as seen in the primitive `blocks worlds' of old), but also over agents and their mental attitudes about both other agents and inanimate objects.
△ Less
Submitted 18 December, 2018; v1 submitted 14 September, 2017;
originally announced September 2017.
-
Strength Factors: An Uncertainty System for a Quantified Modal Logic
Authors:
Naveen Sundar Govindarajulu,
Selmer Bringsjord
Abstract:
We present a new system S for handling uncertainty in a quantified modal logic (first-order modal logic). The system is based on both probability theory and proof theory. The system is derived from Chisholm's epistemology. We concretize Chisholm's system by grounding his undefined and primitive (i.e. foundational) concept of reasonablenes in probability and proof theory. S can be useful in systems…
▽ More
We present a new system S for handling uncertainty in a quantified modal logic (first-order modal logic). The system is based on both probability theory and proof theory. The system is derived from Chisholm's epistemology. We concretize Chisholm's system by grounding his undefined and primitive (i.e. foundational) concept of reasonablenes in probability and proof theory. S can be useful in systems that have to interact with humans and provide justifications for their uncertainty. As a demonstration of the system, we apply the system to provide a solution to the lottery paradox. Another advantage of the system is that it can be used to provide uncertainty values for counterfactual statements. Counterfactuals are statements that an agent knows for sure are false. Among other cases, counterfactuals are useful when systems have to explain their actions to users. Uncertainties for counterfactuals fall out naturally from our system.
Efficient reasoning in just simple first-order logic is a hard problem. Resolution-based first-order reasoning systems have made significant progress over the last several decades in building systems that have solved non-trivial tasks (even unsolved conjectures in mathematics). We present a sketch of a novel algorithm for reasoning that extends first-order resolution.
Finally, while there have been many systems of uncertainty for propositional logics, first-order logics and propositional modal logics, there has been very little work in building systems of uncertainty for first-order modal logics. The work described below is in progress; and once finished will address this lack.
△ Less
Submitted 28 May, 2018; v1 submitted 30 May, 2017;
originally announced May 2017.
-
On Automating the Doctrine of Double Effect
Authors:
Naveen Sundar Govindarajulu,
Selmer Bringsjord
Abstract:
The doctrine of double effect ($\mathcal{DDE}$) is a long-studied ethical principle that governs when actions that have both positive and negative effects are to be allowed. The goal in this paper is to automate $\mathcal{DDE}$. We briefly present $\mathcal{DDE}$, and use a first-order modal logic, the deontic cognitive event calculus, as our framework to formalize the doctrine. We present formali…
▽ More
The doctrine of double effect ($\mathcal{DDE}$) is a long-studied ethical principle that governs when actions that have both positive and negative effects are to be allowed. The goal in this paper is to automate $\mathcal{DDE}$. We briefly present $\mathcal{DDE}$, and use a first-order modal logic, the deontic cognitive event calculus, as our framework to formalize the doctrine. We present formalizations of increasingly stronger versions of the principle, including what is known as the doctrine of triple effect. We then use our framework to simulate successfully scenarios that have been used to test for the presence of the principle in human subjects. Our framework can be used in two different modes: One can use it to build $\mathcal{DDE}$-compliant autonomous systems from scratch, or one can use it to verify that a given AI system is $\mathcal{DDE}$-compliant, by applying a $\mathcal{DDE}$ layer on an existing system or model. For the latter mode, the underlying AI system can be built using any architecture (planners, deep neural networks, bayesian networks, knowledge-representation systems, or a hybrid); as long as the system exposes a few parameters in its model, such verification is possible. The role of the $\mathcal{DDE}$ layer here is akin to a (dynamic or static) software verifier that examines existing software modules. Finally, we end by presenting initial work on how one can apply our $\mathcal{DDE}$ layer to the STRIPS-style planning model, and to a modified POMDP model.This is preliminary work to illustrate the feasibility of the second mode, and we hope that our initial sketches can be useful for other researchers in incorporating DDE in their own frameworks.
△ Less
Submitted 17 July, 2017; v1 submitted 27 March, 2017;
originally announced March 2017.
-
Proof Verification Can Be Hard!
Authors:
Naveen Sundar Govindarajulu,
Selmer Bringsjord
Abstract:
The generally accepted wisdom in computational circles is that pure proof verification is a solved problem and that the computationally hard elements and fertile areas of study lie in proof discovery. This wisdom presumably does hold for conventional proof systems such as first-order logic with a standard proof calculus such as natural deduction or resolution. But this folk belief breaks down when…
▽ More
The generally accepted wisdom in computational circles is that pure proof verification is a solved problem and that the computationally hard elements and fertile areas of study lie in proof discovery. This wisdom presumably does hold for conventional proof systems such as first-order logic with a standard proof calculus such as natural deduction or resolution. But this folk belief breaks down when we consider more user-friendly/powerful inference rules. One such rule is the restricted ω-rule, which is not even semi-decidable when added to a standard proof calculus of a nice theory. While presumably not a novel result, we feel that the hardness of proof verification is under-appreciated in most communities that deal with proofs. A proof-sketch follows.
△ Less
Submitted 25 March, 2017;
originally announced March 2017.
-
P=NP
Authors:
Selmer Bringsjord,
Joshua Taylor
Abstract:
We claim to resolve the P=?NP problem via a formal argument for P=NP.
We claim to resolve the P=?NP problem via a formal argument for P=NP.
△ Less
Submitted 28 June, 2004;
originally announced June 2004.
