On 10 Oct 2006 at 11:23, Matt Mahoney wrote: > My argument for the unpredictability of AGI is based on Legg's paper [1]. It > proves that a Turing > machine cannot predict another machine with greater Kolmogorov complexity.
Firstly, this is for the case of a stand-alone program attempting to generate the same output as another, longer stand-alone program. For verification purposes we always have the program to be 'predicted' available as an input, and in the worst case we could always implement a virtual machine (UTM equivalent) and just emulate the operation of the larger program. This only makes a practical difference if program evaluation can have side effects beyond leaving a final 'tape' configuration in memory, which is already beyond the realm in which simple proofs about isolated Turing machines are useful. Generally though the specific outputs resulting from specific inputs aren't the main concern; we usually care about proving that certain constraints on the output hold for all possible inputs. Constraints can be modelled as boolean classifiers over program execution histories, or if you're in a nice clean theoretical model boolean classifiers over initial and final TM tape configurations. For normal software engineering these constraints are usually pretty simple and compact; working out a sufficient constraint set for FAI is much, much harder, but they will hopefully still be fairly simple compared to the FAI itself. Tractably proving that constraints will hold requires fairly sophisticated inference, either by humans or by an automated logic system. Existing compilers, verifiers and formal methods tools can only prove very basic constraints, but the scope of constraints they can handle is steadily improving with both software progress and more compute power being available. I would expect that dedicated narrow AI could do even better, and AGI better still. A critical point is that it doesn't matter if the constraint verifier errors horribly on the side of pessimism, as long as we know how to design systems that fall within the scope of structures it can handle. The history of software engineering has confirmed again and again that the local inconvenience of having to jump through hoops and make metadata explicit so that the correctness verifier can work is well worth the long term reliability and maintainability benefits. Unfortunately AI is perhaps even worse than games development as a domain where self-proclaimed genius coders wade in and start developing without even a detailed functional spec, never mind a formal software model. To be fair, existing formal software engineering tools are still pretty clunky for normal use and definitely not tailored to the needs of the AI domain. > We already cannot predict what a 30,000 line program will do. During > development, we > break it down into small modules and work on them one at a time while > modeling the > rest of the program abstractly. A critical abstraction is ignoring how a module works and focusing on what it does, where the latter is generally some causal constraint between inputs, outputs and abstracted persistent state expressible as a compact classifier. All programmers do this implicitly; the design by contract paradigm tries to make it explicit via assertions. Humans have a nasty tendency to model by intentionality when the system in question doesn't do search or really have what could sensibly be called a goal system, because we try to leverage all the dedicated wetware we have for modelling intentional systems (specifically, other animals and particularly other humans). It would take a real effort to make an AGI this broken, as reasoning by computationally nontrivial but basically static constraint is much simpler for an AI than reasoning about intent. > Any simplified, abstract model (one whose Kolmogorov complexity is less than > that > of the system modeled) must be probabilitisic, an approximation. When trying to predict exact results, yes. When trying to predict the presence or absence of specific regularities, no, because that's essentially the task of predicting the output of an extremely lossy compressor (the constraints you're interested in) running on the output of the program you want to verify. Michael Wilson Director of Research and Development Bitphase AI Ltd - http://www.bitphase.com ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/[EMAIL PROTECTED]
