Answers.Body: <p>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.</p>
  
  <p><strong>Artificial Networks Performing Logical Inference</strong></p>
  
  <p>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 <a href="https://nlp.stanford.edu/pubs/bpm_logical_semantics.pdf" rel="nofollow noreferrer"><em>Recursive Neural Networks Can Learn Logical Semantics</em> by Samuel R. Bowman, Christopher Potts, and Christopher D. Manning</a>.</p>
  
  <p>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.</p>
  
  <p><strong>Distinct from Automatic Theorem Proving</strong></p>
  
  <p>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.</p>
  
  <p>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.</p>
  
  <ul>
  <li>Learning the known first order predicate logic rules of inference</li>
  <li>Learning the mechanics of applying those rules to proposed theorems</li>
  <li>Learning functional heuristics to know what to try first</li>
  </ul>
  
  <p><strong>Evidence It Can Be Done</strong></p>
  
  <p>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.</p>
  
  <p>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.</p>
  
  <p>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.</p>
  
  <p><strong>Public Access</strong></p>
  
  <p>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.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2018-08-13T01:00:32.233Z
Answers.LastActivityDate: 2018-09-24T17:54:56.457Z
Answers.LastEditDate: 2018-09-24T17:54:56.457Z
Answers.UserDisplayName: Douglas Daseeco
Answers.Body: <p><a href="https://en.wikipedia.org/wiki/Nim" rel="nofollow noreferrer">Nim was actually</a> one of the first games ever played by an electronic machine. It was called the Nimatron and was displayed at the 1940 New York World's Fair.</p>
  <p>It is also well known that neural networks can model the Xor-function, if they have enough layers. Despite that, Marvin Minsky is supposed to have killed neural networks in the sixties, by asserting that networks with a single hidden layer, cannot model XOR.</p>
  <p>I think there were also some large scale projects to classify finite groups using computers.</p>
  <p>Additionally, there have long been <a href="https://en.wikipedia.org/wiki/Automated_theorem_proving" rel="nofollow noreferrer">automated theorem-proving program</a>s, that had some success in mathematical logic. I recently saw <a href="https://arxiv.org/pdf/1606.04442.pdf" rel="nofollow noreferrer">a paper</a> that used deep learning to improve one of these theorem provers.</p>
  <p>That being said, doing real mathematics is probably as difficult as real language understanding. There doesn't seem to have been a real breakthrough yet.</p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-12-07T13:28:04.303Z
Answers.Text: May I ask 1) where did Marvin Minsky went wrong? 2) i suppose AI to classify groups still needs human input on the “group” concept? How far is AI from “invent” the concept? Similar to “recognise” an XOR operation for nim?
Answers.UserDisplayName: athos
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-12-07T14:02:15.827Z
Answers.Text: Marvin Minsky didn't go wrong. It was just that the readers of his book over interpreted his statements. Yes, I'm not even sure the group classification can be called AI. I don't know when AI will "invent" the concept of a group, nor am I sure what that would even look like.
Answers.UserDisplayName: BlindKungFuMaster
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2017-12-07T12:33:03.930Z
Answers.LastActivityDate: 2020-06-28T22:18:23.757Z
Answers.LastEditDate: 2020-06-28T22:18:23.757Z
Answers.UserDisplayName: BlindKungFuMaster
Body: <p>Currently, AI is advancing fast in deep learning: <a href="http://www.telegraph.co.uk/science/2017/12/06/entire-human-chess-knowledge-learned-surpassed-deepminds-alphazero/" rel="nofollow noreferrer">Entire human chess knowledge learned and surpassed by DeepMind's AlphaZero in four hours</a>.</p>
  <p>As a layman, I'm taking this as a quite powerful searching algorithm, using artificial neural networks to identify the patterns of each game.</p>
  <p>However, how good is AI doing in math?</p>
  <p>For example, the key to the theory of the game <a href="https://en.wikipedia.org/wiki/Nim" rel="nofollow noreferrer">Nim</a> is the binary digital sum of the heap sizes, that is, the sum (in binary) neglecting all carries from one digit to another. This operation is also known as <a href="https://en.wikipedia.org/wiki/Exclusive_or" rel="nofollow noreferrer">&quot;exclusive or&quot; (xor)</a> or &quot;vector addition over GF(2)&quot;.</p>
  <p>Is AI good enough to discover/invite operations/logics such as &quot;exclusive or&quot;, or, more advanced, abstract algebra in <a href="https://en.wikipedia.org/wiki/Finite_field" rel="nofollow noreferrer">finite field</a>?</p>
  
