Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Posting-Version: version B 2.10.3 4.3bsd-beta 6/6/85; site ucbvax.ARPA Path: utzoo!watmath!clyde!burl!ulysses!ucbvax!sri-ai.arpa!AIList-REQUEST From: AIList-REQUEST@SRI-AI.ARPA (AIList Moderator Kenneth Laws) Newsgroups: net.ai Subject: AIList Digest V3 #133 Message-ID: <8510040618.AA00324@UCB-VAX.ARPA> Date: Thu, 3-Oct-85 14:10:00 EDT Article-I.D.: UCB-VAX.8510040618.AA00324 Posted: Thu Oct 3 14:10:00 1985 Date-Received: Sat, 5-Oct-85 03:08:49 EDT Sender: daemon@ucbvax.ARPA Reply-To: AIList@SRI-AI Organization: University of California at Berkeley Lines: 283 AIList Digest Thursday, 3 Oct 1985 Volume 3 : Issue 133 Today's Topics: Opinion - AI Hype & System Verification ---------------------------------------------------------------------- Date: Fri, 27 Sep 85 18:52:47 PDT From: Hibbert.pa@Xerox.ARPA Subject: Re: "SDI/AI/Free and open Debate" in AIList Digest V3 #128 Date: Sun, 22 Sep 85 19:44:48 PDT From: Richard K. Jennings Subject: SDI/AI/Free and open Debate ... For those interested in the history of technology, most of the things we take for granted (microelectronics, automobiles, planes, interstate highway system) were gestated and field tested by the US Military. ... If you are willing to stay off the interstate higways, the inland waterways, airplanes and other fruits of technology ripened by close association (computers, and computer networks as has been pointed out) -- worry about the military and AI and SDI. But upon close inspection, I think it is better that the military have the technology and work the bugs out on trivial things like autonomous tanks BEFORE it is an integral part of an artificial life support system. Agreed, the military was responsible for most of the advances you cite. This doesn't do anything towards convincing me that that's the only possible way for that outcome to have come about, or even that better things wouldn't have happened in the absence of all the money going for these ostensibly military purposes. As a matter of fact, given my belief that ends NEVER justify means, I don't even agree that having those things is good. (Considering that people who didn't consent were forced to help pay for them.) P.S. Why do you think field debugging of autonomous tanks will be less costly/dangerous than of artificial life support systems? In neither case will all the bugs be found in simulations and I'd expect programmers to do better debugging in the midst of doctors practicing than in the middle of a tank battle. Chris ------------------------------ Date: Saturday, 28 September 1985 06:53:19 EDT From: Duvvuru.Sriram@cive.ri.cmu.edu Subject: AI/ES Hype : Some Discussions Gary Martin posed some interesting questions in AILIST # 126. One problem lies in the definition of Artificial Intelligence. In recent issues of AILIST some interesting points were raised as to what constitutes an Expert System. Similar discussion on AI would be useful to the AILIST readers. I understand that Gary Martin worked with the development of many "so called AI" systems and he feels that these systems did not do what they were expected to do. One must note that AI has entered the commercial market only recently and it will, probably, be a few years before we see any successes/failures. The commercialization of AI started after the Japanese initiated the fifth generation computing project. The American press also helped in this endeavor. With all the publicity given to the subject, people working in the area decided to sell their (research) products. I guess they have the right to advertise their products. I view expert system techniques as a programming philosophy. I like it and advocate its use. However, I do not claim that these techniques are AI - just that they evolved from research in AI. As a marketing strategy many tool builders use different techniques to sell their product. If people feel that the AI products are sheer crap, they can always speak up in conferences (such as the one in ES in Govt. symposium), magazines (I saw one such article in Datamation sometime ago, written by Gary Martin) - and even write to Consumer Report. Just because a few people take advantage of the situation and make tall claims does not mean that the whole field should be criticized. I have seen some recent Expert System Tools that claim to induce from examples. These systems are nothing but very good decision table evaluators. I guess the phrase "induce from examples" is used as a marketing strategy. This kind of stuff happens in all fields. It is left to the consumer to decide what to buy (I guess that there are a lot of consultants who are willing to advise you on this subject). Sriram ------------------------------ Date: Thu, 26 Sep 85 20:29:22 -0100 From: Gideon Sahar Subject: Hype, AI, et al. Recently a representative of a well known International company gave a seminar here in Edinburgh, in which we were promised the moon, earth, and virtually the whole milky way. It was claimed that with a little work, and some money, a literal pot of gold is just around the corner. Now I do not disagree with the basic premise that there is enormous promise in AI, and I realize that profits are (one) driving force behind any progress. But I do object to glowing accounts of successes in AI, which turn out (always!) to be X1/XCONN. I find hype exasparating and tiring, but in this case it is also dangerous for the continuing well-being of AI. The glowing promises are going to be proven impossible to fulfill, and the holders of the purse strings will draw them tight and plunge AI into another winter. So please, dampen down the enthusiasm, and inject some realism into your reports and salesmanship. Don't forget to mention the blood, the sweat, and the tears. Gideon Sahar (gideon%uk.ac.ed.edai@ucl-cs.arpa) Dept. of AI University of Edinburgh. ------------------------------ Date: 30-Sep-85 16:00:23-PDT From: jbn@FORD-WDL1.ARPA Subject: SIFT Verification The ``AI hype'' problem has been around for some time in the field of program verification by proof of correctness techniques. In that field, there has been little progress in the last two or three years, despite very impressive claims made in the late 1970s and early 1980s. However, we are now getting some hard evidence as to part of the cause of the trouble. I have just obtained a copy of ``Peer Review of a Formal Verification/Design Proof Methodology'', (NASA Conference Publication 2377, NASA Langley Research Center, Scientific and Technical Information Branch, 1985), which is highly critical of SRI International's work in the area. The work being evaluated is SRI's verification of the Software Implemented Fault Tolerance system, a multiprocessor system intended for use in future aircraft flight control systems. SIFT was a major effort to utilize mathematical proof of correctness technology, including automatic theorem provers, on a real problem. This was a multi-year effort, occupying most of a decade. Some quotes from the report: [p. 22] ``Scientific workers are expected to describe their accomplishments in a way that will not mislead or misinform. Members of the peer review panel felt that many publications and conference presentations of the SRI International verification work have not accurately presented the accomplishments of the project; several panel members, as a result of the peer review, felt that much of what they though had been done had indeed not been done.'' ``The research claims that the panel considered to be unjustified are primarily in two categories; the first concerns the methodology purportedly used by SRI International to validate SIFT, and the second concerns the degree to which the validation had actually been done. Many publications and conference presentations concerning SIFT appear to have misrepresented the accomplishments of the project.'' [p. 23] ``The incompleteness of the SIFT verification exercise caused concern at the peer review. Many panel members who expected (from the literature) a more extensive proof were disillusioned. It was the consensus of the panel that SRI's acomplishment claims were strongly misleading.'' This sort of thing cannot be tolerated. When someone publishes papers that make it look as if a hard problem has been cracked, but the results are not usable by others, it tends to stop other work in the field. The pure researchers avoid the field because the problems appear to be solved and someone else has already taken the credit for the solution, and the system builders avoid the field because the published results don't tell them enough to build systems. This is exactly what has happened to verification. I'm singling out SRI here because this is one of the few cases where a funding agency has called for a formal review of a research project by an outside group and the review resulted in findings as strong as the ones quoted above. Some people at SRI who have seen this note have complained that I am quoting the report out of context, so if you are really interested, you should call NASA Langley (VA) and get the entire report; it's free. NASA permitted SRI to insert a rebuttal of sorts as an appendix after the review took place (in 1983), so the 1985 report gives both the SRI position and that of the review committee. John Nagle [As moderator, I felt it my duty to ask for comments from someone at SRI who knew of this project. I thank John Nagle for acknowledging that the review committee's findings are disputed, but feel that additional points in our behind-the-scenes discussion are worth passing along. John's points about the effect of hype on AI research are important and well within the scope of AIList discussion. The current state of the art in automatic verification is also appropriate for AIList (or for Soft-Eng@MIT-XX or ARMS-D@MIT-MC). I do not know whether the merits and demerits of this particular verification project and its peer review are worthy of discussion; I am simply attempting to pass along as balanced and complete a presentation as possible. I hope that my editorial decisions do not reflect undue bias on behalf of my employer, SRI International. -- KIL] Date: Thu 26 Sep 85 15:05:12-PDT From: MELLIAR-SMITH@SRI-AI.ARPA Subject: John Nagle's AIList Request The report refered to by John Nagle (Peer Review of a Formal Verification/Design Proof Methodology, NASA Conference Publication 2377, NASA Langley Research Center, 1985) is a 50-odd page evaluation of an attempt to provide a proof for a realistic system. The project in its entirety was, and still is, beyond the capabilities of our currently available technology, and thus the proof exercise was incomplete; the proofs achieved were design level proofs, down to the level of prepost conditions, rather than proofs to the level of code. The report reviewed what was done, and not entirely negatively. The main cause for concern was that some descriptions of the work did not make sufficiently clear precisely what had been done and what the limitations of the work were. In particular, the first quotation cited by John Nagle continues: "In many cases, the misrepresentation stems from the omission of facts rather than from inclusion of falsehood." [...] A more recent, and very painstaking, peer review of SRI's work in verification, together with the corresponding work at GE Research Labs, SDC, and University of Texas, will be published by the DOD Computer Security Center next month. Michael Melliar-Smith Date: 26-Sep-85 16:35:35-PDT From: jbn@FORD-WDL1.ARPA Subject: Re: SIFT [...] Unfortunately, previous statements have contained rather strong claims. The peer review quotes from Meillar-Smith's and Richard Schwartz's ``Hierchical Specification of the SIFT Fault-tolerant Flight Control System,'' CSL-123, SRI International, March 1981: ``This paper describes the methodology employed to demonstrate rigorously that the SIFT computer meets its reliability requirements.'' And from the same authors, in ``Formal Specification and Mechanical Verification of SIFT'', IEEE Trans on Computers, C-31, #7, July, 1982: ``The formal proof, that a SIFT system in a `safe' state operates correctly despite the presence of arbitrary faults, has been completed all the way from the most abstract specification to the PASCAL program. This proof has been performed using STP, a new specification and verification system, designed and developed at SRI International. Except where explicitly indicated, every specification exhibited in this paper has been mechanically proven consistent with the requirements on SIFT and with the Pascal implementation. The proof remains to be completed that the SIFT executive performs an appropriate, safe, and timely reconfiguration in the presence of faults.'' Those are strong statements. And they just aren't true. [... you have selected two statements from reports of mine about SIFT and stated that they are not true. YOU ARE WRONG! ... -- Michael Melliar-Smith] Unless we make it clear where we are today, future work will founder. When you fail and admit it, the field moves forward; everyone learns what doesn't work and what some of the problems are. But when failure is hidden, new workers are led to make the same mistakes again. I'd like to see verification work and be used. Excessive claims have seriously damaged this field. Only recently, though, has solid information debunking these claims become available. Dissemination of the information in this report will help those in the field make progress that is real. [...] John Nagle ------------------------------ End of AIList Digest ******************** Brought to you by Super Global Mega Corp .com