> On 18 Apr 2019, at 12:28, Philip Thrift <[email protected]> wrote: > > > > 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 >> <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 >> <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/ >> >> <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/ >> >> <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 > > <https://people.csail.mit.edu/jgross/personal-website/papers/2016-lob-icfp-2016-draft.pdf> Quite interesting. That paper explains well why we cannot use the Curry-Howard isomorphism in the mechanist context, except for the S4Grz ([]p & p), which they do not tackle, as far I have seen. I am glad to see people looking at Löb’s theorem, though. It is the main ingredient of the whole machine theology.
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.
