Четвертый раздел искусственного интеллекта — автоматические рассуждения.
Именно они привлекают наибольшее внимание широкой публики и часто становятся главной темой научной фантастики. Тем не менее автоматическим рассуждениям как отдельной дисциплине дала начало не слишком увлекательная задача об автоматическом доказательстве математических теорем.
Часто выдвигаются новые теоремы, которые требуется доказать или опровергнуть. Доказательство теорем может быть крайне сложным. Именно это произошло с великой теоремой Ферма (согласно ей, если n — целое число, большее двух, то несуществует ненулевых натуральных чисел, удовлетворяющих равенству zn = хn + уn) — на доказательство этой теоремы ушло более 200 лет!
В 1956 году экономист Герберт Саймон (1916–2001) и инженер Аллен Ньюэлл (1927–1992) совместно разработали машину под названием Logic Theorist, способную доказывать нетривиальные теоремы математической логики. Разумеется, появление этой машины стало вехой в развитии искусственного интеллекта и вновь вызвало философскую дискуссию о возможности создания мыслящих машин. Эта дискуссия, конечно же, повлияла на литературу и кино 1960—1970-х годов, породив образы мыслящих машин, враждебных человеку. Согласно философу Памеле МакКордак, Logic Theorist доказывает: машина способна выполнять задачи, которые cчитаются творческими и подвластными исключительно человеку.
Гэрберт Саймон (слева) и Аллен Ньюэлл за игрой в шахматы, 1958 год.
В Logic Theorist использовались так называемые символьные системы, созданные математиками, чтобы придать смысл некоторым выражениям и уйти от произвольных обозначений. К примеру, мы можем утверждать: высказывание «быть человеком» означает «быть смертным», что можно записать математически как А —> В, где символ А эквивалентен высказыванию «быть человеком», символ —> — «означает», а В равносильно высказыванию «быть смертным». «Быть человеком означает быть смертным» — это произвольное высказывание, которое записывается выражением А —> В. После формализации всех произвольных членов выполнять операции с ними намного проще с точки зрения математики и информатики.
Для упрощения математических действий символьные системы опираются на аксиомы, из которых выводятся теоремы. Преимущество символьных систем в том, что они являются формальными и однозначно определенными, поэтому программировать их сравнительно просто. Рассмотрим пример:
Сократ — человек.
Все люди смертны.
Следовательно, Сократ смертен, поскольку он — человек.
Если мы запишем эти высказывания в формальном виде, они будут выглядеть так:
А: Сократ
В: человек (люди)
А —> В
С: смертен (смертны)
В —> С
Если А —> В и В —> С, то А —> С, то есть Сократ смертен.
В этом случае правило вывода под названием «гипотетический силлогизм» позволяет заключить, что А —> С истинно, если А —> В и В —> С.
Тем не менее число вариантов, полученных при автоматическом и систематическом выводе теорем на основе аксиом и правил вывода, будет опасно близко к числу атомов во Вселенной. По этой причине в машине Logic Theorist использовались эвристические рассуждения, то есть методы нечеткого прогнозирования, которые помогали выбрать лучшие производные высказывания среди возможных. Отобранные высказывания определяли правильную последовательность выводов, позволявших прийти от аксиом к доказательству теорем.
Рассмотрим практический пример. Мы хотим знать, смертен ли Сократ. Нам известны следующие исходные аксиомы:
А: Сократ
В: болельщик «Олимпиакоса
С: грек
D: человек
Е: смертен
А —> С
С —> D
A —> D
С —> Б
D —> E
Определим, истинно или ложно А —> Е, с помощью «грубой силы», то есть путем перебора всех возможных сочетаний. Имеем:
А —> С —> D —> Е
A —> С —> В
A —> D —> E
Мы выполнили семь логических операций, взяв за основу всего пять аксиом и одно правило вывода — гипотетический силлогизм. Легко догадаться, что в сценариях, содержащих больше аксиом и правил вывода, число возможных сочетаний может оказаться столь велико, что на получение доказательств уйдут годы. Чтобы решить эту проблему так, как это сделали Саймон и Ньюэлл, используем эвристическое рассуждение (или эвристику). В нашем примере эвристика подскажет: если мы хотим доказать, что некий человек смертен, нет необходимости заводить разговор о футболе (А —> С —> В).
И символьные, и эвристические системы широко используются для решения практических задач, а не только для автоматического доказательства теорем.
Приведем еще один пример использования эвристик. На каждом ходу в шахматной партии существует в среднем 37 возможных вариантов. Следовательно, если компьютерная программа будет анализировать партию на восемь ходов вперед, на каждом ходу ей придется рассмотреть 378 возможных сценариев, то есть 3512479453921 ходов — более 3,5 млрд вариантов. Если компьютер тратит на анализ каждого варианта одну микросекунду, то при анализе партии всего на восемь ходов вперед (достаточно простая задача для профессионального шахматиста) мощный компьютер будет думать над каждым ходом больше двух с половиной лет!
Для ускорения процесса нужны какие-то улучшения, которыми и будут эвристики. Эвристики — это правила прогнозирования, позволяющие исключить из рассмотрения ходы, которые ведут к очень невыгодной позиции и поэтому нецелесообразны. Уже благодаря тому, что эвристики позволяют исключить из рассмотрения несколько абсурдных ходов, число анализируемых вариантов существенно сокращается. Таким образом, эвристики — это средства прогнозирования, основанные на интуиции программиста, которые играют столь важную роль в большинстве интеллектуальных систем, что в значительной степени определяют их качество.
* * *
МАТЕМАТИЧЕСКАЯ ЛОГИКА
Математическая логика — раздел математики, занимающийся изучением схем и принципов рассуждений. Это дисциплина, в которой на основе различных правил и методов определяется корректность аргумента. Логика широко используется в философии, математике и информатике как средство проверки корректности имеющихся утверждений и вывода новых. Математическая логика была создана на основе аристотелевой логики Джорджем Булем, автором новой алгебры, которую впоследствии назвали булевой, и Огастесом де Морганом, сформулировавшим законы логики с помощью новой, более абстрактной нотации.
В последние 50 лет математическая логика пережила бурный рост, и на ее основе возникла современная логика, которую следует отличать от классической логики, или логики первого порядка. Формально логика первого порядка рассматривает только конечные выражения и правильно построенные формулы. В ней нет места бесконечным множествам и неопределенности.
Сколь бы сложными ни казались выражения, записанные на доске, в них очень редко используются символы, значение которых выходит за рамки логики первого порядка.
* * *
В последние годы непрерывно развиваются автоматические рассуждения, и теперь интеллектуальные системы способны рассуждать в условиях недостатка информации (неполноты), при наличии противоречивых исходных утверждений (в условиях неопределенности) или в случаях, когда при вводе новых знаний в систему объем совокупных знаний о среде необязательно возрастает (в условиях немонотонности).