Embedding Machine Learning within Quantifier Elimination Procedures

这个项目涉及计算数学和逻辑。其目的是提高计算机执行“量词消除”(QE)的能力。我们说一个逻辑语句是“量化的”，如果它前面有一个限定词，如“for all”或“here Existes”。这里有一个量化陈述的例子：“存在x使得ax^2+bx+c=0对x有两个解”。虽然这一陈述在数学上是精确的，但其含义并不清楚--这一存在陈述对我们施加了什么限制？量化宽松相当于用一个等价的非量化语句替换一个量化语句。在这种情况下，我们可以用“b^2-4ac&gt；0”来代替它，这是x有两个解的条件。当你学习二次方程时，你可能已经从GCSE数学中认识到了这个等价性。这里重要的一点是，后一种表述实际上可以由计算机使用量化宽松程序从前者自动推导出来。量化宽松不受大多数计算的数值舍入误差的影响。解决方案不是以数字答案的形式，而是一种代数描述，它提供了对手头问题结构的洞察。在上面的例子中，QE向我们展示的不是特定二次方程的解是什么，而是解的数量一般如何取决于系数a、b和c。QE在工程和科学中有许多应用。生物学的一个例子是确定生物网络中具有医学重要性的参数值；而经济学的另一个例子是确定经济学理论中的哪些假设是兼容的，以及变量的值是什么。在这两种情况下，量化宽松在理论上都可以有所帮助，但实际上，语句的大小意味着最先进的程序耗尽了计算机时间/内存。量化宽松程序的广泛发展意味着，它们在如何运行方面有很多选择和选择。这些决定可能会极大地影响量化宽松需要多长时间，从而使棘手的问题变得容易，反之亦然。做出正确的选择是一个关键但尚未得到充分研究的问题，也是本项目的重点。目前，量化宽松程序要么在人类的直接监督下做出这样的选择，要么基于原始的人为试探法(基于直觉/经验的经验规则，但科学基础有限)。这个项目的目的是用机器学习技术取代它们。机器学习(ML)是一个重要的术语，指的是允许计算机做出未明确编程的决策的工具，通常涉及对大量数据的统计分析。ML与研究QE的符号计算领域非常不同，因为后者重视精确的正确性，因此避免使用概率工具，使其在这里的应用非常新颖。我们能够组合这些不同的世界，因为我们将使用ML做出的选择都将产生正确和准确的答案(但具有不同的计算成本)。该项目遵循了PI进行的试点研究，该研究试验了一种ML技术，发现它改进了QE算法中两个特定决策的现有启发式方法。我们将以此为基础，通过使用领先的ML工具来确定在符号计算中应用的最佳技术。我们将演示它们在低级算法决策以及不同理论和实现之间的选择中的使用。虽然我们专注于量化宽松，但我们也将展示ML作为一条在更广泛的计算机代数中进行优化的新途径，并围绕项目合作伙伴和活动来最大化这一点。最后，该项目将提供一个改进的量化宽松程序，无需用户输入即可自动使用ML。这将与工业项目合作伙伴Maplesoft合作，在商业计算机代数软件Maple中制作。

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.