From: Ben Goertzel (ben@goertzel.org)
Date: Thu Nov 11 2004 - 08:32:47 MST
Christian,
One key point is that, while embodiment and physical experience are
certainly not necessary guidance for theorem-provers *in general*, it
happens that our existent mathematics is HUMAN mathematics which is mostly
metaphorically grounded in human experience (spatial geometry, language,
etc.). Thus a system sharing some human commonsense intuitions will have an
advantage at dealing with human-created mathematics, although it wouldn't
necessary have an advantage in the greater space of all mathematical
theorems and proofs...
-- Ben
> -----Original Message-----
> From: owner-sl4@sl4.org [mailto:owner-sl4@sl4.org]On Behalf Of Christian
> Szegedy
> Sent: Thursday, November 11, 2004 6:59 AM
> To: sl4@sl4.org
> Subject: Re: Calculemus
>
>
> Ben Goertzel wrote:
>
> >Christian,
> >
> >Do you know the book "Where Mathematics Comes From?" by Lakoff and Nunez.
> >It explores the foundations of mathematical concepts in
> cognitive psychology
> >and embodied experience. I think it well summarizes the essence
> of what's
> >missing in contemporary theorem-proving technology.
> Mathematical proofs, as
> >created by humans, are guided by mathematical intuition, which is mostly
> >grounded in physical and linguistic intuition suitably abstracted. This
> >metaphorical grounding constrains our search through proof space, making
> >some valid proofs opaque to us but compensating but cutting through the
> >otherwise unmanageable combinatorial explosion. Without this sort of
> >grounding, mathematical theorem-provers have nothing to guide them but
> >generic search heuristics, which are far far far too inefficient
> to produce
> >nontrivial proofs without human guidance.
> >
> I agree to some extent, but I am unsure whether mimicking human
> thinking is
> the best approach. Of course, as long as there is not anything better,
> it is a good idea. The nature developed methods which can be
> inferior under
> slightly different cicrcumstances: if we build roads, cars are superior to
> quadrupeds. Evolutionary methods are slow. Neural networks are inefficient
> on current hardware. We can choose different, more efficient ways than
> nature uses. The human thinking is the result of a long
> cumbersome emergent
> process. Some parts work efficiently, some are simply workarounds for
> problems that could be eliminated by better overall design.
>
> I think that the correct approach is to cut the whole deducton
> problem into
> smaller subproblems, specify clear goals, meeasurable objective
> functions for the parts and try to find mathematical optimization methods
> to solve the subproblems efficiently. Whether these methods resemble
> human thinking seems to be irrelevant.
>
> >Thus I argue that, although theorem-proving may indeed be part of an AGI
> >system, getting advanced theorem-proving to work based on human-based
> >mathematics as an initial knowledge base requires a system that
> has a system
> >of internal schemata representing basic physical and linguistic phenomena
> >(measuring, grouping, building, continuous paths, etc. etc.). These
> >experientially grounded schemata are what will allow future
> >advanced-theorem-proving AGI's to create inductive and abductive
> hypotheses
> >that guide their deductive inference.
> >
> >
> >
> Experimental guiding is a natural and good idea, However, I am
> not sure that
> it is necessary to have "real-life" or simulated phyiscal experience
> for pure
> mathematical problem solving.
>
> My intuition is that an AI that could perform experiments on
> mathematical objects
> developed by itself, could perform very well. Of course, pure symbolic
> reasoning like in todays theorem provers is not enough: a theorem prover
> system
> must be able to test the semantics of the mathematical statement by
> performing
> mathematical experiments, hence the necessity of the integration of
> theorem-provers
> and computer-algebra (and optimization) systems. I think that this type
> of experience
> (plus experience about the performance of internal algorithms) could be
> enough
> for a good AI.
>
> This is like a primal-dual optimization approach: the primal world is
> the world of
> formal statement, the dual is the semantics of those statements. When
> looking for
> a proof (a path in the primal world), you can eliminate false paths by
> looking at
> the dual function, just like in mathematical optimization.
>
> > So advanced theorem-proving will emerge from embodied,
> experientially-savvey
> > AGI.
>
> I think that a good AGI would emerge from a synthesis of different
> concepts including formal deduction.
>
>
>
This archive was generated by hypermail 2.1.5 : Tue Feb 21 2006 - 04:22:48 MST