Искусственный интеллект

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

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

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

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