We present a multi-modal Logic for Functional Responsibility (LFR) to model and check actual, capacity, and outcome responsibility of agents within hybrid computational systems with a user level ontology. For AI systems, this allows one to represent and trace responsibility of output to training data, training engine, trained model, policies and end user operations. We exemplify the system with an example of image generation.

A common practice of ML systems development concerns the training of the same model under different data sets, and the use of the same (training and test) sets for different learning models. The first case is a desirable practice for identifying high quality and unbiased training conditions. The latter case coincides with the search for optimal models under a common dataset for training. These differently obtained systems have been considered akin to copies. In the quest for responsible AI, a legitimate but hardly investigated question is how to verify that trustworthiness is preserved by copies. In this paper we introduce a calculus to model and verify probabilistic complex queries over data and define four distinct notions: Justifiably, Equally, Weakly and Almost Trustworthy which can be checked analysing the (partial) behaviour of the copy with respect to its original. We provide a study of the relations between these notions of trustworthiness, and how they compose with each other and under logical operations. The aim is to offer a computational tool to check the trustworthiness of possibly complex systems copied from an original whose behavour is known.

Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs. CTLF adopts a counting worlds semantics where each world represents a possible output at a given step in the generation process and introduces modal operators that allow us to verify whether the current output series respects an intended probability distribution over a protected attribute, to predict the likelihood of remaining within acceptable bounds as new outputs are generated, and to determine how many outputs are needed to remove in order to restore fairness. We illustrate the framework on a toy example of biased image generation, showing how CTLF formulas can express concrete fairness properties at different points in the output series.

In the present work, we develop a novel information-theoretic and logic-based approach to data bias in Machine Learning predictions and show its relevance in the specific context of fairness evaluation. We frame predictions made on biased data as Ulam games, which formalise key aspects of data-driven inference, and from which a variation of the rational non-monotonic consequence relation can be defined. We investigate this framework to model how differential levels of noise in input features impact Machine Learning predictions. To the best of our knowledge, this is the first game-theoretic formalisation of ML unfairness.

Logics of information have abounded in the last two decades. A major point of conceptual and formal difference among various such logics has been represented by the interaction they model between information and truth. Floridi’s logic of ‘being informed’ defines semantic information as the truthful basis for knowledge; Allo’s revisitation of it restraints this relation from the agent’s perspective; Primiero’s logic for ‘becoming informed’ focuses on information as denoting assertibility conditions, whereas truth is only granted by their verification. The present article extends the debate to include aspects originating in semiotics and pragmatics to the study of information, in particular with respect to computational systems. We stress the role of the different informational users in exchanging and determining validity conditions for information and formalize a weighted multi-agent modal logic for ‘using information’. We present both a semantics and axiomatic systems, prove standard meta-theoretical results and show which fragments correspond to different interpretations of use of the computational systems under interpretation.

In this article we propose an extension to the typed natural deduction calculus TNDPQ to model verification of counterfactual fairness in probabilistic classifiers. This is obtained formulating specific structural conditions for causal labels and checking that evaluation is robust under their variation.

In this article we propose an extension to the typed natural deduction calculus TNDPQ to model verification of individual fairness and intersectionality in probabilistic classifiers. Their interpretation is obtained by formulating specific conditions for the application of the structural rule of Weakening. Such restrictions are given by causal labels used to check for conditional independence between protected and target variables.

In this paper we present the probabilistic typed natural deduction calculus TPTND, designed to reason about and derive trustworthiness properties of probabilistic computational processes, like those underlying current AI applications. Derivability in TPTND is interpreted as the process of extracting
samples of possibly complex outputs with a certain frequency from a given categorical distribution. We formalize trust for such outputs as a form of hypothesis testing on the distance between such frequency and the intended probability. The main advantage of the calculus is to render such notion of trustworthiness checkable. We present a computational semantics for the terms over which we reason and then the semantics of TPTND, where logical operators as well as a Trust operator are defined through introduction and elimination rules. We illustrate structural and metatheoretical properties, with particular focus on the ability to establish under which term evaluations and logical rules applications the notion of trustworthiness can be preserved.

Machine Learning (ML) systems, whether predictive or generative, not only reproduce biases and stereotypes but,even more worryingly, amplify them. Strategies for bias detection and mitigation typically focus on either ex post or ex ante approaches, but are always limited to two steps analyses. In this paper, we introduce the notion of Bias Amplification Chain (BAC) as a series of steps in which bias may be amplified during the design, development and deployment phases of trained models. We provide an application to such notion in the credit scoring setting and a quantitative analysis through the BRIO tool.

The widespread emergence of phenomena of bias is certainly among the most adverse impacts of new data-intensive sciences and technologies. The causes of such undesirable behaviours must be traced back to data themselves, as well as to certain design choices of machine learning algorithms. The task of modelling bias from a logical point of view requires to extend the vast family of defeasible logics and logics for uncertain reasoning with ones that capture some few, fundamental properties of biased predictions. However, a logically grounded approach to machine learning fairness is still at early stages in the literature. In this paper, we discuss current approaches to the topic, formulate general logical desiderata for logics to reason with and about bias, and provide a novel approach

We present a method for quantitative, in-depth analyses of fairness issues in AI systems with an application to credit scoring. To this aim we use BRIO, a tool for the evaluation of AI systems with respect to social unfairness and, more in general, ethically undesirable behaviours. It features a model-agnostic bias detection module, presented in [CDG +23], to which a full-fledged unfairness risk evaluation module is added. As a case study, we focus on the context of credit scoring, analysing the UCI German Credit Dataset [Hof94a]. We apply the BRIO fairness metrics to several, socially sensitive attributes featured in the German Credit Dataset, quantifying fairness across various demographic segments, with the aim of identifying potential sources of bias and discrimination in a credit scoring model. We conclude by combining our results with a revenue analysis.

Some computational phenomena rely essentially on pragmatic considerations, and seem to undermine the independence of the specification from the implementation. These include software development, deviant uses, esoteric languages and recent data-driven applications. To account for them, the interaction between pragmatics, epistemology and ontology in computational artefacts seems essential, indicating the need to recover the role of the language metaphor. We propose a User Levels (ULs) structure as a pragmatic complement to the Levels of Abstraction (LoAs)-based structure defining the ontology and epistemology of computational artefacts. ULs identify a flexible hierarchy in which users bear their own semantic and normative requirements, possibly competing with the logical specification. We formulate a notion of computational act intended in its pragmatic sense, alongside pragmatic versions of implementation and correctness.