A correct-by-construction approach to approximate computation

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

基本信息

  • 批准号:
    EP/Y000455/1
  • 负责人:
  • 金额:
    $ 88.29万
  • 依托单位:
  • 依托单位国家:
    英国
  • 项目类别:
    Research Grant
  • 财政年份:
    2023
  • 资助国家:
    英国
  • 起止时间:
    2023 至 无数据
  • 项目状态:
    未结题

项目摘要

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)应用和影响生成:我们在系统生物学和数字孪生领域创建案例研究,以验证我们的研究,并与共同创建此提案的学术/工业合作者产生影响。这涉及近似博弈论的发展,因为这两个案例研究都涉及需要在存在不确定性的情况下做出最佳决策的自主代理。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

Radu Mardare其他文献

On the metric-based approximate minimization of Markov Chains
  • DOI:
    10.1016/j.jlamp.2018.05.006
  • 发表时间:
    2018-11-01
  • 期刊:
  • 影响因子:
  • 作者:
    Giovanni Bacci;Giorgio Bacci;Kim G. Larsen;Radu Mardare
  • 通讯作者:
    Radu Mardare
A multiset-based model of synchronizing agents: Computability and robustness
  • DOI:
    10.1016/j.tcs.2007.11.009
  • 发表时间:
    2008-02-14
  • 期刊:
  • 影响因子:
  • 作者:
    Matteo Cavaliere;Radu Mardare;Sean Sedwards
  • 通讯作者:
    Sean Sedwards

Radu Mardare的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

相似国自然基金

Data-driven Recommendation System Construction of an Online Medical Platform Based on the Fusion of Information
  • 批准号:
  • 批准年份:
    2024
  • 资助金额:
    万元
  • 项目类别:
    外国青年学者研究基金项目
均相液相生物芯片检测系统的构建及其在癌症早期诊断上的应用
  • 批准号:
    82372089
  • 批准年份:
    2023
  • 资助金额:
    48.00 万元
  • 项目类别:
    面上项目
用于小尺寸管道高分辨成像荧光聚合物点的构建、成像机制及应用研究
  • 批准号:
    82372015
  • 批准年份:
    2023
  • 资助金额:
    48.00 万元
  • 项目类别:
    面上项目
仿生膜构建破骨细胞融合纳米诱饵用于骨质疏松治疗的研究
  • 批准号:
    82372098
  • 批准年份:
    2023
  • 资助金额:
    48.00 万元
  • 项目类别:
    面上项目

相似海外基金

Translating an MR-guided focused ultrasound system for first-in-human precision neuromodulation of pain circuits
将 MR 引导聚焦超声系统用于人体首个疼痛回路精确神经调节
  • 批准号:
    10805159
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
Trans-synaptic optical control of user-defined synaptic connections
用户定义的突触连接的跨突触光学控制
  • 批准号:
    10732081
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
2023 RNA Nanotechnology Gordon Research Conference and Seminar
2023年RNA纳米技术戈登研究会议暨研讨会
  • 批准号:
    10598881
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
Small RNA interactions with transgenes in genetically modified mosquito lines
小RNA与转基因蚊子品系中转基因的相互作用
  • 批准号:
    10654368
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
Selection of word-formation processes in naming of things in French: a research based on the approach of Construction Grammar
法语事物命名中构词过程的选择:基于构式语法方法的研究
  • 批准号:
    23K12184
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
    Grant-in-Aid for Early-Career Scientists
Genetic Approach to Therapy for DFNA9
DFNA9 的基因治疗方法
  • 批准号:
    10681990
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
Towards the life-cycle sustainability in construction: A Digital twin approach 1=Built environment 2=Digital economy
实现建筑生命周期的可持续性:数字孪生方法 1=建筑环境 2=数字经济
  • 批准号:
    2871816
  • 财政年份:
    2023
  • 资助金额:
    $ 88.29万
  • 项目类别:
    Studentship
Enhancing safety management systems practices on construction projects: A proactive data-driven approach for project safety planning and control
加强建设项目的安全管理系统实践:用于项目安全规划和控制的主动数据驱动方法
  • 批准号:
    556989-2020
  • 财政年份:
    2022
  • 资助金额:
    $ 88.29万
  • 项目类别:
    Alliance Grants
A database construction of asbestos world flow for supply chain analysis: a multi-regional input-output approach
用于供应链分析的石棉世界流量数据库构建:多区域投入产出方法
  • 批准号:
    22K05940
  • 财政年份:
    2022
  • 资助金额:
    $ 88.29万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
Dynamic Nuclear Polarization of Aerosols - A Novel Approach for Imaging Water Vapor and Enabling Lung Imaging
气溶胶的动态核极化——一种水蒸气成像和肺部成像的新方法
  • 批准号:
    10372747
  • 财政年份:
    2022
  • 资助金额:
    $ 88.29万
  • 项目类别:
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了