MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS

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 formalisation
of 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 representation
of 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.

Impact Summary.

1. Knowledge (science and technology).
The proposed research is a pilot attempt to merge two very different groups of methods -
statistical machine learning and formal methods - using a third group of coalgebraic methods as a method of abstraction and suitable representation.
The ultimate goal for the resulting technique is to advance real-life applications of ITPs,
in the aspects where decidable algorithms and methods are not possible.
The project is distinctly interdisciplinary and has an original research idea and methodology underlying it.
My discussions of the proposed idea and method with
various groups of researchers at AI4FM'11 (AI and Formal Methods community), STP'11 (Theorem Proving community),
and ITP'11 [f] (Inductive Logic and Machine Learning communities) have confirmed my belief that
my approach is indeed new and ground-breaking, (see also letters of support).


I see the EPSRC First Grant scheme as an excellent opportunity to invest efforts into proving the concept,
developing more evidence and accumulating data supporting the proposed ML-CAP method, with a view to a bigger project if the pilot studies are successful.
Another important consequence of the proposed work will be
building confidence among various communities of researchers in both AI and Formal Methods in the potential of
statistical machine-learning methods as useful tools in handling
undecidable aspects of automated reasoning.

2. Economy and Society.
The project contributes to a long-term goal of
achieving the Grand Challenge in Computing - Dependable systems evolution;
as explained in detail in the Background section.

The proposed method will help to automate those
steps in formal proofs that cannot be automated using the state-of-the-art technology available today.
The new technology will directly affect programmers working on software and hardware verification.
In the longer term, the new method will make the process of software verification by means of ITPs lighter, faster, and hence cheaper,
and thus will have serious economic impact.
Also, ML-CAP will work towards creation of new technologies, and therefore may trigger creation of new companies.

As Formal methods improve dependability and security of software, development of these technologies will ultimately have an effect on the Society in terms of the security and quality of life.
As A. Ireland states in the attached letter of support,
``The pervasive nature of software means that software dependability plays a crucial role within the
world economy, as well as the security - from maintaining national security through to protecting
personal data.''


3. People.
In terms of new skill development, the project will affect the newly established group ``Theory of Computing and AI'' at Dundee,
and e.g. my current Honours, MSc and PhD students, as it will create a more vibrant research environment for them,
as well as reinforce our links with researchers from the partner universities in the UK and abroad.