AIList-REQUEST@SRI-AI.ARPA (AIList Moderator Kenneth Laws) (10/03/85)
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 <jennings@AEROSPACE.ARPA>
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 <gideon%aiva.edinburgh.ac.uk@ucl-cs.arpa>
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
********************