From: Christian Szegedy (szegedy@or.uni-bonn.de)
Date: Thu Nov 11 2004 - 04:59:29 MST
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