Comments.ContentLicense: CC BY-SA 3.0
Comments.CreationDate: 2017-12-09T19:06:31.847Z
Comments.Text: Look into J.Pitrat's blog, e.g. [mathematics have disappointed me](http://bootstrappingartificialintelligence.fr/WordPress3/2017/10/mathematics-have-disappointed-me/)
Comments.UserDisplayName: Basile Starynkevitch
Tags: <deep-learning><math><agi><applications><state-of-the-art>
Title: How good is AI in math?
UserDisplayName: athos
ThreadText: # How good is AI in math?
  
  (Asked by: username_0 on 2017-12-07)
  
  Currently, AI is advancing fast in deep learning: [Entire human chess knowledge learned and surpassed by DeepMind's AlphaZero in four hours](http://www.telegraph.co.uk/science/2017/12/06/entire-human-chess-knowledge-learned-surpassed-deepminds-alphazero/).
  
  As a layman, I'm taking this as a quite powerful searching algorithm, using artificial neural networks to identify the patterns of each game.
  
  However, how good is AI doing in math?
  
  For example, the key to the theory of the game [Nim](https://en.wikipedia.org/wiki/Nim) is the binary digital sum of the heap sizes, that is, the sum (in binary) neglecting all carries from one digit to another. This operation is also known as ["exclusive or" (xor)](https://en.wikipedia.org/wiki/Exclusive_or) or "vector addition over GF(2)".
  
  Is AI good enough to discover/invite operations/logics such as "exclusive or", or, more advanced, abstract algebra in [finite field](https://en.wikipedia.org/wiki/Finite_field)?
  
  **Tags:** deep-learning, math, agi, applications, state-of-the-art
  
  > **Comments:**
  > **username_1**: Look into J.Pitrat's blog, e.g. [mathematics have disappointed me](http://bootstrappingartificialintelligence.fr/WordPress3/2017/10/mathematics-have-disappointed-me/)  
  
  ---
  
  ## 2 answers
  
  ### Answer by username_3 on 2017-12-07. Score: 5 | Accepted answer
  
  [Nim was actually](https://en.wikipedia.org/wiki/Nim) one of the first games ever played by an electronic machine. It was called the Nimatron and was displayed at the 1940 New York World's Fair.
  
  It is also well known that neural networks can model the Xor-function, if they have enough layers. Despite that, Marvin Minsky is supposed to have killed neural networks in the sixties, by asserting that networks with a single hidden layer, cannot model XOR.
  
  I think there were also some large scale projects to classify finite groups using computers.
  
  Additionally, there have long been [automated theorem-proving program](https://en.wikipedia.org/wiki/Automated_theorem_proving)s, that had some success in mathematical logic. I recently saw [a paper](https://arxiv.org/pdf/1606.04442.pdf) that used deep learning to improve one of these theorem provers.
  
  That being said, doing real mathematics is probably as difficult as real language understanding. There doesn't seem to have been a real breakthrough yet.
  
  > **Comments:**
  > **username_0**: May I ask 1) where did Marvin Minsky went wrong? 2) i suppose AI to classify groups still needs human input on the “group” concept? How far is AI from “invent” the concept? Similar to “recognise” an XOR operation for nim?  
  > **username_3**: Marvin Minsky didn't go wrong. It was just that the readers of his book over interpreted his statements. Yes, I'm not even sure the group classification can be called AI. I don't know when AI will "invent" the concept of a group, nor am I sure what that would even look like.  
  
  ---
  
  ### Answer by username_2 on 2018-08-13. Score: 2
  
  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](https://nlp.stanford.edu/pubs/bpm_logical_semantics.pdf).
  
  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.
  
  
  ---
  
  