[FOM] Talk on Formal Verification

[Josef Urban]

I don't think today's AI "requires us to write detailed, formal
algorithms". This has been true perhaps in 1980s.

In the last twenty or so years, the "data-driven paradigm" has managed
to produce very significant breakthroughs in AI. This applies to many
areas like image recognition, self-driving cars, language translation,
web search, recently also game (chess, go) playing, etc. Writing
detailed formal algorithms has been more and more replaced by using
generic "meta-algorithms" that learn the very complicated "intelligent
algorithms" from data.

Following is a quote about that from John Shawe-Taylor's and Nello
Cristiani's book Kernel Methods for Pattern Analysis:

"Many of the most interesting problems in AI and computer science in
general are extremely complex often making it difficult or even impossible
to specify an explicitly programmed solution. As an example consider the
problem of recognising genes in a DNA sequence. We do not know how to
specify a program to pick out the subsequences of, say, human DNA that
represent genes. Similarly we are not able directly to program a computer to
recognise a face in a photo. Learning systems offer an alternative methodology
for tackling these problems. By exploiting the knowledge extracted
from a sample of data, they are often capable of adapting themselves to infer
a solution to such tasks. We will call this alternative approach to software
design the learning methodology. It is also referred to as the data driven or
data based approach, in contrast to the theory driven approach that gives
rise to precise specifications of the required algorithms."

Josef


On Fri, Feb 5, 2016 at 1:39 AM, Walt Read <walt.read at gmail.com> wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom