19th March 2025, Assuring Safety in the Face of the Unpredictable

Venturing into the world of autonomous systems, this talk explores the intricacies and challenges of assuring safety in a realm where, as 19th-century philosopher William James put it, “the world is a blooming, buzzing confusion.” The spotlight is on learning-enabled systems, a domain facing urgent safety challenges in our rapidly advancing technological landscape. The presentation revisits the concept of resilience, opening up a vital discussion on the necessity of safety in the face of unpredictability. It lays out the current challenges with a keen eye on the complex balance between system utility and safety. Potential solutions are proposed, providing thought-provoking insights into how we can enable these systems to adapt themselves to diverse contexts without compromising their safety. This talk takes you on a journey into the heart of self-adapting, resilient systems, exploring their complexities, their potential, and their critical role in our future. It's a riveting exploration of a new generation of systems that continuously adapt to meet the unpredictable challenges of the world around them. Based on pertinent examples and current research, this talk not only delves into the dynamics of learning-enabled systems and their safety assurance but also underscores the challenges that remain to be addressed, thereby shedding light on these systems' promising future potential.

Prof. Mario Trapp

Prof. Mario Trapp is Executive Director of the Fraunhofer Institute for Cognitive Systems IKS. In 2005, he obtained his PhD from TU Kaiserslautern, where he also did his habilitation in 2016. He also joined Fraunhofer IESE in 2005, where he started off as a head of department in safety-critical software before becoming head of the Embedded Systems division from 2009 to 2017. After being appointed Acting Executive Director of Fraunhofer ESK (now Fraunhofer IKS) in Munich on January 1, 2018, he assumed this role on a permanent basis on May 1, 2019. In addition to this, Mario Trapp has been a Full Professor at the Technical University of Munich (TUM) since June 1, 2022. He is a Full Professor for Engineering Resilient Cognitive Systems at the School of Computation, Information and Technology CIT. Prior to this, he was an Adjunct Professor in the Department of Computer Science at the TU Kaiserslautern. For many years, Mario Trapp has been contributing his expertise to the development of innovative embedded systems in the context of successful partner projects, in cooperation with both leading international corporations and small and medium-sized enterprises. Currently, his personal research focuses on safety assurance and resilience for cognitive systems, which form the technological basis of many future scenarios such as Industrie 4.0 and automated driving. Mario Trapp has authored numerous international scientific publications. He is also a member of the Bavarian State Government’s Council on AI (Bayerischer KI-Rat) and the Bavarian State Ministry of Economic Affairs, Regional Development and Energy’s AI — Data Science (KI — Data Science) expert panel. Moreover, he is the chair of the EWICS association.

19th February 2025, Neural Model Checking

We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic specification. Unlike testing, model checking provides formal guarantees. Its application is expected standard in silicon design and the EDA industry has invested decades into the development of performant symbolic model checking algorithms. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity using satisfiability solving which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates as well as the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure for model checking is entirely unsupervised, formally sound, and practically effective. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.

Mr. Abhinandan Pal

Originally from Chinsurah, West Bengal, India, I'm currently pursuing my PhD in the Theory of Computer Science Group at the University of Birmingham under the supervision of Mirco Giacobbe with Daniel Kroening as an external supervisor. Prior to this, I completed my undergraduate studies at the Indian Institute of Information Technology Kalyani, where I received the President of India Gold Medal and the department's first prize. During this period, I had the privilege of engaging in research at École Normale Supérieure Ulm, Università degli Studi di Padova, and École Normale Supérieure Paris Saclay, supervised by Caterina Urban, Francesco Ranzato, Marco Zanella, and Mihaela Sighireanu, primarily focusing on the verification of machine learning models.

29th January 2025, Can AVs be careful and competent?

Following four years of development and review by the Law Commissions, the Automated Vehicles Act 2024 gained royal assent setting out some of the requirements that will enable commercial exploitation of self-driving vehicles. The presentation will take us through some of the challenges in making sure that AVs meet the standards set out in the act and some of the further work that will be necessary to ensure that they gain societal acceptance.

 Dr. Nick Reed

For more than twenty years, Dr Nick Reed has worked consistently at the cutting edge of transport research. In 2019, he founded Reed Mobility – an independent expert consultancy on future mobility working across public, private and academic sectors to deliver transport systems that are safe, clean, efficient, ethical and equitable and including projects for the European Commission, DfT, TfL, BSI and RSSB. Having led large scale trials of automated vehicles, much of his recent work has focused on the safety, ethics and societal implications of this technology. November 2021, he was recruited to a three-year part-time role as National Highways' first ever Chief Road Safety Adviser, developing their strategy for eliminating death and serious injury on the strategic road network.

15th January 2025, Representation Engineering for Editing the Brains of LLMs: Detecting and Mitigating Harmful Behaviour

As the popularity of AI rises, so do methods aimed at evaluating and preventing the deployment risks it poses. However, most of those treat the network as a black box, with no insight into what is happening in the internal brain of the model. This is problematic because it does not block or quantify the random (non-deterministic) component of AI reasoning. State-of-the art techniques like representation engineering or activation patching seek to mitigate that.

Mr Lukasz Bartoszcze

