权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

推回柱代数分解的双指数墙

基本信息

批准号：
EP/T015748/1
负责人：
Matthew England
金额：
$ 53.76万
依托单位：
Coventry University
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2021
资助国家：
英国
起止时间：
2021 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FT015748%2F1
关键词：
Pushing Back Doubly Exponential Wall

项目摘要

A statement is quantified if it has a qualification such as "for all" or "there exists". Let us consider an example commonly encountered in high school mathematics when studying quadratics: "there exists x such that ax^2 + bx + c = 0 has two different solutions for x". The statement is mathematically precise but the implications are unclear: what restrictions does this statement of existence force upon us? Quantifier Elimination (QE) replaces such a statement by an equivalent unquantified one, in this case by "either a is not zero and b^2 - 4ac is greater than 0, or all of a=b=c=0". The quantifier "there exists" and the variable x have been eliminated. The key points are: (a) the result may be derived automatically by a computer from the original statement using QE; (b) QE uncovers the special case when a=0 which humans often miss!Solutions to QE problems are not numbers but algebraic descriptions which offer insight. In the example above QE did not provide solutions to a particular equation - it told us in general how the number of solutions depends on (a,b,c). QE makes explicit the mathematical structure that was hidden: it is a way to "simplify" or even "solve" mathematical problems. For statements in polynomials over real numbers there will always exist an equivalent formula without the quantification. However, actually obtaining the answer can be very costly in terms of computation, and those costs rise with the size of the problem. We call this the "doubly exponential wall" in reference to how fast they rise. Doubly exponential means rising in line with the power of a power, e.g. a problem of size n costs roughly 2^(2^n). When applying QE in practice, results may be found easily for small problems, but as sizes increase you inevitably hit the wall where a computation will never finish.The doubly exponential wall cannot be broken completely: this rise in costs is inevitable. However, the aim of this project is to "push back the wall" so that lots more practical problems may be tackled by QE. The scale here means that pushing the wall even a small way offers enormous potential: e.g. 2^(2^4) is less than 66,000 while 2^(2^5) is over 4 billion! We will achieve this through the development of new algorithms, inspired by an existing process (cylindrical algebraic decomposition) but with substantial innovations. The first innovation is a new computation path inspired by another area of computer science (satisfiability checking) which has pushed back the wall of another famously hard problem (Boolean satisfiability). The team are founding members of a new community for knowledge exchange here. The second innovation is the development of a new mathematical formalisms of the underlying algebraic theory so that it can exploit structure in the logic. The team has prior experience of such developments and is joined by a project partner who is the world expert on the topic (McCallum). The third innovation is the relaxation of conditions on the underlying algebraic object that have been in place for 40+ years. The team are the authors of one such relaxation (cylindrical algebraic coverings) together with project partner Abraham.QE has numerous applications, perhaps most crucially in the verification of critical software. Also in artificial intelligence: an AI recently passed the U. Tokyo Mathematics entry exam using QE technology. This project will focus on two emerging application domains: (1) Biology, where QE can be used to determine the medically important values of parameters in a system; (2) Economics where QE can be used to validate findings, identify flaws and explore possibilities. In both cases, although QE has been shown by the authors to be applicable in theory, currently procedures run out of computer time/memory when applied to many problem instances. We are joined by project partners from these disciplines: SYMBIONT from systems biology and economist Mulligan.

如果语句具有诸如“对于所有”或“存在”之类的限定条件，则该语句被量化。让我们考虑一个在中学数学中学习二次方程时经常遇到的例子：“存在x，使得ax^2 + bx + c = 0对x有两个不同的解”。这种说法在数学上是精确的，但其含义尚不清楚：这种存在的说法对我们施加了什么限制？量词消除（QE）用一个等效的非量化的语句代替这样的语句，在这种情况下是“a不为零并且b^2 - 4ac大于0，或者所有a=b=c=0”。量词“there exists”和变量x都被去掉了。关键是：(a)结果可以由计算机从使用QE的原始报表自动导出；(b) QE揭示了当a=0时的特殊情况，这是人类经常忽略的！量化宽松问题的解决方案不是数字，而是提供洞察力的代数描述。在上面的例子中，QE并没有提供特定方程的解——它告诉我们解的数量是如何依赖于（a,b,c）的。量化宽松明确了隐藏的数学结构：它是一种“简化”甚至“解决”数学问题的方法。对于实数多项式的表述，总是存在一个不需要量化的等价公式。然而，就计算而言，实际获得答案可能是非常昂贵的，而且这些成本随着问题的规模而增加。我们称其为“双指数墙”，指的是它们上升的速度。双指数意味着随着幂次的幂次上升，例如，规模为n的问题的成本大约为2^（2^n）。在实践中应用QE时，对于小问题可能很容易找到结果，但是随着规模的增加，您不可避免地会遇到计算永远无法完成的瓶颈。双重指数墙不可能被完全打破：成本的上升是不可避免的。然而，该项目的目的是“推倒墙”，以便通过量化宽松解决更多实际问题。这里的规模意味着，即使是很小的一步，也会提供巨大的潜力：例如，2^（2^4）小于66,000，而2^（2^5）超过40亿！我们将通过开发新的算法来实现这一目标，这些算法受到现有过程（圆柱代数分解）的启发，但具有实质性的创新。第一个创新是由计算机科学的另一个领域（可满足性检查）启发的新的计算路径，它推翻了另一个著名的难题（布尔可满足性）。这个团队是一个新的知识交流社区的创始成员。第二个创新是发展了一种新的数学形式化的基础代数理论，使其能够在逻辑中利用结构。该团队之前有过此类开发的经验，并由该主题的世界专家项目合作伙伴（McCallum）加入。第三个创新是放宽了已经存在了40多年的基础代数对象的条件。该团队与项目伙伴Abraham一起设计了一种这样的松弛（圆柱形代数覆盖物）。QE有许多应用，也许最关键的是在关键软件的验证中。同样在人工智能领域：一个人工智能最近通过了使用QE技术的东京大学数学入学考试。该项目将重点关注两个新兴应用领域：(1)生物学，QE可用于确定系统中参数的医学重要值；(2)量化宽松可以用来验证发现、识别缺陷和探索可能性的经济学。在这两种情况下，尽管作者已经证明QE在理论上是适用的，但当前的过程在应用于许多问题实例时耗尽了计算机时间/内存。来自这些学科的项目合作伙伴加入了我们：系统生物学的SYMBIONT和经济学家Mulligan。