From: Marc Geddes (marc_geddes@yahoo.co.nz)
Date: Sun Apr 04 2004 - 23:44:10 MDT
--- Ben Goertzel <ben@goertzel.org> wrote: >
> Hi Marc,
>
> I have some comments about AGI and mathematical
> reasoning, and also
> about fundraising strategy for your project.
>
> About AGI and mathematical reasoning...
>
> I have long been interested in using the Mizar
> corpus (www.mizar.org) as
> a resource for helping teach AGI's mathematics.
Fascinating, fascinating. I'll check it out.
>
> Mizar is a knowledge base that consists of a large
> amount of
> mathematical knowledge, encoded in a purely formal
> language. (Comparing
> Mizar articles with typical mathematics research
> papers is very
> instructive in terms of how *informal* typical
> mathematical discourse
> is.)
>
> However, the formal language of Mizar is large and
> complicated; a first
> step would be merely to translate Mizar into a
> simpler formal language,
> such as some kind of variant of predicate calculus.
> (Note: My own AI
> system, Novamente, does not use predicate calculus
> or anything terribly
> similar, but, predicate calculus is commonly
> understood, and it's simple
> enough that converting predicate calculus into
> Novamente node-and-link
> structures or pretty much anything else isn't a big
> trick.)
>
> The purpose of translating Mizar into a simpler
> formalism is that one
> can then feed Mizar -- this vast corpus of
> mathematical reasoning --
> into one's AI system, and allow one's AI system to
> learn how
> mathematical reasoning has been done in many past
> cases. The main
> point isn't the *theorems* per se, it's the *proof
> patterns*, both
> low-level and abstract.
> At any rate, this is my best bet regarding how to
> get an AI system to do
> mathematics really well.
Excellent ideas.
>
> The alternative to a Mizar-based approach, in my
> opinion, is to begin
> not with mathematics but with *natural language
> processing*, so that the
> AI system can be taught mathematics by humans.
>
> Without Mizar (or something similar) or NLP, you're
> asking an AI system
> to learn mathematics by all by itself, and that's
> very very hard. By
> "learn mathematics" here, I mean "learn the subtle
> patterns of
> demonstration and hypothesis that characterize
> creative mathematical
> thinking".
I'm thinking (or hoping) that it's a somewhat simpler
task than full-blown AGI. What I also like is that
mathematical problems are well-defined and results are
clear-cut.
>
> Now, about fundraising.
>
> My guess is that you'll have a better chance at
> raising the funds you
> want if you can first demonstrate some notable
> success at a simpler
> mathematical theorem-proving task. The Riemann
> Hypothesis is a big
> goal, obviously.
Well, needless to say, if I ever pull off a proof of
the Riemann Hypothesis all the funding problems would
be over for good. I'd be world famous - ;)
The reason I mentioned the Riemann Hypothesis is
precisely because of the huge interest it generates.
I'm thinking people would 'sit up and take notice' if
I'm actually shooting for some big goal of great
interest, but at the same thing something which is
more understandable and modest than AGI.
But in practise the solution is not the important
thing. It's the proccess of trying to get there that
I'm thinking would generate some results.
>
> The current state of mathematical theorem-provers is
> not very
> impressive, so if you have a genuinely innovative
> and high-quality AGI
> design with a theorem-proving orientation, it
> shouldn't be sooooo hard
> to beat the state of the art. Current
> theorem-provers really only
> perform adequately when given continual human
> guidance regarding the
> choice of which "proof path" to take.
Hmm.
>
> In the Mizar-based approach, mentioned above, it
> would probably be
> fairly simple to make unprecedented progress in
> mathematical
> theorem-proving just by loading Mizar into a
> reasonably robust
> AGI-oriented architecture and letting it lern some
> proof-patterns, and
> setting it loose to prove theorems in a relatively
> compactly
> formalizable domain like set theory or topology.
Good. The reason for the emphasis on mathematics is
that I want something with well defined results and
good prospects for business applications or results of
monetary value (for funding).
Certainly, theorem provers would have a good demand in
many different scientific appplications.
>
> Without demonstrable preliminary results, my guess
> is that in order to
> raise funding you'll need to get someone with some
> record of success in
> automated theorem-proving involved. Unfortunately,
> everyone I know in
> that community is rather conservative in orientation
> and would be
> unlikely to get involved in a project they viewed as
> highly speculative.
> But perhaps my constacts are not representative of
> that community!
>
> Best of luck!
> Ben Goertzel
>
I must say, I like the way you've been 'playing it'
for your own projects. Far smarter than 'Sing Inst'
in my opinion. I think the business-oriented model is
the way to go. For any AGI Project to get on-going
funding, I think what is needed is an emphasis on a
series of more modest, shorter-term applications -
which have clearly defined results and some potential
monetary value. That's why I'm looking the 'theorem
prover' angle.
I'll see what I can do before the end of the year to
raise some interst in N.Z and Australia. At the very
least there will be a new Institute with a team of one
working away part-time ;)
Cheers
=====
"Live Free or Die, Death is not the Worst of Evils."
- Gen. John Stark
"The Universe...or nothing!"
-H.G.Wells
Please visit my web-site: http://www.prometheuscrack.com
Find local movie times and trailers on Yahoo! Movies.
http://au.movies.yahoo.com
This archive was generated by hypermail 2.1.5 : Tue Feb 21 2006 - 04:22:35 MST