Computational Logic in Artificial Neural Networks
Lead Research Organisation:
University of St Andrews
Department Name: Computer Science
Abstract
The fundamental problem of creating (and then evaluating) automated reasoning systems based upon formally defined logical calculi has been considered for centuries. Arguably, the problem is as old as mathematical logic and even computational mathematics.Among the pioneers in this field were Boole, Peano and Hilbert. Hilbert, in his attempts to find proper foundations of mathematics and a proper formal calculus for it, announced the programme of formalising mathematics using a logical calculus. This program is now commonly called Hilbert's Programme . However, in his well-known Incompleteness Theorem [1931], Gdel proved that, in every sufficiently strong formal system, there is an undecidable proposition. It follows that Hilbert's programme cannot be accomplished, as shown by Church and Turing. However, even after these results, the major question, of how one can create some kind of automated reasoning, or, as it was later called, artificial intelligence, remained of interest. It is an open question whether the human mind acts in accordance with some pre-defined algorithm, whether this algorithm is sound, whether it can be soundly formalised by humans, and whether, if formalised, it can be shown to be sound. Turing's machines stimulated the creation of digital computers; biology and neuroscience became proper scientific disciplines. All this progress increased interest in the general problem of creating a form of artificial intelligence.Connectionism is a movement in the fields of artificial intelligence, cognitive science, neuroscience, psychology and philosophy of mind which hopes to explain human intellectual abilities using the idea of an artificial neural network / a simplified mathematical model of a human brain. One of its areas, Neuro-Symbolic Integration, investigates ways of integrating logic and formal languages with neural networks in order to better understand the essence of symbolic (deductive) and human (developing, spontaneous) reasoning, and to show interconnections between them.Many neuro-symbolic systems have been proposed over the last two decades. However, they have been little used in automated reasoning and computational logic. Now is the right time for development of an alternative to the existing neuro-symbolic networks; for this, our proposed SLD neural networks appear to be a most suitable candidate. SLD neural networks use a novel method of performing the algorithm of first-order SLD-resolution for classical logic programs in neural networks. The resulting neural networks are finite, and embody six learning functions as recognised in neurocomputing.We propose to test our SLD neural networks and apply them to a broader class of logic programs and logics. This will lead us to evaluate their effectiveness, comparing them with orthodox methods used in automated reasoning, on the one hand, and with alternative (non-neural) networks used in computational logic, on the other hand. The culmination of the project will be the creation of a more general, and more abstract, neural network interpreter ready to be used as an automated prover for a broad class of logics and logic programs. By achieving its objectives, the project will have a long-term effect of stimulating research in the areas of Neuro-Symbolic Integration and Cognitive Science.
People |
ORCID iD |
Ekaterina Komendantskaya (Principal Investigator) |
Publications
Bertot Y
(2008)
Inductive and Coinductive Components of Corecursive Functions in Coq
in Electronic Notes in Theoretical Computer Science
Bertot Y
(2009)
Types for Proofs and Programs
Ekaterina Komendantskaya
(2009)
Parallel Term Rewriting in Artificial Neural Networks
in ICNC'09 electronic Proceedings
Ekaterina Komendantskaya (Author)
(2010)
Using Inductive Types for Ensuring Correctness of Neuro-Symbolic Computations
Ekaterina Komendantskaya (Author)
(2010)
Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers
Ekaterina Komendantskaya (Author)
(2009)
Intermediate three -valued regular logics of Kleene
in Logic Studies
Ekaterina Komendantskaya (Author)
(2011)
SHERLOCK - an interface for Neuro-Symbolic systems
Ekaterina Komendantskaya (Author)
(2009)
Parallel Rewriting in Neural Networks
Hill A
(2020)
Proof-Carrying Plans: a Resource Logic for AI Planning
Komendantskaya E
(2020)
Continuous Verification of Machine Learning: a Declarative Programming Approach
Komendantskaya E
(2009)
Sound and Complete SLD-Resolution for Bilattice-Based Annotated Logic Programs
in Electronic Notes in Theoretical Computer Science
Komendantskaya E
(2008)
Logics in Artificial Intelligence
Komendantskaya E
(2011)
Algebra and Coalgebra in Computer Science
Komendantskaya E
(2010)
Unification neural networks: unification by error-correction learning
in Logic Journal of IGPL
Komendantskaya E
(2011)
Algebraic Methodology and Software Technology
Komendantskaya E
(2020)
The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
in Theory and Practice of Logic Programming
N/a N/a (Final Report Data)
(2011)
Coalgebraic derivations in logic programming.
in CSL'11
Stewart R
(2021)
Optimising Hardware Accelerated Neural Networks with Quantisation and a Knowledge Distillation Evolutionary Algorithm
in Electronics
Description | The fundamental problem of creating (and then evaluating) automated reasoning system based upon some formally defined logical calculus has been tackled for centuries. One can argue that the problem is as old as mathematical logic and even computational mathematics. Among famous pioneers in this field were Boole, Peano, Hilbert. Hilbert, in his attempts to find proper foundations of mathematics and a proper formal calculus for it, announced the programme of formalising mathematics using some logical calculus. This program is now commonly called ``Hilbert's Programme". In the famous Incompleteness Theorem [1931] Godel proved that there are undecidable propositions in every axiomatic theory, and thus showed that Hilbert's program cannot be accomplished. Equivalent theorems were proven by Turing and Church. However, even after the famous result of Godel, Turing and Church, the major question of how one can create some kind of automated reasoning, or, as it was later called, artificial intelligence, remained appealing. It remains an open question whether Human mind acts in accordance with some pre-defined algorithm, whether this algorithm is sound, whether it can be soundly formalised by humans, and whether, if formalised, it can be proved to be sound. Turing's machines stimulated the creation of digital computers; biology and neuroscience became proper scientific disciplines. And all this progress only increased interest in the general problem of creating an artificial intelligence. Connectionism is a movement in the fields of artificial intelligence, cognitive science, neuroscience, psychology and philosophy of mind which hopes to explain human intellectual abilities using artificial neural networks - a simplified mathematical model of a human brain. One of its areas, Neuro-Symbolic integration, investigates ways of integrating logic and formal languages with neural networks in order to better understand the essence of symbolic (deductive) and human (developing, spontaneous) reasoning, and to show interconnections between them. This EPSRC grant was devoted to studies of various neuro-symbolic methods applicable in automated reasoning. The first research objective was to implement two logic algorithms -- first-order unification and first-order term rewriting -- in artificial neural networks. This goal was achieved, and the software is now published on-line on the project's webpage; the major results are published in journal and conference proceedings. This work was taken to a more general and abstract level by a successive novel method ML-CAP (for ``machine-learning coalgebraic automated proofs") that can use statistical machine learning tools such as Support Vector Machines and Neural networks to determine general properties of formal proofs by detecting variations of proof patterns. The novel ML-CAP method was developed and formulated during the EPSRC PDRF fellowship. Among other things, this method required a careful study of coalgebraic semantics of logic programs, which was undertaken during this grant. These studies led to a new coalgebraic proof procedure for first-order logic programs and laid foundations for the ML-CAP. The method ML-CAP has become the subject of my present and future studies, and is already approved for support by the EPSRC First-grant scheme. The following objectives were achieved: 1. To represent the operational semantics of logic programming languages as (artificial) neural networks. 2. To evaluate the effectiveness of these representations compared with orthodox methods such as resolution and analytic tableaux. 3. To refine these representations in the light of evaluations. 4. To seek abstract and more general representations of which the above representations are special cases. 5. To test, implement and experiment with (existing) SLD Neural Networks and the neural networks yet to be obtained (as above), using standard neural networks software. 6. To look for more broad implementation of the developed techniques in automated reasoning and proof theory. However, the evaluation stage of the proposal showed that the proposed method was not optimal. I went on working on a deeper methods that capture statistical aspects of automated theorem proving, and in the last year of my project, I developed a new alternative method for machine-learning coalgebraic automated proofs (ML-CAP) that lay foundation for my new EPSRC grant ML-CAP. Therefore, one can say that there were two main categories of research results acheived within the EPSRC PRRF - and that is implementation and evaluation of the method I had proposed for the Fellowship, and development of a novel, more optimal and successful method that forms my long-term research agenda. |
Exploitation Route | The research can be adapted for use in a range of industrial-scale Artificial Intelligence Applications. The project's web-page provides a guide for anyone wishing to use the produced software or exploit the theoretical results. |
Sectors | Digital/Communication/Information Technologies (including Software) |
URL | http://www.computing.dundee.ac.uk/staff/katya/CLANN/index.html |
Description | MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS |
Amount | £100,268 (GBP) |
Funding ID | EP/J014222/1 |
Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
Sector | Public |
Country | United Kingdom |
Start | 02/2012 |
End | 02/2014 |
Description | SICSA Distinguished Visitor J.Power |
Amount | £3,060 (GBP) |
Organisation | SICSA Scottish Informatics and Computer Science Alliance |
Sector | Academic/University |
Country | United Kingdom |
Start | 06/2010 |
End | 08/2010 |
Description | SICSA Distinguished Visitor K.U.Kuhnberger |
Amount | £2,200 (GBP) |
Organisation | SICSA Scottish Informatics and Computer Science Alliance |
Sector | Academic/University |
Country | United Kingdom |
Start | 09/2009 |
End | 11/2009 |
Description | SICSA Workshop Funding STP 2011 |
Amount | £400 (GBP) |
Organisation | SICSA Scottish Informatics and Computer Science Alliance |
Sector | Academic/University |
Country | United Kingdom |
Start | 05/2011 |
End | 07/2011 |
Description | Neuro-Symbolic discussion group |
Organisation | City, University of London |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | The partnership between the Universities of Dundee, St Andrews, Imperial College, and City University London |
Start Year | 2009 |
Description | Neuro-Symbolic discussion group |
Organisation | Imperial College London |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | The partnership between the Universities of Dundee, St Andrews, Imperial College, and City University London |
Start Year | 2009 |
Title | CLANN software |
Description | Experimental software supporting experiments on Neuro-symbolic tools for performing unification and term-rewriting in neural networks. |
Type Of Technology | Software |
Year Produced | 2009 |
Open Source License? | Yes |
Impact | The impact was mainly research/academic. |
URL | http://staff.computing.dundee.ac.uk/katya/CLANN/CLANNsoftware.html |