Welcome to the Lab for AI Verification

Artificial Intelligence is a research and engineering area that develops methods for adaptive and autonomous applications. For example, when your mobile phone learns to recognise your voice — this is an example of its adaptive behaviour. And when your car navigator suggests a better route — this is prototypical autonomous planning. It is easy to see that adaptive and autonomous applications have become pervasive in both the global economy and our everyday lives. However, can we really trust them? The question of trust in computer systems is traditionally a subject of Formal Verification domain. The two different domains — AI and Formal Verification — thus have to meet.

LAIV is a team of researchers working on a range of inter-disciplinary problems that combine AI and Formal Verification.

For example, we seek answers to the following questions:

  • How do we establish safety and security of AI applications?
  • What are the mathematical properties of AI algorithms?
  • How can types and functional programming help to verify AI?
  • How can we verify neural networks and other related machine-learning algorithms?
  • How can machine learning improve software verification?

Descriptions of our projects can be found here.


Mid-term news

We are now in the middle of the 2nd term. Several MSc students joined LAIV in January, and already started to present their projects at LAIV Seminars. The seminars run weekly, and feature invited talks, as well as student talks. Past LAIV talks are available on our YouTube page. We always welcome external visitors and …

Youtube Channel for LAIV/AISEC

As part of the AISEC grant activities, we have launched a Youtube channel (https://www.youtube.com/channel/UCuYLyAKf2mEq4ZSvMfwbfIg/featured) featuring speakers from LAIV Seminars. Subscribe to the Youtube channel or drop in to LAIV seminars: http://laiv.uk/laiv-seminars/