MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS

形式推理的某些步骤可能是统计的或归纳的。许多试图形式化或利用形式推理的归纳或统计性质的尝试与神经符号集成、归纳逻辑和关系统计学习的方法有关。建议集中在自动定理证明的一个统计/归纳方面-证明模式识别。高阶交互定理证明器(例如HOL或CoQ)已经成功地开发成用于机械化证明的复杂环境。无论这些证明器是应用于软件验证中的大型工业任务，还是用于数学理论的形式化，程序员都可能不得不处理成千上万个大小和复杂程度不同的引理和定理。用这种语言编写的证明是通过组合有限数量的策略来构造的。一些证明可能产生相同的策略模式，并且可以完全自动化，而另一些可能需要用户干预。在这种情况下，手动为一个有问题的引理找到证明可以作为需要手动证明的其他几个引理的模板。目前，这种证明-模式识别和回收是手工完成的，ML-CAP项目将研究自动化的方法。另一个问题是，不成功的证明尝试-在证据搜索的试错阶段，一旦发现证据，通常就会被丢弃。ML-CAP将利用这一点。然而，由于几个原因，应用统计机器学习方法来分析来自证明论的数据是一项具有挑战性的任务。用正式语言编写的公式具有精确的性质，而不是统计的性质。例如，列表(NIL)可能是一个格式良好的术语，而列表(NOL)-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.