EPSRC Reference: 
EP/J014222/1 
Title: 
MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS 
Principal Investigator: 
Komendantskaya, Dr E 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
School of Computing 
Organisation: 
University of Dundee 
Scheme: 
First Grant  Revised 2009 
Starts: 
01 March 2012 
Ends: 
28 February 2014 
Value (£): 
100,268

EPSRC Research Topic Classifications: 
Artificial Intelligence 
Fundamentals of Computing 

EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
07 Dec 2011

EPSRC ICT Responsive Mode  Dec 2011

Announced


Summary on Grant Application Form 
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 NeuroSymbolic Integration, Inductive Logic and Relational Statistical Learning.
The proposal is focused on one statistical/inductive aspect of automated theorem proving  proofpattern recognition.
Higherorder 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 proofpattern recognition and recycling is done by hand, and the MLCAP project will look into methods to automate this.
Another issue is that unsuccessful attempts of proofs  in the trialanderror phase of proofsearch, are normally discarded once the proof is found.
Conveniently, analysis of both positive and negative examples is inherent in statistical machine learning. And MLCAP is going to exploit this.
However, applying statistical machinelearning 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 wellformed 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 machinelearning algorithms is related to their computational complexity.
Many essential logic algorithms are Pcomplete and inherently sequential (e.g., firstorder 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 proofpatterns 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.
MLCAP 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 wellformed proofs from illformed; distinguish whether a proof belongs to a given family of proofs,
and even make accurate predictions concerning potential success of a proofinprogress. 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.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 
http://staff.computing.dundee.ac.uk/katya/MLCAPman/ 
Further Information: 

Organisation Website: 
http://www.dundee.ac.uk 