Details of Grant 

EPSRC Reference:	EP/J014222/1
Title:	MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS
Principal Investigator:	Komendantskaya, Professor E
Other Investigators:
Researcher Co-Investigators:
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 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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic 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/MLCAP-man/
Further Information:
Organisation Website:	http://www.dundee.ac.uk