[FOM] Talk on Formal Verification

[David McAllester]

On Thu, Feb 4, 2016 at 6:39 PM, Walt Read <walt.read at gmail.com> wrote:

I spent a good piece of my life working in AI, trying to get computers
> to "understand" and I think there's a serious point here.


​ditto
​


> ​... ​
>  But AI
> requires us to write detailed, formal algorithms to generate these
> insights, complete with input and carefully specified steps to
> progress.


​Not any more. I highly recommend reading the alphago paper in Nature.  Go
is interesting precisely because it seems to require intuition that is not
backed up by proof --- not backed up by anything like a complete case
analysis.  Alphago has a neural net move proposer.  Could a net propose
101! ?  It also has a neural net position evaluator. Could a neural net
truth esitimator decide that "prime numbers don't behave like that".  Of
course alphago's networks have to be trained for the game of go --- the
machine must "build intuition" for the domain.  If we think of mathematics
as a search for proofs it is formally equivalent to a one player game.
Alphago is a very general game architecture.

I'm not saying that alphago immediately gives a solution to automating
mathematics.  But I suspect that gradient descent on continuous computation
--- gradient descent on analog circuits or higher level vector-valued
computation --- can ultimately be adapted to train systems to propose
mathematical ideas and judge likelihood of truth.  Alphago is a very nice
case study.

David
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160205/284f70d2/attachment.html>