AISEC: AI Secure and Explainable by Construction
Lead Research Organisation:
Heriot-Watt University
Department Name: S of Mathematical and Computer Sciences
Abstract
AI applications have become pervasive: from mobile phones and home appliances to stock markets, autonomous cars, robots and drones. As AI takes over a wider range of tasks, we gradually approach the times when security laws, or policies, ultimately akin to Isaac Asimov's "3 laws of robotics" will need to be established for all working AI systems. A homonym of Asimov's first name, the project AISEC (``Artificial Intelligence Secure and Explainable by Construction"), aims to build a sustainable, general purpose, and multidomain methodology and development environment for policy-to-property secure and explainable by construction development of complex AI systems.
We will create and deploy a novel framework for documenting, implementing and developing policies for complex deep learning systems by using types as a unifying language to embed security and safety contracts directly into programs that implement AI. The project will produce a development tool AISEC with infrastructure (user interface, verifier, compiler) to cater for different domain experts: from lawyers working with security experts to verification experts and
system engineers designing complex AI systems. AISEC will be built, tested and used in collaboration with industrial partners in two key AI application areas: autonomous vehicles and natural language interfaces.
AISEC will catalyse a step change from pervasive use of deep learning in AI to pervasive use of methods for deep understanding of intended policies and latent properties of complex AI systems, and deep verification of such systems.
We will create and deploy a novel framework for documenting, implementing and developing policies for complex deep learning systems by using types as a unifying language to embed security and safety contracts directly into programs that implement AI. The project will produce a development tool AISEC with infrastructure (user interface, verifier, compiler) to cater for different domain experts: from lawyers working with security experts to verification experts and
system engineers designing complex AI systems. AISEC will be built, tested and used in collaboration with industrial partners in two key AI application areas: autonomous vehicles and natural language interfaces.
AISEC will catalyse a step change from pervasive use of deep learning in AI to pervasive use of methods for deep understanding of intended policies and latent properties of complex AI systems, and deep verification of such systems.
Planned Impact
We will maximise the impact of our research by industrial exploitation, collaboration with other academics, engaging with industry and government stakeholders, and public engagement activities. Activities are planned as follows.
1. Building a working Demonstrator tool, AISEC. This will be co-designed with our industrial partners and developed during the project, as well as used for "in-the-wild" experiments in the third year.
2. Open-source community building around our technology. We will make the AISEC platform freely available on an open-source platform such as Github (the largest worldwide repository of software used by many companies following an Open Innovation model).
3. Direct application of our research in industry, during and after the project. The research has been designed to fit closely with the industrial goals of our partners, who see security and verification of AI as vital to their future business. We are engaging with a range of companies, from start-up through SMEs to large industry. By establishing a regular board meeting, we will support and extend our engagement.
4. To foster the direct impact of our work and conduct in-the-wild experiments, we plan that the third year of the project will have a significant portion of time with our researchers embedded in industry. Our project partners have dedicated resource to support this, and we will pursue additional partnerships during the project.
5. Public engagement. Drawing on experience and expertise in public engagement of the investigatory team, we plan a series of events and online activities which will appeal to the broader public, in particular, to help raise awareness of emerging solutions to the challenge of trustworthy and secure AI.
6. Government and policy-making engagement. We will continue existing engagements with Scottish Government, the Scottish National Cyber Resilience Advisory Board, Police Scotland, as well as UK government contacts in DCMS and NCSC, to discuss future policy and regulation impacts of AI technology and security.
7. Skills and training. The research will contribute both to direct training, of the employed RAs and associated PhD researchers in the project, but also indirectly to educational materials being delivered across our Universities and the wider Scottish education landscape, through connections with Skills Development Scotland, Graduate Apprenticeships in Cyber Security, and the Edinburgh and Glasgow City-Region Deal initiatives.
8. Research community building and Knowledge exchange. Using networking funds available to Scottish Universities through SICSA, we will take part and organise meetings to showcase AISEC research. For AISEC itself, we will organise a specialised annual workshop open to academia and industrial researchers, bringing together partners and researchers from related areas to draw on the excitement and importance of the research topic.
9. Academic networking among associated UK flagship projects. Besides the usual channels for academic dissemination of our research in international conferences and journals, we will network with other significant research activities in the area. Specifically in the UK, we have connections to TIPS, the Cyber Security Research Institutes VeTTS, RITICS and RISCS, the new TIPS Network+ SPRITE, the IoT PETRAS 2.0 Hub, PaCCS as well as smaller responsive mode funded EPSRC projects. We expect to connect to the ISCF initiative in Digital Security by Design. We have recently started a small exploratory research project with NCSC on Security and AI. Through these connections, we expect AISEC will bring additional impact from further routes, and broader networks of interest across industry and government.
All of the above impact activities will be conducted within the ORBIT framework for Responsible Research and Innovation, and activities monitored regularly during the project to ensure delivery on each pathway.
1. Building a working Demonstrator tool, AISEC. This will be co-designed with our industrial partners and developed during the project, as well as used for "in-the-wild" experiments in the third year.
2. Open-source community building around our technology. We will make the AISEC platform freely available on an open-source platform such as Github (the largest worldwide repository of software used by many companies following an Open Innovation model).
3. Direct application of our research in industry, during and after the project. The research has been designed to fit closely with the industrial goals of our partners, who see security and verification of AI as vital to their future business. We are engaging with a range of companies, from start-up through SMEs to large industry. By establishing a regular board meeting, we will support and extend our engagement.
4. To foster the direct impact of our work and conduct in-the-wild experiments, we plan that the third year of the project will have a significant portion of time with our researchers embedded in industry. Our project partners have dedicated resource to support this, and we will pursue additional partnerships during the project.
5. Public engagement. Drawing on experience and expertise in public engagement of the investigatory team, we plan a series of events and online activities which will appeal to the broader public, in particular, to help raise awareness of emerging solutions to the challenge of trustworthy and secure AI.
6. Government and policy-making engagement. We will continue existing engagements with Scottish Government, the Scottish National Cyber Resilience Advisory Board, Police Scotland, as well as UK government contacts in DCMS and NCSC, to discuss future policy and regulation impacts of AI technology and security.
7. Skills and training. The research will contribute both to direct training, of the employed RAs and associated PhD researchers in the project, but also indirectly to educational materials being delivered across our Universities and the wider Scottish education landscape, through connections with Skills Development Scotland, Graduate Apprenticeships in Cyber Security, and the Edinburgh and Glasgow City-Region Deal initiatives.
8. Research community building and Knowledge exchange. Using networking funds available to Scottish Universities through SICSA, we will take part and organise meetings to showcase AISEC research. For AISEC itself, we will organise a specialised annual workshop open to academia and industrial researchers, bringing together partners and researchers from related areas to draw on the excitement and importance of the research topic.
9. Academic networking among associated UK flagship projects. Besides the usual channels for academic dissemination of our research in international conferences and journals, we will network with other significant research activities in the area. Specifically in the UK, we have connections to TIPS, the Cyber Security Research Institutes VeTTS, RITICS and RISCS, the new TIPS Network+ SPRITE, the IoT PETRAS 2.0 Hub, PaCCS as well as smaller responsive mode funded EPSRC projects. We expect to connect to the ISCF initiative in Digital Security by Design. We have recently started a small exploratory research project with NCSC on Security and AI. Through these connections, we expect AISEC will bring additional impact from further routes, and broader networks of interest across industry and government.
All of the above impact activities will be conducted within the ORBIT framework for Responsible Research and Innovation, and activities monitored regularly during the project to ensure delivery on each pathway.
Organisations
- Heriot-Watt University (Lead Research Organisation)
- Schlumberger Limited (Collaboration)
- Microsoft Research (Collaboration)
- Amazon.com (Collaboration)
- UNIVERSITY OF EDINBURGH (Collaboration)
- Google (Collaboration)
- Hebrew University of Jerusalem (Collaboration)
- Apple (Collaboration)
- Microsoft Corporation (Collaboration)
- Imandra Inc (Collaboration)
- Leiden University (Project Partner)
- Symphonic Software (Project Partner)
- Hebrew University of Jerusalem (Project Partner)
- Imandra (Project Partner)
- Boston University (Project Partner)
- Norwegian Defence Research Establishment (Project Partner)
- MIRA (United Kingdom) (Project Partner)
- University of St Andrews (Project Partner)
- HuggingFace Inc. (Project Partner)
- Five AI Limited (Project Partner)
- NEC (Germany) (Project Partner)
Publications
Xu X.
(2021)
AGGGEN: Ordering and aggregating while generating
in ACL-IJCNLP 2021 - 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing, Proceedings of the Conference
Bogani R
(2022)
Garbage in, toxic data out: a proposal for ethical artificial intelligence sustainability impact statements.
in AI and ethics
Scharf T
(2022)
AnalyZr: A Python application for zircon grain image segmentation and shape analysis
in Computers & Geosciences
Norman U
(2022)
Studying Alignment in a Collaborative Learning Activity via Automatic Methods: The Link Between What We Say and Do
in Dialogue & Discourse
Stewart R
(2021)
Optimising Hardware Accelerated Neural Networks with Quantisation and a Knowledge Distillation Evolutionary Algorithm
in Electronics
Sokolovsky A
(2023)
A generic methodology for the statistically uniform & comparable evaluation of Automated Trading Platform components
in Expert Systems with Applications
Xu X.
(2021)
MIRANEWS: Dataset and Benchmarks for Multi-Resource-Assisted News Summarization
in Findings of the Association for Computational Linguistics, Findings of ACL: EMNLP 2021
McLachlan S
(2021)
Smart automotive technology adherence to the law: (de)constructing road rules for autonomous system development, verification and safety
in International Journal of Law and Information Technology
McLachlan S
(2022)
Tempting the Fate of the furious: cyber security and autonomous cars
in International Review of Law, Computers & Technology
ALLAIS G
(2021)
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
in Journal of Functional Programming
Description | The project investigated how legal, security and safety concerns for AI-driven systems can be formalised, with a view of verification. The main outcome was the novel methodology for specification, verification and re-training of Neural networks, given by the language Vehicle. https://github.com/vehicle-lang/vehicle |
Exploitation Route | It can be taken forward as part of verification methodology for complex systems based on AI |
Sectors | Aerospace Defence and Marine Digital/Communication/Information Technologies (including Software) Energy Financial Services and Management Consultancy Healthcare Manufacturing including Industrial Biotechology |
URL | https://vehicle-lang.github.io/tutorial/ |
Description | AI4People ethics guidelines for the use of AI by the legal profession |
Geographic Reach | Europe |
Policy Influence Type | Participation in a guidance/advisory committee |
URL | https://ai4people.eu/wp-content/pdf/AI4People7AIGlobalFrameworks.pdf |
Description | DATAIA scientific advisory board |
Geographic Reach | Europe |
Policy Influence Type | Participation in a guidance/advisory committee |
URL | https://www.dataia.eu/linstitut/le-conseil-scientifique |
Description | Independent Advisory Group on Emerging Technologies report |
Geographic Reach | Local/Municipal/Regional |
Policy Influence Type | Contribution to a national consultation/review |
URL | https://www.sipr.ac.uk/wp-content/uploads/2023/02/Independent-advisory-group-on-emerging-technologie... |
Description | Legislating for AVs in Dubai |
Geographic Reach | Asia |
Policy Influence Type | Participation in a guidance/advisory committee |
Description | Submission to the UK Governemnt co nsultation on Self-driving vehicles: new safety ambitions |
Geographic Reach | National |
Policy Influence Type | Contribution to a national consultation/review |
URL | https://www.gov.uk/government/consultations/self-driving-vehicles-new-safety-ambition |
Description | appointed to the Independent advisory group on emerging technologies in policing (Scotland) |
Geographic Reach | National |
Policy Influence Type | Membership of a guideline committee |
Description | AISEC: AI Secure and Explainable by Construction |
Amount | £2,200,000 (GBP) |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 08/2020 |
End | 08/2023 |
Description | Austrian Standards Senior Fellowship |
Amount | € 3,000 (EUR) |
Organisation | University of Graz |
Sector | Academic/University |
Country | Austria |
Start | 09/2023 |
End | 11/2023 |
Description | Continuous Verification of Neural Networks |
Amount | £90,848 (GBP) |
Organisation | Defence Science & Technology Laboratory (DSTL) |
Sector | Public |
Country | United Kingdom |
Start | 03/2020 |
End | 03/2021 |
Description | ICASE Scholarship |
Amount | £118,483 (GBP) |
Organisation | United Kingdom Research and Innovation |
Sector | Public |
Country | United Kingdom |
Start | 08/2022 |
End | 09/2026 |
Description | Leverhulme Trust Senior Research Fellowship 2020 |
Amount | £47,000 (GBP) |
Funding ID | SRF\R1\201100 |
Organisation | The Royal Society |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 08/2020 |
End | 08/2021 |
Description | Neural Network Verification: in Search of the Missing Spec |
Amount | £100,000 (GBP) |
Organisation | National Cyber Security Centre |
Sector | Public |
Country | United Kingdom |
Start | 03/2021 |
End | 03/2022 |
Description | PhD studentship "Verification of Neural Networks in Imandra" |
Amount | £176,946 (GBP) |
Organisation | Imandra Inc |
Sector | Private |
Country | United States |
Start | 08/2022 |
End | 09/2026 |
Description | PhD studentship from the Edinburgh Center for Robotics |
Amount | £176,946 (GBP) |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 08/2023 |
End | 09/2027 |
Description | Safer aviation from ethical Autonomous Intelligence Regulation (SafeAIR) |
Amount | £200,000 (GBP) |
Funding ID | Dr Scott McLachlan |
Organisation | Royal Academy of Engineering |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 12/2021 |
End | 12/2023 |
Description | The law and policy dimension of automated vehicles in the United Arab Emirates. |
Amount | 300,000 د.إ. (AED) |
Organisation | University of Dubai |
Sector | Academic/University |
Country | United Arab Emirates |
Start | 02/2023 |
End | 01/2024 |
Description | UKRI AI Centre for Doctoral Training in Dependable and Deployable Artificial Intelligence for Robotics (CDT-D2AIR) |
Amount | £9,534,199 (GBP) |
Funding ID | EP/Y030834/1 |
Organisation | United Kingdom Research and Innovation |
Sector | Public |
Country | United Kingdom |
Start | 06/2024 |
End | 12/2032 |
Description | Verification Properties in Neural Network Verification: Exploration of the Design Space |
Amount | £108,000 (GBP) |
Funding ID | 2616531 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 08/2021 |
End | 02/2025 |
Description | Verification of Neural Networks for Natural Language Processing: James Watt Scholarship |
Amount | £108,000 (GBP) |
Funding ID | James Watt Scholarship |
Organisation | Heriot-Watt University |
Sector | Academic/University |
Country | United Kingdom |
Start | 08/2021 |
End | 09/2024 |
Title | BLOOM Large Language Model |
Description | We created BLOOM the first publicly available large language model. This was a year-long collaboration as part of the BigScience workshop with several hundred of international scientists. I co-led one of the working groups. BLOOM stands for BigScience Large Open-science Open-access Multilingual Language Model. |
Type Of Material | Improvements to research infrastructure |
Year Produced | 2022 |
Provided To Others? | Yes |
Impact | First publicly available "foundational model". Widely used and compared in the community. The ambition is to boost academic research and public benefits in competition to privately owned models, e.g. ChatGPT etc,. |
URL | https://huggingface.co/bigscience/bloom |
Title | Tutorial on Neural Network Verification with Vehicle |
Description | Machine learning components, such as neural networks, gradually make their way into software; and, when the software is critically safe, the machine learning components must be verifiably safe. This gives rise to the problem of neural network verification. The community has been making rapid progress in developing methods for incorporating logical specifications into neural networks, both in training and verification. However, to truly unlock the ability to verify real-world neural network-enhanced systems we believe the following is necessary: 1. The specification should be written once and should automatically work with training and verification tools. 2. The specification should be written in a manner independent of any particular neural network training/inference platform. 3. The specification should be able to be written as a high-level property over the problem space, rather than a property over the input space (of the neural network). 4. After verification the specification should be exportable to general interactive theorem provers so that its proof can be incorporated into proofs about the larger systems around the neural network. In this tutorial we presented Vehicle, a tool that allows users to do all of this. We provided an introduction to the Vehicle specification language, and then walked attendees through using it to express a variety of famous and not-so-famous specifications. Subsequently we demonstrate how a specification can be compiled down to i) queries for network verifiers, ii) Tensorflow graphs to be used as loss functions during training and iii) cross-compiled to Agda, a main-stream interactive theorem prover. Finally we discussed some of the technical challenges in the implementation as well as some of the outstanding problems. |
Type Of Material | Improvements to research infrastructure |
Year Produced | 2023 |
Provided To Others? | Yes |
Impact | This tutorial has been run live and adapted for different audiences at: FOMLAS'23 the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems co-allocated with CAV'23 in Paris, France; 18 July 2023; VETSS Summer School at the University of Surrey, UK; 23 August 2023; Youtube recording available; ICFP'23 the International Conference on Functional Programming in Seattle, USA; 08 September 2023. |
URL | https://vehicle-lang.github.io/tutorial/ |
Title | Explainable ML-driven Strategy for Automated Trading Pattern Extraction - Reproducibility Package |
Description | Financial markets are a source of non-stationary multidimensional time series which has been drawing attention for decades. Each financial instrument has its specific changing over time properties, making their analysis a complex task. Improvement of understanding and development of methods for financial time series analysis is essential for successful operation on financial markets. In this study we propose a volume-based data pre-processing method for making financial time series more suitable for machine learning pipelines. We use a statistical approach for assessing the performance of the method. Namely, we formally state the hypotheses, set up associated classification tasks, compute effect sizes with confidence intervals, and run statistical tests to validate the hypotheses. We additionally assess the trading performance of the proposed method on historical data and compare it to a previously published approach. Our analysis shows that the proposed volume-based method allows successful classification of the financial time series patterns, and also leads to better classification performance than a price action-based method, excelling specifically on more liquid financial instruments. Finally, we propose an approach for obtaining feature interactions directly from tree-based models on example of CatBoost estimator, as well as formally assess the relatedness of the proposed approach and SHAP feature interactions with a positive outcome. In this code repository you will find datasets and a notebook to reproduce experiments from our paper |
Type Of Material | Data analysis technique |
Year Produced | 2021 |
Provided To Others? | Yes |
Impact | in progress |
URL | https://zenodo.org/record/4756325#.YhupAz_P1hE |
Title | Machine Learning Classification of Price Extrema Based on Market Microstructure and Price Action Features. A Case Study of S&P500 E-mini Futures. Reproducibility Package. |
Description | The study introduces an automated trading system for S&P500 E-mini futures (ES) based on state-of-the-art machine learning. Concretely: we extract a set of scenarios from the tick market data to train the models and further use the predictions to statistically assess the soundness of the approach. We define the scenarios from the local extrema of the price action. Price extrema is a commonly traded pattern, however, to the best of our knowledge, there is no study presenting a pipeline for automated classification and profitability evaluation. Additionally, we evaluate the approach in the simulated trading environment on the historical data. Our study is filling this gap by presenting a broad evaluation of the approach supported by statistical tools which make it generalisable to unseen data and comparable to other approaches. By Artur Sokolovsky; Luca Arnaboldi |
Type Of Material | Computer model/algorithm |
Year Produced | 2021 |
Provided To Others? | Yes |
Impact | in process |
URL | https://zenodo.org/record/4732928#.YhuoMz_P1hE |
Description | Amazon SimBot Challenge |
Organisation | Amazon.com |
Department | Amazon UK |
Country | United Kingdom |
Sector | Private |
PI Contribution | My student team was selected to participate in the Amazon SimBot challenge. |
Collaborator Contribution | Our entry is supported with a grant from Amazon and in-kind contributions such as an invited visit to Amazon headquarters in Seattle as well as 2 days of workshops with Amazon staff. |
Impact | We expect a number of outcomes, including publications, student internships, and raising the international profile of our lab and university in this research area. |
Start Year | 2021 |
Description | Apple NLU research award |
Organisation | Apple |
Country | United States |
Sector | Private |
PI Contribution | This research gift supports research on low-resource Natural Language Generation. |
Collaborator Contribution | Research gift and monthly meetings. |
Impact | not yet |
Start Year | 2021 |
Description | Collaboration with Airborne Robotics group, Ignazio Viola |
Organisation | University of Edinburgh |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Joint supervision of a PhD student from the Edinburgh Center for Robotics, Colin Kessler. Project ``Verification of Airborne Robots". Second supervisor Prof. Ignazio Viola, School of Engineering, Edinburgh University. 2023- 2027 (\pounds 176,946) |
Collaborator Contribution | Second supervision of a PhD student, lab resources |
Impact | in progress |
Start Year | 2023 |
Description | Collaboration with Hebrew University Jerusalem (HUJI) and Guy Katz |
Organisation | Hebrew University of Jerusalem |
Department | School of Computer Science and Engineering |
Country | Israel |
Sector | Academic/University |
PI Contribution | Joint work on research papers and software (Vehicle). |
Collaborator Contribution | The partner consulted the AISEC team on internals of Marabou, a neural network verifier. |
Impact | The software Vehicle. Publication: Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, Idan Refaeli: Neural Network Robustness as a Verification Property: A Principled Case Study. CAV (1) 2022: 219-231 |
Start Year | 2021 |
Description | Collaboration with Imandra and Grant Passmore |
Organisation | Imandra Inc |
Country | United States |
Sector | Private |
PI Contribution | Research papers and Software Neural networks are increasingly relied upon as components of complex safety-critical systems such as autonomous vehicles. There is high demand for tools and methods that embed neural network verification in a larger verification cycle. However, neural network verification is problematic due to a wide range of verification properties of interest, each so far being amenable to verification only in specialised solvers. In this paper we show how Imandra, a functional programming language and a theorem prover originally designed for verification, validation and simulation of FinTech systems can offer a holistic infrastructure for neural network verification. To showcase Imandra's potential as a single code base, we developed a novel library that formalises convolutional neural networks in Imandra, and covers different important facets of neural network verification. |
Collaborator Contribution | Imandra consulted the research team on internals of Imandra Software, and is sponsoring a PhD studentship. |
Impact | PhD scholarship paid by Imandra to R.Desmartin Papers: Remi Desmartin, Grant O. Passmore, Ekaterina Komendantskaya, Matthew Daggit: CheckINN: Wide Range Neural Network Verification in Imandra. PPDP 2022: 3:1-3:14 Remi Desmartin, Grant O. Passmore, Ekaterina Komendantskaya: Neural Networks in Imandra: Matrix Representation as a Verification Choice. NSV/FoMLAS@CAV 2022: 78-95 |
Start Year | 2021 |
Description | Collaboration with Microsoft Research (J.Protzenko), Law Formalisation |
Organisation | Microsoft Corporation |
Country | United States |
Sector | Public |
PI Contribution | Law formalisation in Catala |
Collaborator Contribution | Research collaboration, consultancy |
Impact | Luca Arnaboldi, David Aspinall, Ronny Bogani, Burkhard Schafer, Scott Herman, Jonathan Protzenko, Ekaterina Komendantskaya, Yue Li , Remi Desmartin. Formalising Criminal Law in Catala. PRoLaLa, POPL Workshop on Programming Languages and the Law 2023 |
Start Year | 2023 |
Description | Collaboration with Microsoft Research (J.Protzenko), Law Formalisation |
Organisation | Microsoft Research |
Country | Global |
Sector | Private |
PI Contribution | Law formalisation in Catala |
Collaborator Contribution | Research collaboration, consultancy |
Impact | Luca Arnaboldi, David Aspinall, Ronny Bogani, Burkhard Schafer, Scott Herman, Jonathan Protzenko, Ekaterina Komendantskaya, Yue Li , Remi Desmartin. Formalising Criminal Law in Catala. PRoLaLa, POPL Workshop on Programming Languages and the Law 2023 |
Start Year | 2023 |
Description | Collaboration with Schlumberger Cambridge (Michael John Williams) |
Organisation | Schlumberger Limited |
Department | Schlumberger Cambridge Research |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | iCASE Scholarship was funded to investigate applications of AISEC results in Schlumberger diagnostics. |
Collaborator Contribution | Consultancy, cosupervision of PhD student |
Impact | Just started |
Start Year | 2022 |
Description | Google Dialog and NLU research award |
Organisation | |
Country | United States |
Sector | Private |
PI Contribution | This research gifts supports an informal collaboration between Google Zurich and my group on topics related to dialogue systems and Natural Language Understanding. |
Collaborator Contribution | We received a research gift from Google to support research expenses. |
Impact | The award has supported my group with hardware, travel and data services (such as transcriptions and crowdsourcing) |
Start Year | 2020 |
Title | Amethyst - an Agda library for NN verification |
Description | Amethyst is an Agda library for neural network verification. Using Agda's expressive dependent type system, Amethyst is capable of specifying the desired properties of the neural network as a type. If your neural network doesn't have the right input/output behaviour, it won't even type-check! Amethyst is superseded by Vehicle in many ways. |
Type Of Technology | Webtool/Application |
Year Produced | 2020 |
Open Source License? | Yes |
Impact | Led to creation of the tool Vehicle. Produced by Wen Kokke |
URL | https://www.macs.hw.ac.uk/aisec/index.php/software-page |
Title | Neural Network Library in IMANDRA |
Description | Neural networks are increasingly relied upon as components of complex safety-critical systems such as autonomous vehicles. There is high demand for tools and methods that embed neural network verification in a larger verification cycle. However, neural network verification is problematic due to a wide range of verification properties of interest, each so far being amenable to verification only in specialised solvers. In this paper we show how Imandra, a functional programming language and a theorem prover originally designed for verification, validation and simulation of FinTech systems can offer a holistic infrastructure for neural network verification. To showcase Imandra's potential as a single code base, we developed a novel library that formalises convolutional neural networks in Imandra, and covers different important facets of neural network verification. |
Type Of Technology | Webtool/Application |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | The software is used as part of industrial collaboration, with Industry Imanra (www.imandra.ai) |
URL | https://github.com/aisec-private/ImandraNN |
Title | Vehicle |
Description | The application provides an Interface for Neural Network Verifiers with Interactive Theorem Provers. Verification of neural networks is currently a hot topic in automated theorem proving. Progress has been rapid and there are now a wide range of tools available that can verify properties of networks with hundreds of thousands of nodes. In theory this opens the door to the verification of larger control systems that make use of neural network components. However, although work has managed to incorporate the results of these verifiers to prove larger properties of individual systems, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs. It overcomes previous issues with maintainability and scalability in similar ITP formalisations by using a standard ONNX file as the single canonical representation of the network. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road, even in the face of an unpredictable cross wind and imperfect sensors. The network has over 20,000 nodes, and therefore this proof represents an improvement of 3 orders of magnitude over prior proofs about neural network enhanced systems in ITPs. |
Type Of Technology | Webtool/Application |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | The software is used as a working tool in collaboration with HUJI and Stanford (researchers developing Marabou) |
URL | https://github.com/vehicle-lang/vehicle |
Title | agda-setup |
Description | Set up Agda, the standard library, or any Git-hosted library, for use in GitHub Actions. This action can install Agda from binary distributions or build Agda from source. |
Type Of Technology | Webtool/Application |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | This tool has been used by several high profile Agda libraries for Continuous Integration testing, listed at https://github.com/wenkokke/setup-agda/network/dependents |
URL | https://github.com/wenkokke/setup-agda |
Description | AISEC webpage and AISEC YouTube Channel |
Form Of Engagement Activity | Engagement focused website, blog or social media channel |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | AISEC Youtube contains recordings of research and educational seminars, for various audiences. AISEC webpage records other activities, including open source software. AISEC Youtube: https://www.youtube.com/channel/UCuYLyAKf2mEq4ZSvMfwbfIg/featured AISEC Webpage: https://www.macs.hw.ac.uk/aisec/index.php |
Year(s) Of Engagement Activity | 2020 |
URL | https://www.youtube.com/channel/UCuYLyAKf2mEq4ZSvMfwbfIg/featured |
Description | CNBC Interview |
Form Of Engagement Activity | A press release, press conference or response to a media enquiry/interview |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Media (as a channel to the public) |
Results and Impact | Interview with CNBC on AI trends/ research predictions for 2022 |
Year(s) Of Engagement Activity | 2021 |
URL | https://www.cnbc.com/2022/01/07/deep-learning-and-large-language-how-ai-is-set-to-evolve-in-2022.htm... |
Description | Demo at Science Festival, Edinburgh, April 2022 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Public/other audiences |
Results and Impact | Presentation of Autonomous Car at Science Festival in Edinburgh |
Year(s) Of Engagement Activity | 2022 |
Description | Invited talk at the First Annual LAST-JD-RIOE Conference of the Marie Sklodowska-Curie Action program "Rights in Internet of Everything" |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | The event was part of the Marie Sklodowska-Curie Action program "Rights in Internet of Everything", a EU project that sponsors a 3 year PhD program involving 15 European Universities It was attended by past and current students on the program, and also other PhD and Master students from participating institutions. I received several expressions of interest to come to the UK for a PhD in this field |
Year(s) Of Engagement Activity | 2021 |
URL | https://rioe.oeg.fi.upm.es/conference/#contact |
Description | New Scientist article on LLMs 2023 |
Form Of Engagement Activity | A press release, press conference or response to a media enquiry/interview |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Media (as a channel to the public) |
Results and Impact | Interview about pruning large language models based on my expertise from participating in the BigScience BLOOM modelling collaboration: "Huge AI models can be halved in size without degrading performance A way to cut the scale of artificial intelligence models by 60 per cent could save huge amounts of energy and make them more accessible" |
Year(s) Of Engagement Activity | 2023 |
URL | https://www.newscientist.com/article/2355078-huge-ai-models-can-be-halved-in-size-without-degrading-... |
Description | Participating in ReMeP workshop as invited particpant on roundtable on "Computational Law" |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Participated in a panel discussion on computational law as part of ReMeP - research meets practice. The aim was to introduce governments and legislators to the potential of computational law, and industry on the business opportunities to support this new form of lawmaking. The panel was attended by 140 participants A follow up request from the Austrian government to explore the possibility of a computational version of the GDPR |
Year(s) Of Engagement Activity | 2021 |
URL | https://remep.live/ |
Description | Seminar on legal ontologies given at ReMeP: Research Meets Practice |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | ReMeP is an annual event to bring research in law and technology to practice. It is attended mainly by representatives from industry, legal practice and government Chaired panel and gave keynote talk on Legal Ontologies. 470 participants, lead to extended questions and discussions, and 2 follow up invitations Recordings of the talks are made available as training tools |
Year(s) Of Engagement Activity | 2020 |
URL | https://www.remep.net/materials-2020/ |
Description | The Conversation Article |
Form Of Engagement Activity | A magazine, newsletter or online publication |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Media (as a channel to the public) |
Results and Impact | E.Komendantskaya, L.Arnaboldi, M.Daggitt "Perfecting self-driving cars - can it be done?". The Conversation, 6 April 2021. A paper explaining challenges in verification of autonomous cars |
Year(s) Of Engagement Activity | 2021 |
URL | https://theconversation.com/perfecting-self-driving-cars-can-it-be-done-157483 |