> On 18 Apr 2019, at 09:11, Philip Thrift <cloudver...@gmail.com> 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 hpc...@hpcoders.com.au <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 everything-list+unsubscr...@googlegroups.com > <mailto:everything-list+unsubscr...@googlegroups.com>. > To post to this group, send email to everything-list@googlegroups.com > <mailto:everything-list@googlegroups.com>. > 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 everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
