`

СПЕЦИАЛЬНЫЕ
ПАРТНЕРЫ
ПРОЕКТА

Архив номеров

Как изменилось финансирование ИТ-направления в вашей организации?

Best CIO

Определение наиболее профессиональных ИТ-управленцев, лидеров и экспертов в своих отраслях

Человек года

Кто внес наибольший вклад в развитие украинского ИТ-рынка.

Продукт года

Награды «Продукт года» еженедельника «Компьютерное обозрение» за наиболее выдающиеся ИТ-товары

 

О машинном доказательстве теорем

Статья опубликована в №43 (562) от 14 ноября

0 
 

Наверное, сегодня звучит банально, что современные компьютеры могут выполнять множество сложнейших операций, доступных ранее только человеку. Кроме таких привычных действий, как распознавание образов, перевод текстов с одного языка на другой, они все больше внедряются в самые сложные сферы искусственного интеллекта – научного направления, моделирующего процесс человеческого мышления. С одним из таких направлений – автоматическом доказательстве теорем – мы и собираемся познакомить читателя.

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

Автоматическое доказательство и логическое программирование

Установление отношений логического следствия, или, что то же самое, доказательство теорем является одной из главных задач логики. Она представляет не только теоретический, но и практический интерес для многих научных и технических областей. В качестве примера назовем две достаточно широкие научно-прикладные сферы, проблемы из которых могут быть выражены в терминах доказательства теорем:

  • анализ программ. Если процесс выполнения программы описывается некоторой логической формулой А, а условие завершения – формулой В, то проверку того, что программа закончит работу, можно сформулировать как доказательство следования В из А;
  • преобразование состояний. Если заданы набор состояний и множество операторов над ними, то проблема достижения некоторого заданного состояния из исходного опять же сводится к доказательству логического следствия.

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

Хотя эти алгоритмы были предложены давно и постоянно совершенствуются, их реализация на традиционных языках программирования вызывает существенные трудности. Потребность в адекватных инструментальных средствах привела к созданию целого направления в программировании, называемого логическим, которое включает подходы и методы, приспособленные для решения задач логики, и в рамках которого созданы специализированные языки.

При решении задач на этих логических языках, как правило, описывают предметную область (называемую иногда универсумом рассмотрения), и на ней определяют функции и предикаты, выражающие взаимосвязи между исследуемыми сущностями. Логическое программирование при этом обладает особыми свойствами, отличающими его от других подходов. В функциональном программировании процедура действует как математическая функция, возвращая значение от аргументов. Логическая же процедура соответствует математическому понятию отношения и обладает большей гибкостью. При определении отношений ничего не говорит о том, какие аргументы исходные и каковы возможные результаты – в разных запросах одни и те же объекты могут играть различные роли.

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

Наличие формальных правил вывода позволяет проверять правильность доказательств, порождая с их помощью из аксиом все новые и новые следствия – до получения интересующего нас предложения. Не менее часто применяется и обратный метод: берут интересующее предложение и выясняют, из каких посылок оно может быть получено, затем анализируют эти посылки и т. д., пока не придут к аксиомам. К сожалению, в обоих случаях крайне сложно оценить необходимый объем вычислений.

Программные пакеты, выполняющие автоматические доказательства или некоторые их элементы, традиционно разделяют на интерактивные и автоматические пруверы (системы доказательств, interactive/automated theorem provers) и верификаторы моделей (model checkers). Данная классификация основана на некоторых параметрах решаемых задач и степени участия пользователя, хотя в целом такое разделение в известной степени условно.

Надо отметить, что с развитием машинных методов стал актуальным вопрос о том, что же считать доказательством в математике. Традиционно под ним понималась обозримая последовательность выводов, которую можно проверить «вручную», условно говоря, с помощью карандаша и листа бумаги. Однако участие в процессе компьютера потребовало пересмотра такого «устаревшего» представления.

Для иллюстрации сказанного приведем пример фундаментальной математической проблемы, решенной (в основном) машинными методами. Это так называемая задача о четырех красках, не поддававшаяся аналитическому решению более века. Она была сформулирована в 1852 г., когда один английский географ заметил, что для раскраски карты Британии (при которой соседние графства имели бы разный цвет) достаточно четырех красок. Математики, заинтересовавшиеся этим любопытным фактом, задались вопросом: а достаточно ли четырех красок для раскрашивания произвольной карты? Оказывается, да.

Упуская занимательную предысторию, скажем, что первое правильное доказательство этой теоремы было получено только в 1976 г. с использованием машинных методов. Между тем оно до сих пор вызывает сомнение у ряда специалистов. Дело в том, что в нем одновременно с громоздкой аналитической частью доказательства, состоящего из десятков страниц сложнейших выкладок и тысяч (!) дополнительных диаграмм, имеется машинная часть, которую удалось проверить только на компьютере (использовался суперкомпьютер Cray-1A).

Авторы доказательства логически свели задачу к исследованию 1482 базовых карт, сформированных специальным образом – их раскраска на Cray потребовала 50 суток компьютерного времени. Это-то и поставило под сомнение надежность данного метода – вероятность ошибки (как программной, так и аппаратной) при таком объеме не является пренебрежимо малой. Впрочем, доказательство 1976 г. было подтверждено позже. В 1990-х годах задача о четырех красках была сведена к раскрашиванию «всего» 633 базовых карт, что может быть реализовано на современном ПК за вполне приемлемое время – всего за несколько часов. Тем не менее поводы для скепсиса не исчезли – ведь задача опять решена машинными методами, и о проверке доказательства «вручную» можно даже не мечтать.

Coq и Gallina

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

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

Система автоматизированного построения доказательств Coq, созданная в исследовательском институте INRIA (Франция), является достаточно сбалансированным приложением, сочетающим поддержку широкого спектра логических процедур, высокую стабильность работы и относительную простоту освоения для широких кругов пользователей. Система и сопровождающая ее документация могут быть свободно загружены с узла продукта.

Разработчики определяют Coq как Proof Assistant, что в приведенной классификации соответствует интерактивным пруверам. Кроме того, Coq поддерживает процедуры полностью машинного вывода, характерные для автоматических пруверов, т. е. система обладает качествами сразу двух выделенных нами классов программ.

Coq реализован на нескольких платформах (Linux, Mac OS, Windows, Solaris) и имеет набор интерфейсов, облегчающих взаимодействие с пользователем. В ОС Windows основным средством работы с системой является стандартная командная консоль, хотя в поставку входит и графический интерфейс CoqIde.

О машинном доказательстве теорем
Интерфейс интегрированной среды разработки системы автоматизированного построения доказательств Coq

Базируется Coq на собственном языке спецификаций Gallina, состоящем из объявлений, определений и команд. Объявление ставит в соответствие некоторому имени его спецификацию, что примерно отвечает созданию переменной определенного типа в алгоритмических языках. Спецификации делятся на логические высказывания, математические коллекции и абстрактные типы. Например, спецификация nat является аксиоматическим понятием, принадлежащим математической коллекции, и означает натуральное число. Команда

Variable n:nat.

объявляет объект n как переменную натурального типа.

С помощью определений создаются и именуются новые объекты (в то время как объявления приписывают объектам только типы). Например, в арифметическом модуле Coq определен объект plus, ставящий в соответствие двум натуральным числам их сумму (очевидно, что он является прямым аналогом функционального символа «сумма» из исчисления предикатов).

Как же проводятся доказательства в Coq? Кратко поясним только схему, не вдаваясь в детали. Утверждение (в терминах Gallina называемое целью), которое должно быть доказано, записывается с помощью соответствующих операторов. Заранее, если необходимо, вводятся используемые в нем объекты – переменные, функциональные символы и др. Затем к цели применяются специальные команды, называемые тактиками, являющиеся примитивами построения доказательства. Тактика действует на текущую цель, пытаясь построить доказательство исходного предложения, возможно, на основе некоторых гипотетических суждений, добавляющихся затем к текущему списку предположений. Процесс проведения доказательства с помощью тактик предусматривает активное участие пользователя и осуществляется, как правило, за несколько шагов, число которых может быть весьма значительным. При этом от него требуются довольно глубокие знания языка спецификаций. Таким образом, Coq функционирует как интерактивный прувер. Однако в Gallina также имеются тактики, пытающиеся построить доказательство без участия человека. Для их применения достаточно введения единственной команды, а в случае успеха выдается соответствующее сообщение. В этом случае Coq действует подобно полностью автоматическим системам.

В завершение нашего знакомства с Coq укажем на такое важное качество системы, как модульность и расширяемость. Применяемые в системе понятия и тактики оформлены в виде модулей-библиотек, которые можно подключать по мере необходимости. При обычном старте в систему загружается минимальный набор библиотек, содержащий лишь логические связки и ряд арифметических понятий. Для работы в каких-то специфических предметных областях потребуются соответствующие дополнительные инструменты.

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

Завершая наш обзор, хотелось бы затронуть вопрос о сравнении интеллектуальных способностей человека и возможностей современных пакетов автоматических доказательств при проведении логических выкладок. Иными словами, способны ли сегодняшние системы доказательств конкурировать, скажем, с математиками, делающими это без применения компьютеров? При всей неоднозначности такой постановки вопроса считается, что машинные системы доказательств пока заметно отстают от профессиональных ученых, тогда как уровень среднего школьника и даже студента ими давно пройден. Для сравнения: компьютерные программы, играющие в шахматы, сегодня практически победили человека; имеется всего лишь несколько шахматистов, способных играть на равных с Fritz или Shredder, особенно с их двухпроцессорными версиями (которые обычно снабжаются приставкой Deep). При этом программы неустанно совершенствуются, так, чуть больше года назад настоящий фурор произвел шахматный движок Rybka (созданный всего одним человеком, правда, профессиональным шахматистом), возглавляющим сегодня все рейтинги. Вместе с тем имеются области, где пруверы вне конкуренции – например, в Software Engineering для проверки корректности программ или непротиворечивости требований к ПО. Поэтому хотя невозможно спрогнозировать, превзойдут ли машинные системы доказательств человека, в настоящее время они уже нашли свои ниши, и в дальнейшем сфера их применения будет только расширяться.

Не женская, не мужская, но математическая – логика

Математическая логика рассматривает языки, предназначенные для обеспечения символизма (т. е. системы формальных обозначений) для различных рассуждений. При этом речь может идти не только о точных науках, но и о самых разных областях человеческой деятельности вплоть до повседневной жизни.

Простейшая система символизма – логика высказываний, под которыми понимают любые утверждения, могущие быть либо истинными, либо ложными. Например, когда мы говорим «сегодня – пятница», то очевидно, что это либо правда, либо нет, но никак не что-то среднее. Традиционно значения, которые принимают высказывания, называют истиной или ложью и для краткости обозначают, например, буквами И и Л. Из единичных высказываний (называемых атомарными, или атомами) строят составные (формулы) – с помощью логических связок: ¬ (отрицание), ∨ (дизъюнкция), ∧ (конъюнкция), ⇒ (импликация). Как и атомы, формулы принимают значения И или Л.

Связки имеют интуитивно понятный смысл и соответствуют языковым конструкциям, используемым нами для описания различных ситуаций. Так, если А – некоторое высказывание, то ¬А означает отрицание А. Так, для приведенного выше примера отрицание звучит как «сегодня – не пятница». Аналогично, под АВ следует понимать «А или В», под АВ – «А и В», под АВ – «из А следует В».

Любая логическая формула полностью описывается своей таблицей истинности, которая каждой комбинации значений атомов (называемой интерпретацией) ставит в соответствие значение самой формулы. Так, дизъюнкция АВ будет всегда равна И, за исключением того случая, когда оба высказывания ложны. Значением АВ будет Л, кроме случая, когда А и В – истинны. Это в целом соответствует семантическим значениям языковых конструкций с учетом того, что связка «или» имеет не взаимоисключающий характер. Менее очевидна таблица истинности для импликации. В частности, если А – ложно, то АВ будет истинным независимо от значения В. На обычный язык это интерпретируется таким образом, что из ложных посылок можно сделать любые выводы.

Как в математике, так и в быту нам часто приходится решать, следует ли одно утверждение из другого. Формализацией данной ситуации является понятие логического следствия, которое вводится следующим образом. Пусть F1, F2, ..., Fn, G – логические формулы. Говорят, что G есть логическое следствие F1, F2, ..., F2, если для каждой интерпретации, где все Fi истинны, будет истинно и G. В логике доказывается, что в этом случае значением (F1 ∧ F2 ∧ ... ∧ Fn) ⇒ G всегда будет И. При этом формулы F1, F2, ..., Fn называют аксиомами (или посылками), G – заключением теоремы, а (F1F2 ∧ ... ∧ Fn) ⇒ G – теоремой. Само рассуждение, устанавливающее факт логического следствия, называют доказательством теоремы. Именно так на языке логики выглядит процесс математического доказательства, знакомый нам со школьных времен. Например, если F1: а > 0, F2: b > 0 и G: a ∙ b > 0, то очевидно, что теорема F1F2G верна, т. е. произведение двух положительных чисел также положительно.

Установление факта логического следствия является одной из главных задач математической логики и ее разделов, связанных с автоматическом доказательством теорем. На бытовом уровне эта задача сводится к тому, чтобы сделать правильный («логичный») вывод исходя из некоторого набора условий. Именно поэтому логика так же важна в повседневной жизни, как и в науке.

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

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

Первые два из них имеют достаточно очевидный смысл, а остальные, не вдаваясь в подробности, проще пояснить на примерах. Например, функциональный символ prod(x, y) ставит в соответствие переменным х и y их произведение. Термом называют любые выражения, содержащие переменные, константы и функциональные символы, а предикатом – некоторую функцию от термов, принимающую значения И или Л. Скажем, мы можем вести предикат Р(х), равный И при x > 0 и Л в ином случае. Наконец, два специальных символа – ∀ и ∃ – называются кванторами всеобщности и существования. Если G – некоторая формула, то высказывание (∀х)G принимает значение И, если G равно И для всех х из заданной предметной области, а (∃х)G истинно тогда, когда G равно И хотя бы для одного х из предметной области.

Значения предикатов от некоторых термов называют атомами, и к ним можно применять логические связки, используемые в логике высказываний. При построении и исследовании формул в исчислении предикатов необходимо учитывать, что интерпретация в общем случае должна включать предметную область (где действуют переменные), значений всех констант, функциональных символов и предикатов.

Например, упомянутая выше простейшая теорема арифметики на предметной области из действительных чисел может быть записана в виде

(∀х)(P(x)) ∧ (∀y)(P(y)) ⇒ P(prod(x, y)).

Как видим, перейдя к предикатам, нам не нужно абстрагироваться от общематематических понятий – логика первого порядка позволяет легко описать их и многие другие. Между тем и исчисления предикатов не всегда достаточно для адекватного описания многих научных и творческих задач. Попытки создания адекватных средств приводят к различным дедуктивным системам, являющимся расширениями традиционной логики. Об одной из них – нечеткой логике – слышал, пожалуй, каждый современный человек.

0 
 

Напечатать Отправить другу

Читайте также

 
 
IDC
Реклама

  •  Home  •  Рынок  •  ИТ-директор  •  CloudComputing  •  Hard  •  Soft  •  Сети  •  Безопасность  •  Наука  •  IoT