On Thursday, April 18, 2019 at 4:33:48 AM UTC-5, Bruno Marchal wrote: > > > On 18 Apr 2019, at 09:11, Philip Thrift <[email protected] <javascript:>> > 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] >> Economics, Kingston University 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 > > I think Lumar is just part of the "Gödel-Löb logic hacker" gang (MIT, MIRI). They want working code, not "correctness".
cf. Löb’s Theorem A functional pearl of dependently typed quining https://people.csail.mit.edu/jgross/personal-website/papers/2016-lob-icfp-2016-draft.pdf - 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]. 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.
