Доказательство математических теорем

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

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

Гипотеза четырех красок была впервые выдвинута Фрэнсисом Гутри в 1852 г. и, невзирая на применение множества оригинальных и изобретательных мат. идей, не поддавалась доказательству до тех пор, пока, наконец, спустя столетие Аппель и Хакен не пустили в ход способности И. и. Гипотеза четырех красок кратко формулируется следующим образом: «Для раскрашивания любой карты т. о., чтобы соседние страны с общей границей имели разные цвета, достаточно четырех красок».

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

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

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

Революционное применение И. и. вызвало острые споры как среди математиков, так и среди философов. Аппель и Хакен выразили свое отношение к проблемам доказательства математиком и доказательства компьютером в следующих словах:

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

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

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

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

Изменяется ли «смысл основополагающего понятия доказательства» или изменяется только субъект доказательства, — это стратегический вопрос для математиков и философов, однако интеллектуальные последствия искусственного мат. интеллекта вполне могут оказать радикальное влияние на внедрение подобных исслед. во всех дисциплинах.

Правовое обоснование

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

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

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

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