MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS

形式推理的一些步骤本质上可能是统计的或归纳的。许多形式化或利用形式化推理的归纳或统计性质的尝试与神经符号整合、归纳逻辑和关系统计学习的方法有关。该建议侧重于自动定理证明的一个统计/归纳方面——证明模式识别。高阶交互定理证明（如HOL或Coq）已经成功地发展到复杂的机械证明环境中。无论这些证明是应用于软件验证中的大型工业任务，还是应用于数学理论的形式化，程序员都可能不得不处理成千上万的大小和复杂性各异的引理和定理。这种语言中的证明是通过组合有限数量的策略来构建的。有些证明可能会产生相同的策略模式，并且可以完全自动化，而其他证明可能需要用户的干预。在这种情况下，手动找到一个有问题引理的证明可以作为需要手动证明的其他几个引理的模板。目前，这种证明模式识别和回收是手工完成的，ML-CAP项目将研究自动化这一过程的方法。另一个问题是，在证明搜索的试错阶段，不成功的证明尝试通常在找到证据后被丢弃。方便的是，统计机器学习固有的正反例分析。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.