> On 18 Apr 2019, at 09:11, Philip Thrift <[email protected]> wrote: > > > > On Wednesday, April 17, 2019 at 8:29:25 PM UTC-5, Russell Standish wrote: > On Wed, Apr 17, 2019 at 06:22:35PM -0700, 'Brent Meeker' via Everything List > wrote: > > > > But how complete must the self-model be. > > That is the 64 million dollar question. > > > As Bruno has pointed out, it can't > > be complete. Current Mars Rovers have some "house keeping"self-knowledge, > > like battery charge, temperature, power draw, next task, location, time,... > > I don't think that's enough. I think it must have the ability to > recognise other (perhaps similar) robots/machines as being like > itself. > > > Of course current rovers don't have AI which would entail them learning and > > planning, which would require that they be able to run a simulation which > > included some representation of themself; but that representation might be > > very simple. When you plan to travel to the next city your plan includes a > > representation of yourself, but probably only as a location. > > > > Hod Lipson's starfish's representation of itself is no doubt rather > simple and crude, but it does pose the question of whether it might > have some sort of consciousness. > > > -- > > ---------------------------------------------------------------------------- > Dr Russell Standish Phone 0425 253119 (mobile) > Principal, High Performance Coders > Visiting Senior Research Fellow [email protected] <javascript:> > Economics, Kingston University http://www.hpcoders.com.au > <http://www.hpcoders.com.au/> > ---------------------------------------------------------------------------- > > > > > "self reference" has been long been a subject of AI, programming language > theory (program reflection), theorem provers (higher-order logic). > > I haven't seen yet what Hod Lipson has done > > Columbia engineers create a robot that can imagine itself > January 30, 2019 / Columbia Engineering > https://engineering.columbia.edu/press-releases/lipson-self-aware-machines > > > but here is an interview with another researcher: > > > The Unavoidable Problem of Self-Improvement in AI: An Interview with Ramana > Kumar, Part 1 > March 19, 2019/by Jolene Creighton > https://futureoflife.org/2019/03/19/the-unavoidable-problem-of-self-improvement-in-ai-an-interview-with-ramana-kumar-part-1/ > > The Problem of Self-Referential Reasoning in Self-Improving AI: An Interview > with Ramana Kumar, Part 2 > March 21, 2019/by Jolene Creighton > https://futureoflife.org/2019/03/21/the-problem-of-self-referential-reasoning-in-self-improving-ai-an-interview-with-ramana-kumar-part-2/ > > > To break this down a little, in essence, theorem provers are computer > programs that assist with the development of mathematical correctness proofs. > These mathematical correctness proofs are the highest safety standard in the > field, showing that a computer system always produces the correct output (or > response) for any given input. Theorem provers create such proofs by using > the formal methods of mathematics to prove or disprove the “correctness” of > the control algorithms underlying a system. HOL theorem provers, in > particular, are a family of interactive theorem proving systems that > facilitate the construction of theories in higher-order logic. Higher-order > logic, which supports quantification over functions, sets, sets of sets, and > more, is more expressive than other logics, allowing the user to write formal > statements at a high level of abstraction. > > In retrospect, Kumar states that trying to prove a theorem about multiple > steps of self-reflection in a HOL theorem prover was a massive undertaking. > Nonetheless, he asserts that the team took several strides forward when it > comes to grappling with the self-referential problem, noting that they built > “a lot of the requisite infrastructure and got a better sense of what it > would take to prove it and what it would take to build a prototype agent > based on model polymorphism.” > > Kumar added that MIRI’s (the Machine Intelligence Research Institute’s) > Logical Inductors could also offer a satisfying version of formal > self-referential reasoning and, consequently, provide a solution to the > self-referential problem.
Proving makes sense only in a theory. How could we know that the theory is correct? That is precisely what Gödel and tarski showed to be impossible. Bruno > > > - pt > > -- > You received this message because you are subscribed to the Google Groups > "Everything List" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected] > <mailto:[email protected]>. > To post to this group, send email to [email protected] > <mailto:[email protected]>. > Visit this group at https://groups.google.com/group/everything-list > <https://groups.google.com/group/everything-list>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