Lukasz is researcher at the Alan Turing Institute and currently a third-year Feuer Scholar PhD student studying machine learning robustness, following from a successful Masters at Columbia University. Lukasz has worked on frontier model safeguards, being a contributor to LLM Guard, a popular open-source guardrail library, and experience working on hallucination mitigation techniques, automated jailbreaking and fine-tuning of models for improved robustness, as well as work on ControlAI, a unified platform for connecting regulatory requirements to specific LLM guardrails used to build auditable security evidence for AI systems. He also has worked on AI threats which includes building taxonomies of machine-learning robustness, defining appropriate threat models, and performing red-teaming,  and blue-teaming and implementing safeguards directly for commercial clients against both test-time and training-time attacks during work for Palantir, BCG and Accenture in various consulting and engineering roles. Lukasz has also researched attack strategies such as malicious fine-tuning with harmful results, backdoor attacks, multilingual attacks, and ciphers against LLMs. Lukasz has worked across a range of industries, completing projects for both commercial and governmental clients in healthcare, supply chain and national defence in the UK, US, Poland and Ukraine and is also a member of ML Commons (an organisation dedicated to AI Security) and was recently a part of the UN AI security report for OSET (Office of Secretary General’s Envoy on Technology).

11th December 2024, Runtime Repair for Assumption Violations in High-level Robot Controllers

Recent advancements in robotics have enabled robots to perform sophisticated navigation and manipulation skills. To fully leverage these capabilities, it is essential to design high-level controllers that can safely compose these skills to accomplish complex tasks. However, creating such controllers with correctness guarantees is a significant challenge due to the complexity of the tasks and the unpredictability of the real-world environments. Formal synthesis offers a promising solution by automatically transforming high-level specifications into correct-by-construction controllers. Yet, the synthesized controllers rely on assumptions about the environment behavior. In real-world applications, these assumptions may be violated during runtime, leading to a loss of correctness guarantees and potentially unsafe or undesired robot behaviors.

 Mr Qian Meng

Qian Meng is a Ph.D. student in Computer Science at Cornell University under the guidance of Prof. Hadas Kress-Gazit. He received his B.S. in Computer Science and Mathematics from the University of North Carolina at Chapel Hill. His research focuses on applying formal methods to robotic systems to enhance their robustness and adaptability.

20th November 2024,

Who is responsible for that?” A scrutiny of the ethics and trust within the human-robot paradigm in telerobotics applications

The integration of human-robot interaction, specifically robotic teleoperation, in various sectors raises significant ethical and trust-related concerns. This talk delves into the complexities of responsibility within the human-robot paradigm , particularly in telerobotics applications, with a focus on three <problem, solution> pairs: (i) enhancing telesurgery through novel surgeon-robot interfaces; (ii) alleviating firefighter workload through immersive telerobotics; and (iii) improving construction safety using novel training systems and robotic mechanisms. By analysing case studies and practical frameworks, the talk aims to provide an insight into the hows, whys, and where tos for some of the ethical considerations and trust issues towards ensuring responsible deployment of telerobotics technology.

 Dr. Nikhil Deshpande

Nikhil Deshpande is an Associate Professor of Robotics and AI, with his primary affiliation with the Cyber-physical Health and Assistive Robotics Technologies (CHART) group. With over 15 years of experience in Robotics and AI covering different aspects, including navigation, manipulation, mechanism design, machine learning, computer vision, and mixed reality, he has focused on applications in telesurgery, telerobotics, therapy, industrial training, among others. Prior to joining CS @ Nottingham, Nikhil was a Researcher and Team Leader at the Italian Institute of Technology (IIT), Genova, Italy, leading the VICARIOS Mixed Reality and Simulations Lab, where his group focused on immersive remote telerobotics in hazardous environments, covering topics including remote telemanipulation, shared autonomy, 3D semantic scene understanding, haptics, mixed reality for industrial training, control simulations, etc. Nikhil has been the lead organiser of the XR-ROB workshop, the only gathering of its kind at the IEEE/RSJ IROS international conference exploring the confluence of extended reality (XR) and robotics technologies. Nikhil has been PI and co-I for multiple collaborative projects, with R&D funding exceeding €7 million, working closely with stakeholders, including surgeons, firefighters, and construction workers, and demonstrated the project outcomes in public dissemination events, including to the President of Italy in 2022. Nikhil received his PhD in Electrical Engineering, with a focus on Robotics, in 2012, from the North Carolina State University (NCSU), USA, Master's in Integrated Manufacturing Systems Engineering at NCSU in 2007, and his Bachelor's in Electrical Engineering in 2003 from the College of Engineering (COEP), Pune, India.

6th November 2024, Forward and Backward Analysis for Neural Network Certification

In the past decade, artificial intelligence (AI), especially deep learning (DL), has achieved significant advancement. Despite the wide deployment and enthusiastic embrace of AI technologies, the instability and black-box nature of DL systems are raising concerns about the readiness and maturity of AI. As with any automation technology, certification is an essential step to take for AI to be deployed in real-world safety- and security-critical applications. In this talk, I will present recent research outcomes for forward and backward analysis of neuron networks (NNs) to provide provable guarantees on the critical decisions made by NN-based systems. We propose an automated convex bounding algorithm for forward analysis of neural networks with general activation functions. For backward analysis, we present an efficient anytime algorithm to derive preimage approximations, which enables sound and complete quantitative verification for piecewise-linear neural networks.

 Dr. Xiyue Zhang

Xiyue Zhang is a Lecturer in the School of Computer Science at the University of Bristol. Before joining Bristol, she was a Research Associate in the Department of Computer Science at the University of Oxford. She received her PhD in 2022 from Peking University, where she focused on trustworthiness assurance of deep learning systems, and her BSc in 2017, also from Peking University. Her research mainly focuses on trustworthy deep learning, integrating both provable certification and practical empirical methods. Her recent work includes abstraction and verification for deep learning models and deep learning-enabled systems.