[FOM] Talk on Formal Verification

[Walt Read]

On Thu, Feb 4, 2016 at 11:56 AM, Colin McLarty <colin.mclarty at case.edu> wrote:
>
> I really doubt that Tim Gowers thought AI would never be able to think of
> factorials in the search for runs of composite numbers.  What could be more
> paradigmatic of composite numbers than factorials, or a more convenient
> source of numbers with many factors?
>
> Colin
>

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. Much of our
highly-trained and culturally conditioned thinking seems so
spontaneous that we think it must be "natural" in some sense. But AI
requires us to write detailed, formal algorithms to generate these
insights, complete with input and carefully specified steps to
progress. Lenat's AM, e.g., was a math discovery program that started
with Lisp functions, made essentially random modifications (e.g.,
changing an AND to an OR) and then tested the new functions for
"interestingness" by certain criteria. It was moderately successful
initially because Lisp, based on the lambda calculus, already somewhat
resembled math. (See Lenat and Brown's "Why AM and Eurisko Appear to
Work".) Of course there are multiple options at each step and most AI
ends up being heuristic search, a search through exponentially growing
trees. I see no reason why a general reasoner would fairly shortly
come up with factorials, unless we put in a heuristic saying "if
you're asked about composites, think factorials" and then keep
checking that possibility every time "composite" comes up as well as
checking all the other heuristics about composites you've added to the
system. (And of course every time "prime" comes up, "composite" comes
up.) Each of these heuristics starts another branch of the search
tree. Try making a list of all possible heuristics for tackling
problems with composites, then write a formal program that takes as
input a specific problem about composites, parses the statement and on
objective criteria prioritizes the heuristics list in some optimal way
and that works for most any "composites" question. In my experience,
formalizing our best thinking is way harder than it looks before you
sit down and actually try to write AI programs.

-Walt