AlphaGeometry: An Olympiad-level AI system for Geometry https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/
On Thursday, January 18, 2024 at 12:32:34 AM UTC-5 Tim Daly wrote: > While the question of human intelligence is interesting > please note that my post topic has been restricted to the > application of GPT-like / AI-like systems to the automation > of proof and computer algebra. > > Given the changes I'm seeing and the research I'm doing it > is likely that there will be a very rapid change from the legacy > version of computer algebra we now use, taking advantage of > the growing power of these systems. > > I've been involved and published in AI-like systems since the 1973, > including such > "AI-like" areas of machine vision, robotics, expert systems, speech, neural > nets, knowledge representation, planning, etc. All of these were considered > "intelligent behavior" ... until they weren't. Indeed, in the 1960s > computer > algebra-like systems were considered "intelligent". > > Intelligence is a "suitcase word" [0], interesting but irrelevant. > > The topic at hand is "computational mathematics", meaning the application > of recent technology (proof assistants, theorem databases, algorithm > proofs, and reasoning assistants) to moving beyond 50-year-old legacy > computer algebra. Proving computer algebra algorithms correct and > providing useful interfaces is the long-term goal. > > Tim > > [0] "Marvin Minsky, in his fascinating book "The Emotion Machine" ... > described > words such as "emotions," "memory," "thinking" and "intelligence" as > suitcase > words - words that mean "*nothing by itself, but holds a bunch of things > inside * > *that you have to unpack*." > > On Wednesday, January 17, 2024 at 10:03:53 PM UTC-5 [email protected] > wrote: > >> Good morning Waldek, >> >> My response will be delving into some areas of philosophical and >> metaphysical response. >> >> On Thu, Jan 18, 2024 at 2:56 AM Waldek Hebisch <[email protected]> wrote: >> >>> On Thu, Jan 18, 2024 at 01:16:55AM +1100, Hill Strong wrote: >>> > On Wed, Jan 17, 2024 at 11:09 PM Tim Daly <[email protected]> wrote: >>> > >>> > They can raise the issue all they like. What they are not seeing is >>> that >>> > artificial stupidity (AI) systems are limited. As I said above. The >>> only >>> > intelligence you will find in these systems is the stuff generated by >>> human >>> > intelligence. No artificial stupidity (AI) system can ever exceed the >>> > limitations of the programming entailed in them. >>> >>> Well, humans are at least as limited: your claim as true as claim >>> that "humans can not ever exceed the limitations of the programming >>> entailed in them". In case of humans programming meaning both things >>> >> >> Though we are limited in every sort of way, we are capable of exceeding >> any programming that is involved in our development. What is so not obvious >> is that there is a category error when comparing humans to any sort of >> machine that we build. Though we can build machines stronger, faster and >> able to handle tedious tasks far better than we can do, due to our very >> distinctive intelligence, we are able to do what no machine can do and that >> is solve the problems that arise. >> >> >> hardcoded in genome and chemical machinery of the body and "learned >>> stuff". Already at age 1 toys, customized environment and interactions >>> >> >> You speak here about [programming] hard-coded in the genome and chemical >> machinery of the human body. But I somehow don't think you realise just how >> far beyond us is that machinery. Within a single living cell, the automatic >> adaptive capabilities are so far beyond our current levels of technology >> that in comparison, we are no more advanced than some caveman when we >> compare the entire planetary industrial and planetary capabilities that we >> have already made. >> >> The more we learn about cellular biology with its internal >> transportation, control and manufacturing systems the more we should be >> recognising that we are not capable of building any computerised system >> that will ever be intelligent. >> >> with other humans make significant difference to learning. At later >>> stages there are stories which were perfected for thousends of years, >>> school curricula and books. There were myths that people from >>> non-western cultures are less "inteligent" than people from western >>> culture. More deeper research showed that part of our "inteligence" >>> is really "programmed" (learned) and "programming" in differnet >>> cultures were different. >>> >> >> Though part of our intelligence is learned there is something that is so >> far beyond this, so that, even though this is an active area of research, >> we haven't a clue as to what this is. >> >> >>> In slightly different spirit, in fifties there were efforts to >>> define inteligence and researcheres from that time postulated >>> several abilities that every inteligent being should have. >>> Based on that there were "proofs" that artificial inteligence >>> is impossible. One of such "proofs" goes as follows: people >>> can prove math theorems. But Goedel and Church proved that >>> no machine can prove math theorem. So no machine will match >>> humans. The fallacy of this argument is classic abuse of >>> quantifiers: humans can prove same (easy) math theorems. >>> >> >> Here you are now arguing against the various incompleteness theorems and >> in doing so, you are entering the realm of metaphysics and philosophy. >> These incompleteness theorems highlight something quite interesting in that >> the basis of our logic and mathematics (the fundamental axioms used) cannot >> be proved true from within our logic and mathematics. We can argue for them >> from metaphysics and philosophy but we are unable to prove them from within >> the systems that are based on those fundamental axioms. >> >> What you have missed here is that any theorems developed within the >> systems are provable based on those unprovable axioms and previously proven >> theorems. That is how we can build up the various systems of mathematics in >> use. However, new mathematical systems require insights not possible to any >> computerised system. These new insights are in the realm of human >> intelligence which does exceed any programming that individual humans may >> be exposed to. >> >> No machine or human can prove _each_ math theorem. Actually, >>> we still do not know how hard is proving, but common belief >>> >> >> All theorems can be proved if they are based on the initial set of axioms >> used. How hard it is to prove the theorem is another matter. >> >> >>> is that complexity of proving is exponential in length of the >>> proof. What is proven is that that there is no computable >>> bound on length of shortest proof. Clearly this difficulty, >>> that is large length of proofs affect humans as much as >>> computers. >>> >> >> Maybe. The thing of interest here is that it is humans who can find >> alternative ways of proving a theorem which is not a part of the exhaustive >> processes previously used. >> >> As you would well know, the Halting problem is not solvable by any Turing >> machine or corresponding alternative. But we can see the problem >> immediately. We make leaps and find solutions that are not possible within >> a logical/mathematical system. >> >> >>> To put is differently, if you put strong requirements on >>> inteligence, like ability to prove each math theorem, then >>> humans are not inteligent. If you lower your requirements, >>> so that humans are deemed inteligent, than appropriately >>> programmed computer is likely to qualify. >>> >> >> Your comment above is false. It is false logically, rationally, >> metaphysically and philosophically. The ability to prove a mathematics >> theorem, if based on previous axioms and theorems, is not a sign of >> intelligence. I would agree that we do this as a part of our intelligence, >> but this is not a sign of intelligence. The axioms used at the fundamental >> level which are designed and specified may well be a sign of intelligence, >> but no computerised system does this. I have spent 40 years looking at >> these kinds of things and every computerised system is based on the human >> intellectual capacity (intelligence) for these systems to even exist. >> >>> >>> One more thing: early in history of AI there was Eliza. >>> It was simple pattern matcher clearly having no inteligence, >>> yet it was able to fool some humans to belive that they >>> communicate with other human (ok, at least for some time). >>> >> >> The ability to fool people does not challenge our intelligence. Every >> human is flawed and can be fooled. We see that every day in every society. >> This does not lessen what humanity has in terms of being intelligent. We >> act irrationally, we act in completely adverse ways. We make decisions that >> make no sense. We even choose options that are not actually available to >> us. We can see this in the recent Iowa caucus where the winner wasn't even >> on the available options. >> >> Machine programming doesn't allow this. Certainly, we can see all sorts >> of errors and when fully studied, we see why those errors occurred. They >> are logically defined. >> >> Some people take this to consider all solved AI problems >>> as kind of fake and show that the problem was not about >>> inteligence. But IMO there is different possiblity: that >>> all our inteligence is "fake" in similar vein. In other >>> >> >> If our intelligence is [fake] then the logical consequence of that >> argument is that there is no mathematics, no scientific investigation, no >> rationality, no intelligence, no progress in any form. This is a >> contradiction. We do do mathematics, we do do scientific investigation, we >> do do philosophy and metaphysics, we do do rational things. >> >> words, we do not solve general problem but use tricks which >>> happen to work in real life. Or to put it differently, >>> >> >> Yes we do do tricks and this is one sign of intelligence here. Certainly >> we are limited and I have been saying such things for a long time. However, >> for all of our limitations, we are in a category that is very different to >> all other things, living or otherwise and we often fail to recognise, let >> alone understand that category difference. >> >> I have seen too many people who dismiss philosophy and metaphysics as >> being useless. Yet it is by these that we show forth our intelligence and >> by which we can justify mathematics and scientific investigation as valid, >> rational and proper intellectual pursuits. >> >> >> we may be much more limited than we imagine. Eliza clearly >>> shows that we can be easily fooled into assuming that >>> something has much more abilities than it really has >>> (and "something" may be really "we"). >>> >>> -- >>> Waldek Hebisch >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "FriCAS - computer algebra system" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> >> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/fricas-devel/Zaf4t0bQZRQAsouA%40fricas.org >>> . >>> >> -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/7847d8fa-e682-4808-9ea6-5cade706234dn%40googlegroups.com.
