Разум, машины и математика

ЗАДАЧА КОММИВОЯЖЕРА

Порой определенная задача может быть отнесена к тому или иному разделу искусственного интеллекта в зависимости оттого, с какой стороны мы подойдем к ее решению. Хорошим примером является задача коммивояжера (Travelling Salesman Problem, или TSP), которую можно решить путем поиска или планирования.

Формулировка этой задачи звучит так: для данного множества городов, дорог между ними и расстояний нужно найти маршрут коммивояжера, проходящий через все города. Коммивояжер не может заезжать в один и тот же город дважды и при этом он должен преодолеть наименьшее расстояние. Как читатель может догадаться, в зависимости от расположения маршрутов между городами коммивояжер обязательно посетит какой-либо город дважды, следовательно, это условие можно считать несущественным.

Пример графа городов, связанных между собой. Расстояние между городами в километрах указано на ребрах графа.

Автоматические рассуждения

Четвертый раздел искусственного интеллекта — автоматические рассуждения.

Именно они привлекают наибольшее внимание широкой публики и часто становятся главной темой научной фантастики. Тем не менее автоматическим рассуждениям как отдельной дисциплине дала начало не слишком увлекательная задача об автоматическом доказательстве математических теорем.

Часто выдвигаются новые теоремы, которые требуется доказать или опровергнуть. Доказательство теорем может быть крайне сложным. Именно это произошло с великой теоремой Ферма (согласно ей, если n — целое число, большее двух, то несуществует ненулевых натуральных чисел, удовлетворяющих равенству zⁿ = хⁿ + уⁿ) — на доказательство этой теоремы ушло более 200 лет!

В 1956 году экономист Герберт Саймон (1916–2001) и инженер Аллен Ньюэлл (1927–1992) совместно разработали машину под названием Logic Theorist, способную доказывать нетривиальные теоремы математической логики. Разумеется, появление этой машины стало вехой в развитии искусственного интеллекта и вновь вызвало философскую дискуссию о возможности создания мыслящих машин. Эта дискуссия, конечно же, повлияла на литературу и кино 1960—1970-х годов, породив образы мыслящих машин, враждебных человеку. Согласно философу Памеле МакКордак, Logic Theorist доказывает: машина способна выполнять задачи, которые cчитаются творческими и подвластными исключительно человеку.

Гэрберт Саймон (слева) и Аллен Ньюэлл за игрой в шахматы, 1958 год.

В Logic Theorist использовались так называемые символьные системы, созданные математиками, чтобы придать смысл некоторым выражениям и уйти от произвольных обозначений. К примеру, мы можем утверждать: высказывание «быть человеком» означает «быть смертным», что можно записать математически как А —> В, где символ А эквивалентен высказыванию «быть человеком», символ —> — «означает», а В равносильно высказыванию «быть смертным». «Быть человеком означает быть смертным» — это произвольное высказывание, которое записывается выражением А —> В. После формализации всех произвольных членов выполнять операции с ними намного проще с точки зрения математики и информатики.

Для упрощения математических действий символьные системы опираются на аксиомы, из которых выводятся теоремы. Преимущество символьных систем в том, что они являются формальными и однозначно определенными, поэтому программировать их сравнительно просто. Рассмотрим пример:

Сократ — человек.

Все люди смертны.

Следовательно, Сократ смертен, поскольку он — человек.

Если мы запишем эти высказывания в формальном виде, они будут выглядеть так:

А: Сократ

В: человек (люди)

А —> В

С: смертен (смертны)

В —> С

Если А —> В и В —> С, то А —> С, то есть Сократ смертен.

В этом случае правило вывода под названием «гипотетический силлогизм» позволяет заключить, что А —> С истинно, если А —> В и В —> С.