|
|
|
|
|
|
by Almaviva
3799 days ago
|
|
|
Obviously accomplishments like this are interesting for their own sake. But the really interesting question for me is, is there anything here, that is new, that can be used outside of tree-based games of complete information? (A much weaker question, is there anything new here that can be used in other games?) Let's take the ability to match the best humans at various tasks. If we put doing long multiplication better than the best human at "1", and passing the Turing Test at "10", where is a Go playing engine? I'd say less than "2", but still higher than chess. Much higher (but still short of general intelligence, obviously) would be beating the best humans at language translation, proving math theorems, or answering factual questions phrased in natural language. Then, if and when computers can write novels which you'd prefer to read over the best human author, now we're talking. So I think, we don't need to worry about our humanity here yet, and we're not remotely close. Over less than a century we've gone from outperforming humans in arithmetic to outperforming us in things that are a little less like arithmetic but still discrete games modeled by trees and precise searches. |
|
|
There's a lot of similarity. Take math theorem proving, which is an active area of machine learning; the algorithms tend at the moment to look something like create a tree of possible theorems, then the algorithm tries to traverse down the tree towards the target theorem by evaluating each branch by the probability it leads towards the target. Because of the exponential explosion, it's very important to select good theorems to expand at each level of the tree, and the ML algorithms can learn characteristics of good intermediate theorems by learning on the existing corpuses of machine-checkable proofs, which gives them much higher success rates in reaching target theorems. So right now the best theorem-provers can already reprove a lot of existing proofs. But they're using stuff like SVMs last I saw, and were much less sophisticated than a deep q-learner.
Some links: "Theorem Proving in Large Formal Mathematics as an Emerging AI Field", Urban & Vyskocil 2012; "Mathematics in the Age of the Turing Machine", Hales 2014 http://arxiv.org/pdf/1302.2898v1.pdf ; "Josef Urban on Machine Learning and Automated Reasoning" http://intelligence.org/2013/12/21/josef-urban-on-machine-le...