Logics for safe Artificial Intelligence

Course goals

Upon successful completion of this course, a student:

• knows the logical and computational techniques for specifying, verifying and synthesizing the behavior of AI agents and multi-agent systems, and the limitations of these techniques
• is able to read and assess the research literature in this field
• is able to use appropriate underlying logical formalisms as a framework for specifying, verifying and synthesizing the behavior of AI agents and multi-agent systems, and has a good understanding of the computational aspects of these formalisms
• is able to use appropriate tools implementing these techniques to specify, verify and synthesize the behavior of AI agents and multi-agent systems
• has acquired a mastery of technical artificial intelligence at an advanced academic level 

Assessment
One final exam, pass grade 6/10. 
In order to sit the exam, students need tot pass 50% of the coursework assignments.

Bonus point calculation (where exam is your grade for the final exam):
- if your coursework average is in the range 8-8.49, your grade is min(exam + 0.25, 10)
- if your coursework average is in the range 8.5-8.99, your grade is min(exam + 0.5, 10)
- if your coursework average is in the range 9-9.49, your grade is min(exam + 0.75, 10)
- if your coursework average is in the range 9.5-10, your grade is min(exam + 1, 10)

To qualify for a repair of the final result the mark needs to be at least a 4, or “AANV”.

Content

This course is about ensuring the safety and reliability of autonomous AI agents and multi-agent systems.
In order to guarantee that the behavior of a system achieves its objectives, we use formal proofs rather than empirical studies, and either formally verify that the system behaves in accordance with the specified objectives, or automatically synthesize provably correct behaviors from specifications of the system objectives.
The formal techniques for doing this include epistemic and temporal logics and their combinations, and constitute the main technical content of the course.
The emphasis is on mastering these techniques, their computational aspects, and the use of tools implementing them to verify and synthesize AI agents and multi-agent systems.

The course also prepares students for undertaking research on formal aspects of artificial intelligence, and provides the foundation for undertaking Masters projects on developing safe and reliable AI systems.
Lab sessions will introduce students to relevant specification and modelling techniques and the use of tools such as STV and SynKiti for the verification and synthesis of AI agents and multi-agent systems. 

Course format
Lectures, lab sessions, assignments.