AISEC: AI Secure and Explainable by Construction

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

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.