ABSTRACT. The increasingly pervasive use of big data and machine learning is raising various ethical issues, in particular privacy and fairness.In this talk, I will discuss some frameworks to understand and mitigate the issues, focusing on iterative methods coming from information theory and statistics.In the area of privacy protection, differential privacy (DP) and its variants are the most successful approaches to date. One of the fundamental issues of DP is how to reconcile the loss of information that it implies with the need to pr eserve the utility of the data. In this regard, a useful tool to recover utility is the Iterative Bayesian Update (IBU), an instance of the famous Expectation-Maximization method from Statistics. I will show that the IBU, combined with the metric version of DP, outperforms the state-of-the art, which is based on algebraic methods combined with the Randomized Response mechanism, widely adopted by the Big Tech industry (Google, Apple, Amazon, ...). Furthermore I will discuss a surprising duality between the IBU and one of the methods used to enhance metric DP, that is the Blahut-Arimoto algorithm from Rate-Distortion Theory. Finally, I will discuss the issue of biased decisions in machine learning, and will show that the IBU can be applied also in this domain to ensure a fairer treatment of disadvantaged groups.

Brief Bio:Catuscia Palamidessi is Director of Research at INRIA Saclay (since 2002), where she leads the team COMETE. She has been Full Professor at the University of Genova, Italy (1994-1997) and Penn State University, USA (1998-2002). Palamidessi's research interests include Privacy, Machine Learning, Fairness, Secure Information Flow, Formal Methods, and Concurrency. In 2019 she has obtained an ERC advanced grant to conduct research on Privacy and Machine Learning. She has been PC chair of various conferences including LICS and ICALP, and PC member of more than 120 international conferences. She is in the Editorial board of several journals, including the IEEE Transactions in Dependable and Secure Computing, Mathematical Structures in Computer Science, Theoretics, the Journal of Logical and Algebraic Methods in Programming and Acta Informatica. She is serving in the Executive Committee of ACM SIGLOG, CONCUR, and CSL.

http://www.lix.polytechnique.fr/~catuscia/

ABSTRACT. Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a $\lambda$-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations --- a recently introduced notion of higher-order distance between programs --- both pure and effectful, bringing them back to a common picture with traditional ones.

ABSTRACT. We explore the possibility of extending Mardare et al.'s quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results which clearly delineate to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.

ABSTRACT. We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper's recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between "higher" and "lower" security, and second to verify the computational adequacy of our sheaf semantics with respect to a version of Abadi et al.'s dependency core calculus to which we have added a construct for declassifying termination channels.

ABSTRACT. Matching algorithms are often central sub-routines in many areas of automated reasoning. They are used in areas such as functional programming, rule-based programming, automated theorem proving, and the symbolic analysis of security protocols. Matching is related to unification but provides a somewhat simplified problem. Thus, in some cases, we can obtain a matching algorithm even if the unification problem is undecidable. In this paper we consider a hierarchical approach to constructing matching algorithms. The hierarchical method has been successful for developing unification algorithms for theories defined over a constructor sub-theory. We show how the approach can be extended to matching problems which allows for the development, in a modular way, of hierarchical matching algorithms. Here we focus on regular theories, where both sides of each equational axiom have the same set of variables. We show that the combination of two hierarchical matching algorithms leads to a hierarchical matching algorithm for the union of regular theories sharing only a common constructor sub-theory.

ABSTRACT. Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately the type of the set of solutions in nominal anti-unification (with explicit atoms) is infinitary, since every solution set can be strictly refined. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL-A-constraints (with atom-variables), and EQR-constraints based on Equivalence Relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL-A-freshness constraints, and for EQR-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.

ABSTRACT. Implementing unification modulo Associativity and Commutativity (AC) axioms is crucial in rewrite-based programming and theorem provers. We modify Stickel's seminal AC-unification algorithm to avoid mutual recursion and formalise it in the PVS proof assistant. More precisely, we prove the adjusted algorithm's termination, soundness, and completeness. To do this, we adapted Fages' termination proof, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. This development (to the best of our knowledge) provides the first fully formalised AC-unification algorithm.

ABSTRACT. Current AI systems lack several important human capabilities, such as adaptability, generalizability, self-control, consistency, common sense, and causal reasoning. We believe that existing cognitive theories of human decision making, such as the thinking fast and slow theory, can provide insights on how to advance AI systems towards some of these capabilities. In this talk, I will present the work done by IBM and collaborators in this space, including the definition of a general architecture that is based on fast/slow solvers and a metacognitive component. I will then present experimental results on the behavior of an instance of this architecture, for AI systems that make decisions about navigating in a constrained environment. The results will show how combining the fast and slow decision modalities allows the system to evolve over time and gradually pass from slow to fast thinking with enough experience, and that this greatly helps in decision quality, resource consumption, and efficiency.

Bio:

Francesca Rossi is an IBM Fellow and the IBM AI Ethics Global Leader. She is a computer scientist with over 30 years of experience in AI research. Before joining IBM, she has been a professor of computer science at the University of Padova, Italy, for 20 years. Her research interests focus on artificial intelligence, specifically they include constraint reasoning, preferences, multi-agent systems, computational social choice, and collective decision making. She is also interested in ethical issues in the development and behavior of AI systems, in particular for decision support systems for group decision making. She is a fellow of both AAAI and of EurAI and she has been president of IJCAI and the Editor in Chief of the Journal of AI Research. She will be the next president of AAAI. She co-leads the IBM AI ethics board and she actively participate in many global multi-stakeholder initiatives on AI ethics. She is a member of the board of directors of the Partnership on AI and the industry representative in the steering committee of the Global Partnership on AI. She is a fellow of both the worldwide association of AI (AAAI) and of the European one (EurAI), and she will be the next president of AAAI from July 2022.