The question of whether nets can be trained to take over more and more of what was entirely within the domain of production systems was asked (to the dismay of those who worked on first order predicate calculus inference in the LISP community) back in the early 1990s.
Artificial Networks Performing Logical Inference
At Stanford University's Department of Linguistics the learning of the logic required to assemble a semantic graph by an artificial net has been demonstrated and documented in Recursive Neural Networks Can Learn Logical Semantics by Samuel R. Bowman, Christopher Potts, and Christopher D. Manning.
Even the earliest work on artificial networks were targetted toward learning logic, such as the elusive exclusive-or operation, which was achieved by adding a second layer to the original perceptron design and applying what we now call gradient descent.
Distinct from Automatic Theorem Proving
Most of the early work on computer proofs of theorems was based on the production system approach (sometimes call expert systems). These are rules based systems, not artificial networks. It was thought that the rules of predicate logic could be executed in proper sequence by pattern matching the antecedents (conditions in which a mathematical technique based on axiomatic information and already proven theory may be applied) in proper order. Some success was achieved using heuristic meta rules.
Using artificial networks to prove a theorem is an entirely different approach. To take semantic learning further so that an artificial network could learn how to assemble a mathematical proof requires three further levels of abstraction in the network learning model.
- Learning the known first order predicate logic rules of inference
- Learning the mechanics of applying those rules to proposed theorems
- Learning functional heuristics to know what to try first
Evidence It Can Be Done
The evidence that artificial networks may be developed which can learn to construct a mathematical proof is not that current artificial nets can perform some natural language functioning or creatively develop a melody or some interior design. The reason DARPA has traditionally invested in neural network research pointed in the direction of simulating logic is the proof of concept proposed by Minsky.
The strongest evidence that neural networks can potentially learn the various layers of abstraction listed above to actually do math is that human children cannot prove a theorem or even read one out loud understandably, yet some may grow up to be proficient in theorem proving. The biological neural nets of the brain must learn such proficiency.
As of this writing, no counter-example exists that an artificial network cannot achieve the proficiency of Gauss or Gödel, so the idea cannot logically be dismissed. Many advanced research projects continue to target higher cognitive skills as their AI objective.
Public Access
It is likely, since much of the work on logical inference and the investigation into whether artificial networks could be trained to do it was funded by government bodies, that some of the results of research is not available to the public.
