Ontic looks like an interesting and elegant formalism, but I don't see how it would help an AGI learn mathematics. We are not yet at the point where we can solve word problems like "if I pay for a $4.95 item with a $10 bill, how much change should I get back?" Never mind the harder problem of proving theorems.
Learning word problems seems to me related to learning high level grammar. I have 3 apples and eat one. 3 - 1 = 2. I have 2 apples left. I have 15 dollars and spend 6. 15 - 6 = 9. I have 9 dollars left. After many examples, we learn the pattern: I have X (noun)s and (remove) Y. X - Y = Z. I have Z (noun)s left. And we do this thousands of times with many different patterns. The problem is hard because it requires learning a grammar that spans sentences, and it requires a more complex form of variable substitution than pronoun dereferencing. We have not there yet. The developmental process is: phonemes, word segmentation, semantics, parts of speech, phrases, sentences, paragraphs. Practical language models are still at the level of semantics, and we need to get to the paragraph level. Of course we have to teach an AGI grade school math before we can solve the much harder problem of proving theorems. Unlike simple math, there is no formula for discovering proofs. It is not computable. Mathematicians learn to do it by studying thousands of examples and using lots of heuristics in ways we don't understand. At best, proving theorems is an exponential search problem with no guarantee of success. Even if the problem is well defined, like chess, our understanding of heuristics is poor. Why did Deep Blue need to explore 200,000,000 chess positions per second, compared to 3 per second for Kasparov? --- "J. Storrs Hall, PhD." <[EMAIL PROTECTED]> wrote: > Look also at Ontic: > http://lambda-the-ultimate.org/classic/message6641.html > http://ttic.uchicago.edu/%7Edmcallester/ontic-spec.ps > http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html > http://citeseer.ist.psu.edu/witty95ontic.html > > Josh > > On Saturday 21 April 2007 17:45, Lukasz Stafiniak wrote: > > Hi, > > > > How should an AGI think about formal mathematical ideas? What > > formalization of a logical argument would be the most digestible? Many > > mathematicians don't like formalized approaches, because they think on > > the level of patterns (which correspond to understanding the reality), > > not on the "assembly" level of formalizations. But AGI could take > > advantage of perceiving and manipulating the formalization itself. > > Although I live not far from Bialystok, I don't think Mizar is the > > right formalization to use. Mizar is a sophisticated artificial > > language. What I would like to see used is a powerful, intelligible > > system with frugal formulation, a logic whose assertions combine > > theorems and proofs, and whose proofs are algorithms: the Calculus of > > Inductive Constructions (CIC). The system that implements CIC is Coq > > (http://coq.inria.fr/). The AGI would still need to think on the > > patterns level (sometimes called heuristics), and it would still be > > very useful to translate Mizar to CIC (perhaps the AGI could do the > > translation...) but to have a being embodied at once in the physical > > world and in the CIC world, wow! That would certainly prove something > > ;-) > > > > Best regards, > > Lukasz Stafiniak -- Matt Mahoney, [EMAIL PROTECTED] ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=231415&user_secret=fabd7936
