AISEC: AI Secure and Explainable by Construction

AISEC：人工智能通过构建变得安全且可解释

• 批准号: EP/T026952/1
• 负责人: Ekaterina Komendantskaya
• 金额: $ 102.85万
• 依托单位: Heriot-Watt University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FT026952%2F1
• 关键词: AISEC; AI; Secure; Explainable; Construction

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.

人工智能应用已经变得无处不在：从手机和家用电器到股票市场、自动驾驶汽车、机器人和无人机。随着人工智能接管更广泛的任务，我们逐渐接近需要为所有工作人工智能系统建立安全法律或政策的时代，最终类似于艾萨克·阿西莫夫的“机器人三定律”。 AISEC 项目与阿西莫夫的名字同音（“通过构建实现安全和可解释的人工智能”），旨在构建一个可持续的、通用的、多领域的方法论和开发环境，通过复杂人工智能系统的构建开发来确保政策到财产的安全和可解释。我们将创建和部署一个新颖的框架，通过使用类型作为统一语言来嵌入安全和安全合约，用于记录、实施和开发复杂深度学习系统的策略 直接进入实现人工智能的程序。该项目将生产一个具有基础设施（用户界面、验证器、编译器）的开发工具 AISEC，以满足不同领域专家的需求：从与安全专家合作的律师到设计复杂人工智能系统的验证专家和系统工程师。 AISEC 将与工业合作伙伴合作在两个关键的人工智能应用领域进行构建、测试和使用：自动驾驶汽车和自然语言界面。AISEC 将促进 从人工智能中普遍使用深度学习到普遍使用方法来深入理解复杂人工智能系统的预期策略和潜在属性以及对此类系统进行深度验证的一步转变。

项目成果

The Cambridge Handbook of Information Technology, Life Sciences and Human Rights

剑桥信息技术、生命科学和人权手册

• DOI: 10.1017/9781108775038.018
• 发表时间: 2022
• 作者: Bogani R

A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

具有绑定的类型和范围安全的语法宇宙：它们的语义和证明

• DOI: 10.1017/s0956796820000076
• 发表时间: 2021
• 期刊: Journal of Functional Programming
• 影响因子: 1.1
• 作者: ALLAIS G

Mirages. On Anthropomorphism in Dialogue Systems

海市蜃楼。

• DOI: 10.18653/v1/2023.emnlp-main.290
• 发表时间: 2023
• 作者: Abercrombie G

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively

• DOI: 10.1145/3573105.3575674
• 发表时间: 2023-01
• 期刊: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
• 作者: M. Daggitt;R. Atkey;Wen Kokke;Ekaterina Komendantskaya;Luca Arnaboldi-

Neural Network Robustness as a Verification Property: A Principled Case Study

• DOI: 10.1007/978-3-031-13185-1_11
• 发表时间: 2021-04
• 期刊: ArXiv
• 作者: Marco Casadio;Ekaterina Komendantskaya;M. Daggitt;Wen Kokke;Guy Katz;Guy Amir;Idan Refaeli