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 the 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?

The Lab was established in 2019, with the initial intent to provide a local hub where researchers and research students from the Edinburgh Center for Robotics and the National Robotarium can meet with Computer Scientists, Logicians and Programming Language experts interested in verification of AI. Since then, the range of our projects and collaborations widened. Descriptions of our projects can be found here, and here you can learn more about LAIV members and publications. Get in touch with us if you are interested in establishing a new collaboration!


New LAIV PhD students

We are happy to welcome two new PhD students this Autumn: Remi Desmartin, who will work with supervisors Komendantskaya, Stark and Passmore (from Imandra.ai) on neural network libraries in Imandra and Aina Centelles Tarres, who will work with supervisors Gabbay and Komendantskaya on nominal logic for neural network verification. Remi and Aina, have a great …

ACCV success of Daniel Kienitz

LAIV PhD student, Daniel Kienitz, has just had his paper accepted at the Asian Conference on Computer Vision (ACCV 2022): D. Kienitz, E. Komendantskaya and M. Lones.  Comparing Complexities of Decision Boundaries for Robust Training: A Universal Approach. Many congratulations, Daniel!

LAIV MSc student success

MSc dissertation marks have been released, and MSc students supervised by the LAIV team: Youssef, Henri-Louis, Assya, Samuel, Sinead, Haoran, all got excellent marks (one B and five As). Many congratulations to the students, but also their supervisors: Luca, Matthew, Marco, Natalia, Yuhui! Well done all. If curious to see the final titles and supervisory …