MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS

形式推理中的一些步骤可能是统计或归纳的。许多试图形式化或利用这种归纳或统计性质的形式推理的方法都与神经符号集成，归纳逻辑和关系统计学习有关。该建议集中在自动定理证明的一个统计/归纳方面-证明模式识别。高阶交互式定理证明器（如HOL或Coq）已成功地发展成复杂的环境，用于机械化证明。无论这些证明器是应用于软件验证中的大型工业任务，还是应用于数学理论的形式化，程序员都可能必须处理数千个大小和复杂度可变的引理和定理。有些证明可能会产生相同的策略模式，并且可以完全自动化，而另一些可能需要用户的干预。在这种情况下，手动发现的一个有问题的引理的证明可能会作为其他几个需要手动证明的引理的模板。目前这种证明模式识别和回收是手工完成的，ML-CAP项目将研究自动化的方法。另一个问题是，不成功的证明尝试-在证明搜索的试错阶段，一旦发现证明，通常会被丢弃。方便的是，对正面和负面例子的分析是统计机器学习所固有的。然而，应用统计机器学习方法来分析来自证明理论的数据是一项具有挑战性的任务，原因有几个。用形式语言写的公式具有精确的性质，而不是统计性质。例如，list（nil）可能是一个格式良好的术语，而list（nol）-不是;尽管它们可能具有机器学习方法可识别的相似模式。合并形式逻辑和统计机器学习算法时出现的另一个问题与它们的计算复杂性有关。许多基本逻辑算法是P-完全的，并且固有地是顺序的（例如，作为上述问题的解决方案，自动化证明的共代数方法可以提供正确的抽象技术，允许使用机器学习方法分析证明模式。首先，共代数计算有助于并发性，这可能是获得所概述问题的充分表示的关键。其次，它们基于潜在无限计算的重复模式的思想，而不是有限计算的输出。这些模式可以通过统计模式识别的方法来检测。ML-CAP基于一种在形式证明分析中使用统计机器学习的新方法。总之，它提供了从自动证明中提取这些特征的算法，这些特征允许使用统计机器学习工具（如神经网络）检测证明模式。因此，神经网络可以被训练以区分形式良好的证明和形式不良的证明;区分证明是否属于给定的证明族，甚至对正在进行的证明的潜在成功做出准确的预测。这三个任务在自动推理中都有重要的应用。该项目的目标是推广这种方法，并将其发展成为一种可靠的自动化证明通用技术。它将产生对不同领域的研究人员有用的新方法，如人工智能，形式方法，余代数和认知科学。

Some steps in formal reasoning may be statistical or inductive in nature.Many attempts to formalise or exploit this inductive or statistical nature of formal reasoning are related to methods of Neuro-Symbolic Integration, Inductive Logic and Relational Statistical Learning.The proposal is focused on one statistical/inductive aspect of automated theorem proving -- proof-pattern recognition. Higher-order interactive theorem provers (e.g. HOL or Coq) have been successfully developed into sophisticated environments for mechanised proofs. Whether these provers are applied to big industrial tasks in software verification, or to formalisationof mathematical theories, a programmer may have to tackle thousands of lemmas and theorems of variable sizes and complexities.A proof in such languages is constructed by combining a finite number of tactics. Some proofs may yield the same pattern of tactics, and can be fully automated, and others may require a user's intervention.In this case, manually found proof for one problematic lemma may serve as a template for several other lemmas needing a manual proof.At present this kind of proof-pattern recognition and recycling is done by hand, and the ML-CAP project will look into methods to automate this. Another issue is that unsuccessful attempts of proofs --- in the trial-and-error phase of proof-search, are normally discarded once the proof is found.Conveniently, analysis of both positive and negative examples is inherent in statistical machine learning. And ML-CAP is going to exploit this.However, applying statistical machine-learning methods to analyse data coming from proof theory is a challenging task for several reasons. Formulae written in formal language have a precise, rather than a statistical nature. For example, list(nil) may be a well-formed term, while list(nol) - not; although they may have similar patterns recognisable by machine learning methods.Another problem that arises when merging formal logic and statistical machine-learning algorithms is related to their computational complexity.Many essential logic algorithms are P-complete and inherently sequential (e.g., first-order unification), while neural networks and other similar devices are based on linear algebra and perform parallel computations.As a solution to the outlined problems, the coalgebraic approach to automated proofs may provide the right technique of abstraction allowing to analyse proof-patterns using machine learning methods. Firstly, coalgebraic computations lend themselves to concurrency, and this may be the key to obtaining adequate representationof the outlined problems.Secondly, they are based on the idea of repeating patterns of potentially infinite computations, rather than outputs of finite computations. These patterns may be detected by methods of statistical pattern recognition. ML-CAP is based upon a novel method of using statistical machine learning in analysis of formal proofs.In summary, it provides algorithms for extracting those features from automated proofs that allow to detect proof patterns using statistical machine learning tools, such as neural networks.As a result, neural networks can be trained to distinguish well-formed proofs from ill-formed; distinguish whether a proof belongs to a given family of proofs, and even make accurate predictions concerning potential success of a proof-in-progress. All three tasks have serious applications in automated reasoning. The project will aim to generalise this method and develop it into a sound general technique for automated proofs. It will result in new methods useful for a range of researchers in different areas, such as AI, Formal Methods, Coalgebra and Cognitive Science.