Embedding Machine Learning within Quantifier Elimination Procedures

将机器学习嵌入量词消除程序中

基本信息

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

来源：
https://gtr.ukri.org/projects?ref=EP%2FR019622%2F1
关键词：
Embedding Machine Learning within Quantifier

项目摘要

This project concerns computational mathematics and logic. The aim is to improve the ability of computers to perform ``Quantifier Elimination'' (QE). We say a logical statement is ``quantified'' if it is preceded by a qualification such as "for all" or "there exists". Here is an example of a quantified statement: "there exists x such that ax^2 + bx + c = 0 has two solutions for x".While the statement is mathematically precise the implications are unclear - what restrictions does this statement of existence force upon us? QE corresponds to replacing a quantified statement by an unquantified one which is equivalent. In this case we may replace the statement by:"b^2 - 4ac > 0", which is the condition for x to have two solutions.You may have recognised this equivalence from GCSE mathematics, when studying the quadratic equation. The important point here is that the latter statement can actually be derived automatically by a computer from the former, using a QE procedure.QE is not subject to the numerical rounding errors of most computations. Solutions are not in the form of a numerical answer but an algebraic description which offers insight into the structure of the problem at hand. In the example above, QE shows us not what the solutions to a particular quadratic equation are, but how in general the number of solutions depends on the coefficients a, b, and c.QE has numerous applications throughout engineering and the sciences. An example from biology is the determination of medically important values of parameters in a biological network; while another from economics is identifying which hypotheses in economic theories are compatible, and for what values of the variables. In both cases, QE can theoretically help, but in practice the size of the statements means state-of-the-art procedures run out of computer time/memory. The extensive development of QE procedures means they have many options and choices about how they are run. These decisions can greatly affect how long QE takes, rendering an intractable problem easy and vice versa. Making the right choice is a critical, but understudied problem and is the focus of this project. At the moment QE procedures make such choices either under direct supervision of a human or based on crude human-made heuristics (rules of thumb based on intuition / experience but with limited scientific basis). The purpose of this project is to replace these by machine learning techniques. Machine Learning (ML) is an overarching term for tools that allow computers to make decisions that are not explicitly programmed, usually involving the statistical analysis of large quantities of data. ML is quite at odds with the field of Symbolic Computation which studies QE, as the latter prizes exact correctness and so shuns the use of probabilistic tools making its application here very novel. We are able to combine these different worlds because the choices which we will use ML to make will all produce a correct and exact answer (but with different computational costs). The project follows pilot studies undertaken by the PI which experimented with one ML technique and found it improved upon existing heuristics for two particular decisions in a QE algorithm. We will build on this by working with the spectrum of leading ML tools to identify the optimal techniques for application in Symbolic Computation. We will demonstrate their use for both low level algorithm decisions and choices between different theories and implementations. Although focused on QE, we will also demonstrate ML as being a new route to optimisation in Computer Algebra more broadly and work encompasses Project Partners and events to maximise this. Finally, the project will deliver an improved QE procedure that makes use of ML automatically, without user input. This will be produced in the commercial Computer Algebra software Maple in collaboration with industrial Project Partner Maplesoft.

该项目涉及计算数学和逻辑。目的是提高计算机执行``量化器''''（QE）的能力。我们说，逻辑上的陈述是``量化''，如果它先于诸如“全部”或“存在”之类的资格。这是一个量化语句的一个示例：“存在X，使AX^2 + Bx + C = 0具有X的两个解决方案。量化宽松对应于量化的量化语句用无序的语句替换为等效的语句。在这种情况下，我们可以通过以下方式替换以下陈述：“ B^2-4ac> 0”，这是X具有两个解决方案的条件。在研究二次方程时，您可能已经认识到GCSE数学的同等性。这里的重要一点是，后者实际上可以使用QE Procedure的计算机自动派生。解决方案不是数值答案的形式，而是代数描述，该描述提供了对当前问题结构的见解。在上面的示例中，量化宽松不是向我们展示特定二次方程的解决方案，而是解决方案数量的依赖于系数A，B和C.QE在整个工程和科学中都有许多应用。生物学的一个例子是确定生物网络中参数的医学重要值。尽管经济学的另一个是确定经济理论中哪些假设是兼容的，以及变量的价值。在这两种情况下，量化宽松在理论上都可以提供帮助，但实际上，语句的大小意味着最先进的过程用完了计算机时间/内存。量化宽松程序的广泛发展意味着他们对如何运行有许多选择和选择。这些决定可以极大地影响量化宽松的时间，使一个棘手的问题变得容易，反之亦然。做出正确的选择是一个关键的问题，但研究了，这是该项目的重点。目前，量化宽松程序在人类的直接监督下或基于原始的人为启发式法（基于直觉 /经验的经验法则，但科学基础有限）做出这样的选择。该项目的目的是通过机器学习技术替换这些。机器学习（ML）是允许计算机做出未明确编程的决策的工具的总体术语，通常涉及大量数据的统计分析。 ML与研究量化宽松的符号计算领域相当不利，因为后者估计了确切的正确性，因此避开了概率工具的使用，从而使其在这里应用非常新颖。我们能够结合这些不同的世界，因为我们将使用ML做出的选择都会产生正确而确切的答案（但具有不同的计算成本）。该项目遵循PI进行的试点研究，该研究通过一种ML技术进行了实验，并发现它在QE算法中的两个特定决策的现有启发式方面有所改善。我们将通过使用领先的ML工具来识别用于符号计算中应用的最佳技术来建立在此基础上。我们将证明它们在不同理论和实现之间的低级算法决策和选择中的使用。尽管专注于量化宽松，但我们还将证明ML是在计算机代数中更广泛地进行优化的新途径，并且工作涵盖了项目合作伙伴和事件以最大程度地实现这一目标。最后，该项目将提供改进的量化量化宽松过程，无需用户输入即可自动使用ML。这将与工业项目合作伙伴Maplesoft合作在商用计算机代数软件枫木中生产。