Искусственный интеллект - [136]

В качестве формальных систем математические теории не обязательно должны быть наглядными или «интуитивно истинными» - наглядность и интуитивная достоверность не являются их критериями истинности. Достаточно лишь, чтобы эти теории были бы формально правильными, свободными от внутренних противоречий. В рамках формальной аксиоматики система аксиом может быть также исследована на предмет наличия таких свойств, как независимость какой-либо аксиомы от других, полнота, категоричность, и т.д. Традиционным способом проверки истинности, формальной правильности математических доказательств является их перепроверка другими математиками, сообщество которых выступает в роли окончательных «верховных» судей. Однако математики тоже люди, и они могут ошибаться - такие случае широко известны из истории научного познания. Формализация доказательств автоматизировала вычисления и тем самым создала предпосылки для конструирования современной вычислительной техники. Создание такой техники, в свою очередь, открыла новые возможности для проверки правильности математических доказательств и их поиска компьютером. Первые попытки использовать ЭВМ для проверки и получения логико-математических доказательств были предприняты еще в 50-х гг. XX в. (программа «Логический Теоретик»), К настоящему времени эта область применения ЭВМ значительно расширилась, причем перечень проблем, решаемых только компьютером, постоянно пополняется.

Одной из таких проблем, представляющей особый интерес для эпистемологии, является доказательство математических гипотез и решение задач, относящихся к категории необозримых. В таких случаях традиционные методы вычислений и проверки полностью исключаются - никакой исследователь не в состоянии ни провести требуемые вычисления «вручную», ни шаг за шагом повторить и перепроверить весь процесс доказательств или решений. Поиск необозримых доказательств и их верификация может быть осуществлен исключительно «искусственным интеллектом», компьютером. Поскольку доказательство в формальных дедуктивных системах является эффективным, т.е. существует некоторая механическая процедура, задающая последовательность выполнения тех или иных действий (алгоритм), которая позволяет проверить, будет ли полученная последовательность формул правильно построенным выводом или нет, то задача проверки правильности формального доказательства, представленного в виде текста, оказывается алгоритмически разрешимой и может быть реализована на компьютере. Перепроверку формальных доказательств в принципе может выполнить любой компьютер, удовлетворяющий соответствующим системным требованиям и обладающий нужными вычислительными характеристиками. Таким образом, в случае формального вывода полученные результаты оказываются независимыми от конкретного типа компьютера. Более того, обнаружилось, что эти результаты также независимы и от программы, обеспечивающей получение формального вывода, и даже от языка программирования, который был использован для написания исходной программы. Сложнее дело обстоит с проверкой правильности программ.

Компьютер представляет собой физическое устройство, состоящее из электронных микросхем, материальных накопителей информации, оборудования для её ввода и вывода и т.д., которое обеспечивает его функционирование как логического устройства, позволяющего представить доказательства в виде формальных выводов в некоторой дедуктивной системе и зафиксировать эти выводы на материальных носителях информации. Работоспособность аппаратных средств, отсутствие у оборудования ошибок и сбоев в работе можно проверить с помощью соответствующих тестирующих программ, перепроверки результатов тестовых вычислений на других компьютерах и т.д. Если работоспособность компьютера как физического и логического устройств сомнений не вызывает, то для проверки правильности необозримых доказательств и решений остаётся лишь убедиться в правильности соответствующих программ. На практике правильность программы (алгоритма) выявляется на этапе её прогона и проверки с помощью специальных тестов, подбор которых во многих случаях представляет собой далеко не тривиальную задачу. Такое тестирование, по-видимому, носит сугубо теоретический характер, так как в ходе него соотносятся два теоретических продукта - программа и полученные с её помощью результаты вычислений. Однако положительные тесты все же не могут гарантировать отсутствие логических ошибок в программе и служить доказательством её правильности. Проблема сдвигается в плоскость традиционных методов, поскольку удостовериться в формальном выполнении алгоритма и тем самым доказать формальную правильность программы может только человек. Рассматривая текст программы как статический математический объект, на который распространяются аксиомы и логико-математические правила вывода, разработчик должен «вручную» воспроизвести действия, строго соответствующие имеющемуся алгоритму. Если для создания программы был использован язык с обозримым алфавитом, то доказательство правильности программы оказывается обозримой процедурой и осуществить его не представляет особого труда. Обозримая программа в принципе способна совершить необозримое число шагов, проверить и вывести сколь угодно длинные формулы. Если же текст программы