AIAI Seminar-13 May-Talk by Mark Chevallier and Chiara Manganini

Speaker: Mark Chevallier

Title: A Verified Neurosymbolic Pipeline for Learning Temporal Behaviour

Abstract: We introduce a pipeline integrating theorem proving, automatic code generation, and neural networks for neurosymbolic learning. In particular, we mechanise Signal Temporal Logic (STL) over tensors in Isabelle/HOL and use it to specify constraints that are then injected into the learning process. Our aim is to improve the safety of robotic movement using these temporal constraints in a rigorous, formally verified manner. 

The pipeline consists of two main parts: a formally verified logical system with code generation mechanisms and a learning agent that uses both the symbolic constraint and the training data. We demonstrate our approach with several experiments involving behaviour over time.

Speaker: Chiara Manganini

Title: Reasoning About Bias of ML Decision-Making - Chiara Manganini

Abstract: In this talk, I present a logical approach to the fairness of ML decision-making, where decisions are automatically driven by data through the use of a probabilistic ML model. Contrarily to the standard statistically based approach, I propose a logical understanding of bias that can be used in the context of logical reasoning, with possible applications in neuro-symbolic settings and formal verification. More specifically, a measure of the monotonicity of an ML prediction is used to quantitatively assess bias. Finally, I present a game-theoretical interpretation of the work, particularly suitable for gaining insight into some crucial data-quality aspects of ML unfairness.