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

Тем не менее число вариантов, полученных при автоматическом и систематическом выводе теорем на основе аксиом и правил вывода, будет опасно близко к числу атомов во Вселенной. По этой причине в машине Logic Theorist использовались эвристические рассуждения, то есть методы нечеткого прогнозирования, которые помогали выбрать лучшие производные высказывания среди возможных. Отобранные высказывания определяли правильную последовательность выводов, позволявших прийти от аксиом к доказательству теорем.

Рассмотрим практический пример. Мы хотим знать, смертен ли Сократ. Нам известны следующие исходные аксиомы:

А: Сократ

В: болельщик «Олимпиакоса

С: грек

D: человек

Е: смертен

А —> С

С —> D

A —> D

С —> Б

D —> E

Определим, истинно или ложно А —> Е, с помощью «грубой силы», то есть путем перебора всех возможных сочетаний. Имеем:

А —> С —> D —> Е

A —> С —> В

A —> D —> E

Мы выполнили семь логических операций, взяв за основу всего пять аксиом и одно правило вывода — гипотетический силлогизм. Легко догадаться, что в сценариях, содержащих больше аксиом и правил вывода, число возможных сочетаний может оказаться столь велико, что на получение доказательств уйдут годы. Чтобы решить эту проблему так, как это сделали Саймон и Ньюэлл, используем эвристическое рассуждение (или эвристику). В нашем примере эвристика подскажет: если мы хотим доказать, что некий человек смертен, нет необходимости заводить разговор о футболе (А —> С —> В).

И символьные, и эвристические системы широко используются для решения практических задач, а не только для автоматического доказательства теорем.

Приведем еще один пример использования эвристик. На каждом ходу в шахматной партии существует в среднем 37 возможных вариантов. Следовательно, если компьютерная программа будет анализировать партию на восемь ходов вперед, на каждом ходу ей придется рассмотреть 37⁸ возможных сценариев, то есть 3512479453921 ходов — более 3,5 млрд вариантов. Если компьютер тратит на анализ каждого варианта одну микросекунду, то при анализе партии всего на восемь ходов вперед (достаточно простая задача для профессионального шахматиста) мощный компьютер будет думать над каждым ходом больше двух с половиной лет!

Для ускорения процесса нужны какие-то улучшения, которыми и будут эвристики. Эвристики — это правила прогнозирования, позволяющие исключить из рассмотрения ходы, которые ведут к очень невыгодной позиции и поэтому нецелесообразны. Уже благодаря тому, что эвристики позволяют исключить из рассмотрения несколько абсурдных ходов, число анализируемых вариантов существенно сокращается. Таким образом, эвристики — это средства прогнозирования, основанные на интуиции программиста, которые играют столь важную роль в большинстве интеллектуальных систем, что в значительной степени определяют их качество.

* * *

МАТЕМАТИЧЕСКАЯ ЛОГИКА

Математическая логика — раздел математики, занимающийся изучением схем и принципов рассуждений. Это дисциплина, в которой на основе различных правил и методов определяется корректность аргумента. Логика широко используется в философии, математике и информатике как средство проверки корректности имеющихся утверждений и вывода новых. Математическая логика была создана на основе аристотелевой логики Джорджем Булем, автором новой алгебры, которую впоследствии назвали булевой, и Огастесом де Морганом, сформулировавшим законы логики с помощью новой, более абстрактной нотации.

В последние 50 лет математическая логика пережила бурный рост, и на ее основе возникла современная логика, которую следует отличать от классической логики, или логики первого порядка. Формально логика первого порядка рассматривает только конечные выражения и правильно построенные формулы. В ней нет места бесконечным множествам и неопределенности.

Сколь бы сложными ни казались выражения, записанные на доске, в них очень редко используются символы, значение которых выходит за рамки логики первого порядка.

* * *