Cтраница 2
Искусственный интеллект ( ИИ) как наука существует около полувека. Первой интеллектуальной системой считается программа Логик-Теоретик, предназначенная для доказательства теорем и исчисления высказываний. Ее работа впервые была продемонстрирована 9 августа 1956 г. В создании программы участвовали такие известные ученые, как А. Саймон и др. За прошедшее с тех пор время в области ИИ разработано великое множество компьютерных систем, которые принято называть интеллектуальными. Области их применения охватывают практически все сферы человеческой деятельности, связанные с обработкой информации. [16]
К числу других таких программ относятся Логик-теоретик [117, 118] и программа игры в шахматы [119], однако здесь мы на них подробно не будем останавливаться. [17]
Одна из эволюционных моделей искусственного интеллекта основана на оценке поисковых процедур рассмотренных нами программ. Первые программы, такие, как Логик-теоретик, GPS, символический интегратор Слэйджла, система для доказательства геометрических теорем, часто при получении решения прибегали к длительному поиску. Более поздние программы ( например, программа для решения содержательно заданных алгебраических задач Боброу, программа установления геометрического подобия Эванса, визуальная программа Газ-мана) значительно менее терпеливы и получают решение, обходясь без чересчур длительного поиска. Некоторые программы побочной линии ( например, программа символического интегрирования Мозеса) также отличаются небольшим объемом поиска. [18]
Как ранние эвристические программы согласуются с этими определениями. Если мы в качестве примера рассмотрим программу Логик-теоретик [117], станет ясно, что она удовлетворяет последним трем условиям почти так же, как и алгоритм. [19]
Именно в этом кроются дополнительные возможности геометрической машины в поиске доказательства теорем, необходимые для такой сложной формальной системы. Они не были нужны, а потому и не искались в машине Логик-теоретик Ньюэлла, Шоу и Саймона ( см. Пойа [870]), предназначенной для исчисления высказываний. [20]
Одна из первых работ в области эвристического программирования была посвящена разработке программы Логик-теоретик для доказательства математических теорем. В программе логик-теоретик практически реализована возможность автоматизированного доказательства математических теорем символической логики, а именно, теорем по исчислению высказываний. Программа Логик-теоретик на основании правил вывода позволяет получать новые теоремы из исходных аксиом и других теорем. [21]
Одна из первых работ в области эвристического программирования была посвящена разработке программы Логик-теоретик для доказательства - математических теорем. В программе Логик-теоретик практически реализована возможность автоматизированного доказательства математических теорем символической логики, а именно - теорем по исчислению высказываний. Программа Логик-теоретик на основании правил вывода позволяет получать новые теоремы из исходных аксиом и других теорем. В доказательстве используют три правила вывода: подстановку, замену, отделение, а в качестве аксиом - пять истинных высказываний. Построение доказательства начинают от конечного результата по направлению к исходным посылкам. Эта направленность доказательства и вопросы иерархического наследования в доказательстве теорем имеют ряд общих черт с процедурой синтеза структуры ХТС. На каждом этапе из заданного списка аксиом или ранее доказанных теорем выбирается такая, из которой с помощью правил вывода может быть выведена теорема данного этапа. Поэтапная процедура доказательства продолжается до тех пор, пока в списке для вывода не окажутся исходные посылки. В этом случае задача считается решенной. Необходимо, однако, отметить, что в ряде случаев поиск метода доказательства теоремы может оказаться безуспешным. [22]
В то время как Логик-теоретик показал, что программы могут решать задачи из символической логики, иные программы пытались решать задачи в других областях математики, в играх и даже в производственных ситуациях. Среди этих новых программ особенно следует отметить систему, развитую Гелернтером [45] и его коллегами, которая фактически использует некое внутреннее представление чисел и графических построений для решения геометрических задач. [23]
Ван Хао [1133, 1134] критиковал проект ЛТ на том основании, что, как было показано им и другими, существуют машинные методы доказательства, требующие для того же круга задач значительно меньших усилий, чем ЛТ, и имеющих то преимущество, что они в конце концов позволяют найти доказательство любого доказуемого предложения. Программа ЛТ не располагает процедурой решения столь исчерпывающего характера и может оказаться несостоятельной при доказательстве некоторых теорем. Авторы работы Эмпирические исследования машины Логик-теоретик, вероятно, неосведомленные о существовании скромных по эффективности исчерпывающих методов, подкрепляют свои аргументы сравнением с одним особенно неэффективным исчерпывающим процессом. И все же я чувствую, что некоторые из выпадов Ван Хао несправедливы. Его критика направлена не по адресу. Он, по-видимому, не понял, что авторов ЛТ интересует не столько доказательство этих теорем, сколько общая проблема решения сложных задач. [24]
Характерное для этой работы Ньюэлла, Шоу и Саймона внимание к методам, используемым человеком при решении задач, лежит в основе всех совместных исследований этих авторов. В этой связи интересно указать на работы ( 1005 ] и [1008], в которых, хотя они написаны свыше ЛО лет назад, уже в значительной степени содержится основная схема механизма принятия решений. Эта схема была затем воплощена в программах Шахматист и Логик-теоретик, а также в программе Кларксона, выбирающей портфель ценных бумаг ( см. стр. [25]
Мы исследовали некоторые проблемы упрощения и аппроксимации, подлежащие разрешению, и показали, как эти проблемы разрешаются в одной из сложноорганизованных программ для решения задач. Тем, кто хочет подробнее познакомиться с устройством таких систем обработки информации и уже имеет некоторое представление о языке ИПЛ-V, весьма рекомендуется обратиться к превосходной работе Стеф-ферада [163], в которой дан анализ программы Ньюэл-ла, Шоу и Саймона Логик-теоретик. В следующей главе мы сравним систему GPS с другой системой обработки информации, причем уделим особое внимание лежащим в ее основе психологическим допущениям и вопросам ее структуры. [26]
Проблема обучения представляет интерес не только для психологов, изучающих мышление человека, но и для исследователей в области искусственного интеллекта, стремящихся повысить эффективность программ для вычислительных машин. Читателя, интересующегося этим кругом вопросов, мы отсылаем к статье Минского ( стр. Ньюэлла, Шоу и Саймона о программе Логик-теоретик ( стр. Фейгенбаум и Саймон [320] обсуждают возможные - применения описанной в данном разделе модели вербального обучения к проблеме искусственного разума. [27]
Известно, что только небольшую часть своих знаний человек может точно сформулировать вербальным или формальным способом. Обширная область интуитивных знаний специалистов, которые необходимы для успешной работы интеллектуальных систем, остается недоступной из-за отсутствия средств их извлечения и представления. Нисходящий метод соответствует дедуктивному подходу, в рамках которого на этапе становления искусственного интеллекта разрабатывались программы, способные решать сложные задачи на основе логической обработки содержащихся в них знаний. Примерами таких программ являются знаменитый Логик-Теоретик и GPS - универсальный решатель задач. [28]
Интерес Маккарти к алгебраической обработке списков и к исследованию искусственного интеллекта побудил его принять участие в 1956 г. в летней школе по искусственному интеллекту в Дартмуте ( США), которая считается первой организованной встречей по исследованиям в этой области. Саймон представили разработанный ими язык IPL ( Newell Алан Ньюэлл. Он был предназначен для программы искусственного интеллекта Логик-теоретик вывода теорем логики. [29]
Уместно еще раз подчеркнуть тот факт, что объектом наших исследований была не конструкция машины, способной доказывать теоремы из эвклидовой геометрии на плоскости или, того более, теоремы в некоторой неразрешимой системе, например в теории чисел. Машины для доказательства теорем, как таковые, являются предметом исследования математиков и логиков. Важная работа в этом направлении сделана Ван Хао и Гилмором в исследовательском центре IBM. Ван Хао написал для машины IBM-704 программу, которая может доказать все теоремы исчисления высказываний, сформулированные Расселом и Уайтхедом в их Principia Mathematica, тогда как Логик-теоретик мог справиться только с 38 из 52 теорем гл. Кроме того, Логику-теоретику потребовалось для доказательства намного больше времени, чем программе Ван Хао. [30]