A correct-by-construction approach to approximate computation

一种近似计算的构造修正方法

• 批准号: EP/Y000455/1
• 负责人: Radu Mardare
• 金额: $ 88.29万
• 依托单位: University of Strathclyde
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY000455%2F1
• 关键词: correct; construction; approach; approximate; computation

Correct-by-construction program development uses advanced type systems to describe both the data manipulated by computation, and the correctness of those computations. Embedding correctness within software has many advantages, as certified by several decades of pioneering work in the UK and elsewhere, which have culminated in systems such as Agda, Idris, Coq, Lean, HOL, Isabelle, etc., which are powerful enough to implement this vision and which are now having significant impact in both academia and industry. The main question that motivates this research is: can correct-by-construction programming be extended to computation with approximate values, e.g. in: i) stochastic systems where one needs to handle inherent/simulated randomness; ii) resource limited environments, where exact computation is prohibitively expensive; iii) systems with imperfect/partial recall, where one only has limited information about what has happened or the intentions/trustworthiness of each agent; and iv) non-exact computation where primitive data (e.g. from sensors) is inexact and supplied with error bars. These scenarios arise in e.g. cyber-physical systems, machine learning, robotics, automotive engineering, aerospace, and energy systems. Measuring how close measurements might be from their true values naturally leads to the use of metrics but, despite some successes, their use suffers from a number of drawbacks, e.g. i) metrics defined in one problem domain often do not carry over to others; ii) metrics based upon system structure often do not reflect behavioural similarity and vice-versa; and iii) increasingly accurate models of a system's structure are not guaranteed to have increasingly accurate behaviours to that of the modelled system.We conjecture that these problems are manifestations of the deeper problem that all of the mathematics underpinning computation takes exact equality as primitive, so approximation is built over an exact meta-theory. However, in a recent breakthrough, Mardare and his collaborators introduced Quantitative Algebra (QA) which generalises one of the central pillars of modern mathematics, namely universal algebra (UA), to allow approximate equations in formal reasoning. The generality of this new idea - replacing classical reasoning with a more refined approximate reasoning in the very fabric of mathematics - gives us a new paradigm which supports a rigorous logical framework for a proper approximation theory, where bounds can be handled, convergences proven and limits approximated.This project will transform the theory and applications of approximate computation by designing, implementing and deploying a new language for trusted approximate computation. It involves:i) Mathematical Research: We replicate the shift from UA to QA with a similarly revolutionary one from exact computation to approximate computation by developing new quantitative generalisations of the common mathematical structures underpinning exact computation. Approximate computation will then be driven by these new approximate versions of the key structures that drive exact computation.ii) Type Theory & Programming Languages Research: We develop a core dependent type theory incorporating equality-up-to-approximation and type checking to ensure approximation bounds are adhered to; and we convert our type theory into a usable programming language by developing high level features.iii) Applications and Impact Generation: We create case studies in systems biology and digital twins to validate our research and create impact with academic/industrial collaborators who have co-created this proposal. This involves the development of approximate game theory as both these case studies involve autonomous agents that need to make optimal decisions in the presence of uncertainty.

构造正确程序开发使用高级类型系统来描述计算操作的数据以及这些计算的正确性。在软件中嵌入正确性有很多优势，英国和其他地方数十年的开创性工作已经证明了这一点，这些系统最终形成了 Agda、Idris、Coq、Lean、HOL、Isabelle 等系统，这些系统功能强大，足以实现这一愿景，并且现在在学术界和工业界都产生了重大影响。推动这项研究的主要问题是：构造修正编程是否可以扩展到具有近似值的计算，例如在： i) 需要处理固有/模拟随机性的随机系统； ii) 资源有限的环境，精确计算的成本极其昂贵； iii）具有不完美/部分回忆的系统，其中人们对所发生的事情或每个代理的意图/可信度只有有限的信息； iv) 非精确计算，其中原始数据（例如来自传感器的数据）不精确并且带有误差线。这些场景出现在例如网络物理系统、机器学习、机器人、汽车工程、航空航天和能源系统。测量测量结果与其真实值的接近程度自然会导致使用指标，但尽管取得了一些成功，但它们的使用仍存在许多缺点，例如i) 在一个问题域中定义的度量通常不会转移到其他问题域； ii) 基于系统结构的度量通常不能反映行为相似性，反之亦然； iii）系统结构的日益精确的模型不能保证与建模系统的行为越来越精确。我们推测这些问题是更深层次问题的表现，即所有支撑计算的数学都以精确相等为基元，因此近似是建立在精确元理论之上的。然而，在最近的一项突破中，Mardare 和他的合作者引入了定量代数 (QA)，它概括了现代数学的核心支柱之一，即通用代数 (UA)，以允许在形式推理中使用近似方程。这个新想法的普遍性——在数学结构中用更精确的近似推理取代经典推理——为我们提供了一个新的范式，它支持适当逼近理论的严格逻辑框架，其中可以处理边界、证明收敛性和近似极限。该项目将通过设计、实现和部署一种用于可信近似计算的新语言来改变近似计算的理论和应用。它涉及：i) 数学研究：我们通过对支撑精确计算的常见数学结构开发新的定量概括，以类似的革命性方式从精确计算到近似计算来复制从 UA 到 QA 的转变。然后，近似计算将由这些驱动精确计算的关键结构的新近似版本驱动。ii) 类型理论和编程语言研究：我们开发了一种核心依赖类型理论，结合了近似相等和类型检查，以确保遵守近似边界；我们通过开发高级功能将类型理论转换为可用的编程语言。iii）应用和影响生成：我们在系统生物学和数字孪生领域创建案例研究，以验证我们的研究，并与共同创建此提案的学术/工业合作者产生影响。这涉及近似博弈论的发展，因为这两个案例研究都涉及需要在存在不确定性的情况下做出最佳决策的自主代理。