EnnCore: End-to-End Conceptual Guarding of Neural Architectures

EnnCore将解决基于神经的(NB)架构中的一个基本安全问题，允许系统设计人员指定和验证系统的概念/行为核心，该核心可用于保护NB系统免受意外行为和攻击。它将开创当代可解释神经模型和全栈神经软件验证之间的对话。因此，我们将开发方法、算法和工具来实现完全可验证的智能系统，这些系统是可解释的，其正确行为得到保证，并且对攻击具有健壮性。EnnCore将在三个不同和高影响的应用场景中进行验证：(I)确保用于癌症诊断的人工智能系统(Health-癌症研究英国，The Christie)；(Ii)确保对话代理的道德和法律行为(Health-癌症研究英国，The Christie)；以及(Iii)确保用于需求响应的人工智能系统(Energy-Urbanchain)。使用案例将在一个临床和一个工业合作伙伴的帮助下，在真实世界的数据条件下进行共同设计和验证。因此，EnnCore将解决一个基本研究问题，通过考虑从开发到部署的整个生命周期来确保神经启用组件的安全性。解决这一研究问题将对医疗保健、基于伦理的人工智能和需求响应等领域产生深远影响，这些领域严重依赖安全和可信的软件组件来满足安全关键要求。因此，我们的总体研究目标是对编写安全可信的基于AI的软件组件产生长期影响，从而为完全可验证软件的共同愿景做出贡献，其中基于NB的底层架构是建立在强大的符号和数学保证的基础上的。该项目将通过映射、使用和扩展现有神经符号DNN体系结构(例如，图网络、可微归纳逻辑编程)的可解释性属性，从而通过符号验证、抽象解释和程序合成方法来保护它们，从而推动安全深度神经网络(DNN)模型的发展。EnnCore将开创可解释DNN和正式验证之间的多学科对话。尤其是，EnnCore将为安全关键的NB架构提供保护，具有以下新特性：(1)全栈符号软件验证：我们将开发第一个位精确和可扩展的符号验证框架，以对DNN的实际实施进行推理，从而进一步保证与基础硬件和软件有关的安全属性，这些属性在现有文献中通常被忽视。(2)可解释性/可解释性：EnnCore将率先整合基于知识和神经可解释性的方法，以支持最终用户指定安全约束和诊断安全风险，以便随着NB型号的发展而对其安全性提供保证。将特别注意对安全情景中的语义漂移现象进行定量和定性描述。(3)可伸缩性：我们将系统地结合当代符号方法来解释、解释和验证神经表征。特别是，我们将开发一个神经符号保障框架，将基于结构化知识的表征元素与注意结构元素联系起来，以前所未有的方式实现可伸缩性和精确度。我们还将开发新的学习技术，以便在不同的验证运行中重用信息，以减少公式大小并一致地改进约束求解。

EnnCore will address a fundamental security problem in neural-based (NB) architectures, allowing system designers to specify and verify a conceptual/behavioral hardcore to the system, which can be used to safeguard NB systems against unanticipated behavior and attacks. It will pioneer the dialogue between contemporary explainable neural models and full-stack neural software verification. We will, therefore, develop methods, algorithms and tools to achieve fully-verifiable intelligent systems, which are explainable, whose correct behavior is guaranteed, and that are robust towards attacks.EnnCore will be validated on three diverse and high-impact application scenarios: (i) securing an AI system for cancer diagnosis (health -- Cancer Research UK, The Christie); (ii) ensuring ethical and legal behavior of a conversational agent (health -- Cancer Research UK, The Christie); and (iii) securing an AI system for demand response (energy -- Urbanchain). The use cases will be co-designed and validated under real-world data conditions with the help of one clinical and one industrial partner.As a result, EnnCore will address a fundamental research problem to ensure the security of neural-enabled components by taking into account its entire lifecycle from development to deployment. Solving this research problem will have a far-reaching impact on areas such as health care, ethically grounded AI and demand response, which heavily depend on secure and trusted software components to meet safety-critical requirements. Therefore, our overall research objective is to have a long-term impact on writing secure and trusted AI-based software components, thus contributing to a shared vision of fully-verifiable software, where underlying NB-based architectures are built with strong symbolic and mathematical guarantees.To achieve this objective, EnnCore will design and validate a full-stack symbolic safeguarding system for NB architectures. This project will advance the state-of-the-art in the development of secure Deep Neural Network (DNN) models by mapping, using and extending explainability properties of existing neuro-symbolic DNN architectures (e.g., Graph Networks, Differentiable Inductive Logic Programming), thus safeguarding them with symbolic verification, abstract interpretation and program synthesis methods. EnnCore will pioneer the multi-disciplinary dialogue between explainable DNNs and formal verification.In particular, EnnCore will deliver safeguarding for safety-critical NB architectures with the following novel properties:(1) Full-stack symbolic software verification: we will develop the first bit-precise and scalable symbolic verification framework to reason over actual implementations of DNNs, thereby providing further guarantees of security properties concerning the underlying hardware and software, which are routinely ignored in existing literature.(2) Explainability / Interpretability: EnnCore will pioneer the integration of knowledge-based and neural explainability methods to support end-users specifying security constraints and diagnosing security risks, in order to provide assurances about its security as NB models evolve. Particular attention will be given to the quantitative and qualitative characterization of semantic-drift phenomena in security scenarios. (3) Scalable: we will systematically combine contemporary symbolic methods for explaining, interpreting and verifying neural representations. In particular, we will develop a neuro-symbolic safeguard framework by linking the structural knowledge-based representation elements to the attentional architecture elements, to achieve scalability and precision in an unprecedented manner. We will also develop new learning techniques for reusing information across different verification runs to reduce formulae size and consistently to improve constraint solving.