Машины шутят
Созданная шутниками из Массачусетского технологического института программа случайной генерации псевдонаучных текстов SciGen и ее производная, MathGen, создающая тексты псевдоматематические, уже не раз использовались для провоцирования нечистых на руку научных журналов, готовых публиковать любою галиматью за небольшое вознаграждение. Самый известный пример в России - это, конечно, история с “Корчевателем”, эксперимент биоинформатика Михаила Гельфанда, который сгенерировал статью программой SciGen, перевел ее на русский язык при помощи автоматического переводчика (достаточно хорошего) и направил в реферируемый «Журнал научных публикаций аспирантов и докторантов». Статья, состоящая примерно из таких пассажей
"Пространство ОЗУ вставленного испытательного полигона для доказательства коллективно надежного поведения слабо насыщенных топологически шумных модальностей было утроено, а скорость оптического диска масштабируемого кластера – удвоена."
была принята к публикации, правда, предварительно “рецензент” потребовал внести в текст несколько литературных правок.
Похожие попытки отправить случайно сгенерированного троянского коня в какое-нибудь реферируемое издание предпринимались многократно и не только в России. Об одной из них, когда немец Штефан Фридль опубликовал в Journal of Algebra and Number Theory Academia, журнале далеко не первого ряда, математическую бессмыслицу, созданную программой MathGen, мы уже писали. Совсем недавно журналист издания Science умудрился опубликовать хотя и не созданную случайно, но содержащую заведомо грубые и очевидные ошибки статью сразу в 157 научных журналах открытого доступа. Обычно такие провокации проводятся, чтобы продемонстрировать алчность научных издателей и низкое качество рецензирования - большие проблемы для академического сообщества, зависимого от системы peer-review.
Машины уже не шутят
Здесь есть, однако, другая, не менее интересная сторона. Способен ли компьютер в принципе создать текст, который будет не только неотличим от написанного человеком для невнимательного рецензента или редактора, но и действительно будет иметь научную ценность или, во всяком случае, состоятельность? Полгода назад знаменитый британский математик Тимати Гаверз выложил в своем личном блоге необычный опрос. Текст содержал пять элементарных теорем (утверждения были из серии “пересечение двух открытых множеств в метрическом пространстве открыто”), к каждой из которых были предложены по три доказательства, написанных в разных формулировках. Гаверз предлагал читателям оценить, какие из доказательств понятнее и легче читаются.
Спустя некоторое время автор блога признался, что для каждой из теорем одно доказательство было написано студентом, одно - подготовленным аспирантом, а третье.. компьютером! Как ни странно, никому из принявших участие в опросе даже не пришло в голову, что какие-то из вариантов созданы нечеловеческим разумом. Гаверз предложил еще один опрос - угадать, какая из версий каждого доказателства - компьютерная (можно было ответить: “уверен, что такой-то вариант сгенерирован компьютером” и “возможно, такой-то вариант сгенерирован компьютером”). Результаты показали, что из нескольких сотен проголосовавших в среднем половина смогли правильно угадать, какой вариант - компьютерный, и только половина из них были уверены в своем выборе. Совсем неплохой результат, в довольно узком смысле означающий, что компьютерный алгоритм прошел тест Тьюринга.
Естественно, компьютер не только “записал” доказательства. Машина самостоятельно доказала эти несложные утверждения. Это - результат работы программы, которую Гаверз и его соавтор Мохан Ганесалингам (лингвист и специалист в информационных технологиях) готовили около трех лет. В препринте статьи, который был опубликован в конце сентября, авторы, описывая свое достижение, отмечают, что программы автоматических доказательств существовали и до них (об этом ниже). Прорыв в другом. Создавая “доказывающую” часть алгоритма, Гаверз с соавтором уделили очень мало внимания “записывающей” части, той, которая демонстрирует на экране окончательное доказательство. Другими словами, они даже не попытались специально придать компьютерному доказательству удобочитаемую форму. Несмотря на это - и свидетелями тому стали несколько сотен читателей блога Гаверза - машинные рассуждения оказалось сложно отличить от человеческих. “Результат работы программы не мог бы выглядеть настолько по-человечески, - утверждают авторы, - если бы она не была близким отражением мыслительной работы математика-человека”.
Машины делают черновую работу
Математическое доказательство - цепочка строгих логических рассуждений, связывающая доказываемое утверждение с доказанными ранее. В основе этих цепочек лежат аксиомы - утверждения, истинность которых принимается на веру. По большому счету, поиск или построение доказательств является основным занятием математиков. Основным, но, пожалуй, не самым важным - науку двигают вперед гипотезы - утверждения, которые обладающий сильной интуицией ученый считает доказуемыми. Без доказательств нет математики, но очень часто процесс доказательства превращается в изматывающую рутину, которую приличный исследователь с удовольствием перекладывает на аспирантов, приглашая их затем в соавторы статьи.
Но перспектива использования компьютера для доказательства математических утверждений, конечно, не ограничивается освобождением студентов и аспирантов от выполнения рутинных и достаточно тривиальных задач. Доказательство некоторых математических теорем требует перебора огромного количества вариантов и сложных вычислений, на которые у людей ушли бы даже не годы, а десятилетия. Компьютер способен справиться с ними за секунды, часы или дни.
Первой большой теоремой, доказанной при помощи машинного разума, стала теорема о четырех красках. Звучит она так: для того, чтобы раскрасить любую географическую карту, достаточно всего четырех различных красок. Естественно, имеется в виду, что граничащие регионы не могут быть одного цвета. Эта гипотеза была высказана еще в середине XIX века, но доказана была только в 1976 году. Как выяснилось, проверка утверждения сводится к раскраске примерно 2000 типов карт. Сделать это вручную за разумное время не представлялось возможным и американские математики Кеннет Аппель и Вольфганг Хакен сделали это с помощью компьютера IBM с 64 килобайтами оперативной памяти. Для проверки всех вариантов машине понадобилось примерно 1200 часов. Естественно, компьютер при этом не должен был выдавать никаких рассуждений высокого уровня. Всю “творческую” часть сделали люди, машине оставалось лишь произвести перебор. И все же без помощи искусственного помощника теорема о четырех красках (в истинности которой, в общем-то, давно никто не сомневался), скорее всего, до сих пор оставалась бы недоказанной - во всяком случае, никто и по сей день не придумал, как обойти при доказательстве сложный перебор.
С тех пор компьютеры неоднократноиспользовались при доказательствах теорем. Например, с их помощью была решена задача об упаковке шаров, известная как гипотеза Кеплера: как оптимально упаковать одинаковые твердые шарики в большой чемодан? Один из наиболее естественных вариантов упаковки - класть шарики как фрукты на рыночном прилавке, когда шар следующего слоя кладется в углубление, возникающее между тремя лежащими впритык шарами предыдущего слоя. Этот вариант действительно является наилучшим, при этом только около 26% объема чемодана окажутся заполненными воздухом. Вот только доказать эту гипотезу, высказанную знаменитым Иоганном Кеплером еще в начале XVII века, никому не удавалось до 1998 года! Пятнадцать лет назад американец Том Хейлз доказал оптимальность гранецентрированной кубической упаковки - так в математике называется укладка апельсинов на рынке, - используя при этом сложнейшие компьютерные вычисления. Опубликованная работа Хейлза представляла собой 250 страниц текста плюс 3 гигабайта компьютерного кода. Для проверки доказательства была создана специальная комиссия, которая проработала до 2004 года, пока большая часть ее членов не решила, что есть занятия и поинтереснее. Сегодня считается, что вопрос о верности гипотезы Кеплера снят на 99 процентов.
Более свежий пример - задача о единственности решения головоломки судоку. В квадрате 9 на 9 клеток нужно расставить цифры от 1 до 9 так, чтобы цифры не повторялись ни в одном столбце, строке и ни в одном из 9 блоков размера 3x3 клетки. Обычно для решения головоломки дается некоторое количество подсказок, то есть несколько цифр стоят на своих местах заранее. При этом решение головоломки с данными подсказками не обязательно единственное. Сколько нужно открыть цифр, чтобы решение наверняка было единственным? Только в прошлом году группа ирландских математиков смогла доказать, что подсказок должно быть не меньше 17. И сделано это было с помощью компьютерных вычислений. Кстати, общее число решений головоломки судоку - 6,670,903,752,021,072,936,960 - более шести с половиной секстиллионов.
Машины творят
Эти примеры объединены тем, что ученые использовали компьютер лишь в качестве инструмента, способного достаточно быстро производить громоздкие вычисления или осуществлять сложный перебор. За творческую часть отвечали живые математики. Но способен ли компьютер на самостоятельное творчество? Оказывается, да. В 1996 году американец Вильям Маккьюн представил доказательство сформулированной в 30-е годы XX века гипотезы Роббинса, выполненное автоматическим доказателем EQP. Видимо, это первый пример, когда компьютерная система смогла самостоятельно справиться с теоремой, которая оказалась слишком крепким орешком для людей.
Ясно, что компьютеры обладают базовым набором качеств, необходимых для поиска математических доказательств: они способны на логические построения, основанные на заранее заданных аксиомах, машины можно научить применять различные эвристические подходы, выбирать из набора гипотез те, что ведут в нужном направлении. Попытки построения автоматических систем, которые, как предполагалось, могли бы со временем полностью заменить людей при доказательстве математических утверждений, начались в середине прошлого века и поначалу были весьма активны. Исследования подогревал всеобщий энтузиазм по поводу искусственного интеллекта; казалось, мыслящие роботы - дело ближайшего будущего.
С самого начала в разработке автоматических доказателей боролись два противоположных подхода, человекоориентированный и машиннориентированный. Первый предполагал, что при доказательстве теоремы система должна по возможности близко повторять человеческую манеру рассуждать. Второй требовал от машины только одного: любыми способами построить логически строгую цепочку, которая соединила быаксиомы и нужное утверждение. Человекоориентированный автоматический доказатель Logic Theory Machine был создан Алленом Ньюелом и Гербертом Саймоном уже в 1956 году. Программа была способна доказывать элементарные теоремы и считается первой в истории системой искусственного интеллекта. Однако вскоре верх стал одерживать машиноориентированный подход. В 1965 году англичанин Джон Алан Робинсон предложил логический «метод резолюций», не имевший аналога в человеческих доказательных рассуждениях, но оказавшийся удивительно эффективным для компьютерных доказателей. Бум машинноориентированных систем продолжался до начала 70-х, года, когда было открыто существование так называемых NP-полных алгоритмических задач и стало понятно, что построить достаточно быстро (за полиномиальное время) работающий универсальный автоматический доказатель математических теорем в принципе невозможно.
На волне недолгого, но яркого взлета машинноориентированных систем попытки построения автоматических доказателей с псевдочеловеческой манерой рассуждения были почти полностью прекращены. Машинноориентированные автоматические доказатели, хоть и по-прежнему изредка используются в математике (доказательство гипотезы Робинсона - один из примеров), в основном применяются для решения задач информатики и промышленности. Основанные на них системы используются, например, для верификации и проверки интегральных плат и процессоров. Математикам они неинтересны: даже в тех редких случаях, когда компьютерная система способна доказать утверждение, не поддающееся человеку, живой математик не может понять ход ее рассуждений и использовать их логику и промежуточные результаты в будущих исследованиях.
Ответ корчевателя
Тимоти Гаверз и Мохан Ганесалингам утверждают, что у забытого человекоориентрированного подхода есть будущее. Построенная ими система обладает четырьмя качествами:
- удобный интерфейс ввода, не требующий формулирования утверждения в специальном формате;
- удобный формат результата, похожий на запись доказательства, какую мог бы сделать человек;
- информативность результата, то есть ясная и “человеческая” логика работы системы на каждом шаге;
- легкая расширяемость, то есть система легко может быть дополнена уже известными теоремами, методами доказательства и так далее.
Программа Гаверза и Ганесалингама умеет доказывать ряд несложных утверждений о метрических пространствах, которые пользователь может сформулировать на обычном английском языке. При этом результат работы программы - текст доказательства - выглядит таким образом, что его можно не редактируя публиковать в научном журнале. Авторы уверены, что человекоориентированный подход при автоматическом доказательстве не только более удобен для восприятия и использования, но и во многих случаях может оказаться более эффективным. Одна из главных проблем автоматических доказателей - так называемый комбинаторный взрыв: исходная задача приводит к необходимости решения нескольких других, каждая из которых раскладывается на еще несколько более простых задач и так далее, число утверждений, требующих доказательства, растет как снежный ком. Человек в такой ситуации изначально концентрируется на одном направлении и не увязает в бессмысленных второстепенных задачах. Как это происходит, мы не знаем, но чем ближе рассуждения автоматической системы будут соответствовать человеческим, тем больше шансов, что и машина приобретет своего рода человеческую интуицию.
Современные шахматные программы играют на равных с лучшими гроссмейстерами мира, естественно, в первую очередь за счет способности моментально просчитывать огромное количество позиций. Доказательство математических теорем куда больше, чем шахматы, зависит от интуиции и творческого озарения, способность к которым и отличает крупных ученых. Мы до сих пор мало знаем о природе нашего собственного сознания и не можем предсказать, возможно ли в принципе создать искусственную систему, обладающую настоящим разумом. Компьютерные вычисления при доказательстве некоторых теорем оказались необходимы, но автоматически доказатели в ближайшем будущем вряд ли смогут всерьез соперничать с математиками и тем более заменить их. Тем не менее, эксперимент Гаверза с читателями его блога показывает, что угадать нечеловеческое авторство научного текста будет все сложнее - даже если вы не редактор «Журнала научных публикаций аспирантов и докторантов» и речь в тексте идет не о корчевателе.
Радио Свобода
Созданная шутниками из Массачусетского технологического института программа случайной генерации псевдонаучных текстов SciGen и ее производная, MathGen, создающая тексты псевдоматематические, уже не раз использовались для провоцирования нечистых на руку научных журналов, готовых публиковать любою галиматью за небольшое вознаграждение. Самый известный пример в России - это, конечно, история с “Корчевателем”, эксперимент биоинформатика Михаила Гельфанда, который сгенерировал статью программой SciGen, перевел ее на русский язык при помощи автоматического переводчика (достаточно хорошего) и направил в реферируемый «Журнал научных публикаций аспирантов и докторантов». Статья, состоящая примерно из таких пассажей
"Пространство ОЗУ вставленного испытательного полигона для доказательства коллективно надежного поведения слабо насыщенных топологически шумных модальностей было утроено, а скорость оптического диска масштабируемого кластера – удвоена."
была принята к публикации, правда, предварительно “рецензент” потребовал внести в текст несколько литературных правок.
Похожие попытки отправить случайно сгенерированного троянского коня в какое-нибудь реферируемое издание предпринимались многократно и не только в России. Об одной из них, когда немец Штефан Фридль опубликовал в Journal of Algebra and Number Theory Academia, журнале далеко не первого ряда, математическую бессмыслицу, созданную программой MathGen, мы уже писали. Совсем недавно журналист издания Science умудрился опубликовать хотя и не созданную случайно, но содержащую заведомо грубые и очевидные ошибки статью сразу в 157 научных журналах открытого доступа. Обычно такие провокации проводятся, чтобы продемонстрировать алчность научных издателей и низкое качество рецензирования - большие проблемы для академического сообщества, зависимого от системы peer-review.
Машины уже не шутят
Здесь есть, однако, другая, не менее интересная сторона. Способен ли компьютер в принципе создать текст, который будет не только неотличим от написанного человеком для невнимательного рецензента или редактора, но и действительно будет иметь научную ценность или, во всяком случае, состоятельность? Полгода назад знаменитый британский математик Тимати Гаверз выложил в своем личном блоге необычный опрос. Текст содержал пять элементарных теорем (утверждения были из серии “пересечение двух открытых множеств в метрическом пространстве открыто”), к каждой из которых были предложены по три доказательства, написанных в разных формулировках. Гаверз предлагал читателям оценить, какие из доказательств понятнее и легче читаются.
Спустя некоторое время автор блога признался, что для каждой из теорем одно доказательство было написано студентом, одно - подготовленным аспирантом, а третье.. компьютером! Как ни странно, никому из принявших участие в опросе даже не пришло в голову, что какие-то из вариантов созданы нечеловеческим разумом. Гаверз предложил еще один опрос - угадать, какая из версий каждого доказателства - компьютерная (можно было ответить: “уверен, что такой-то вариант сгенерирован компьютером” и “возможно, такой-то вариант сгенерирован компьютером”). Результаты показали, что из нескольких сотен проголосовавших в среднем половина смогли правильно угадать, какой вариант - компьютерный, и только половина из них были уверены в своем выборе. Совсем неплохой результат, в довольно узком смысле означающий, что компьютерный алгоритм прошел тест Тьюринга.
Естественно, компьютер не только “записал” доказательства. Машина самостоятельно доказала эти несложные утверждения. Это - результат работы программы, которую Гаверз и его соавтор Мохан Ганесалингам (лингвист и специалист в информационных технологиях) готовили около трех лет. В препринте статьи, который был опубликован в конце сентября, авторы, описывая свое достижение, отмечают, что программы автоматических доказательств существовали и до них (об этом ниже). Прорыв в другом. Создавая “доказывающую” часть алгоритма, Гаверз с соавтором уделили очень мало внимания “записывающей” части, той, которая демонстрирует на экране окончательное доказательство. Другими словами, они даже не попытались специально придать компьютерному доказательству удобочитаемую форму. Несмотря на это - и свидетелями тому стали несколько сотен читателей блога Гаверза - машинные рассуждения оказалось сложно отличить от человеческих. “Результат работы программы не мог бы выглядеть настолько по-человечески, - утверждают авторы, - если бы она не была близким отражением мыслительной работы математика-человека”.
Машины делают черновую работу
Математическое доказательство - цепочка строгих логических рассуждений, связывающая доказываемое утверждение с доказанными ранее. В основе этих цепочек лежат аксиомы - утверждения, истинность которых принимается на веру. По большому счету, поиск или построение доказательств является основным занятием математиков. Основным, но, пожалуй, не самым важным - науку двигают вперед гипотезы - утверждения, которые обладающий сильной интуицией ученый считает доказуемыми. Без доказательств нет математики, но очень часто процесс доказательства превращается в изматывающую рутину, которую приличный исследователь с удовольствием перекладывает на аспирантов, приглашая их затем в соавторы статьи.
Но перспектива использования компьютера для доказательства математических утверждений, конечно, не ограничивается освобождением студентов и аспирантов от выполнения рутинных и достаточно тривиальных задач. Доказательство некоторых математических теорем требует перебора огромного количества вариантов и сложных вычислений, на которые у людей ушли бы даже не годы, а десятилетия. Компьютер способен справиться с ними за секунды, часы или дни.
Первой большой теоремой, доказанной при помощи машинного разума, стала теорема о четырех красках. Звучит она так: для того, чтобы раскрасить любую географическую карту, достаточно всего четырех различных красок. Естественно, имеется в виду, что граничащие регионы не могут быть одного цвета. Эта гипотеза была высказана еще в середине XIX века, но доказана была только в 1976 году. Как выяснилось, проверка утверждения сводится к раскраске примерно 2000 типов карт. Сделать это вручную за разумное время не представлялось возможным и американские математики Кеннет Аппель и Вольфганг Хакен сделали это с помощью компьютера IBM с 64 килобайтами оперативной памяти. Для проверки всех вариантов машине понадобилось примерно 1200 часов. Естественно, компьютер при этом не должен был выдавать никаких рассуждений высокого уровня. Всю “творческую” часть сделали люди, машине оставалось лишь произвести перебор. И все же без помощи искусственного помощника теорема о четырех красках (в истинности которой, в общем-то, давно никто не сомневался), скорее всего, до сих пор оставалась бы недоказанной - во всяком случае, никто и по сей день не придумал, как обойти при доказательстве сложный перебор.
С тех пор компьютеры неоднократноиспользовались при доказательствах теорем. Например, с их помощью была решена задача об упаковке шаров, известная как гипотеза Кеплера: как оптимально упаковать одинаковые твердые шарики в большой чемодан? Один из наиболее естественных вариантов упаковки - класть шарики как фрукты на рыночном прилавке, когда шар следующего слоя кладется в углубление, возникающее между тремя лежащими впритык шарами предыдущего слоя. Этот вариант действительно является наилучшим, при этом только около 26% объема чемодана окажутся заполненными воздухом. Вот только доказать эту гипотезу, высказанную знаменитым Иоганном Кеплером еще в начале XVII века, никому не удавалось до 1998 года! Пятнадцать лет назад американец Том Хейлз доказал оптимальность гранецентрированной кубической упаковки - так в математике называется укладка апельсинов на рынке, - используя при этом сложнейшие компьютерные вычисления. Опубликованная работа Хейлза представляла собой 250 страниц текста плюс 3 гигабайта компьютерного кода. Для проверки доказательства была создана специальная комиссия, которая проработала до 2004 года, пока большая часть ее членов не решила, что есть занятия и поинтереснее. Сегодня считается, что вопрос о верности гипотезы Кеплера снят на 99 процентов.
Более свежий пример - задача о единственности решения головоломки судоку. В квадрате 9 на 9 клеток нужно расставить цифры от 1 до 9 так, чтобы цифры не повторялись ни в одном столбце, строке и ни в одном из 9 блоков размера 3x3 клетки. Обычно для решения головоломки дается некоторое количество подсказок, то есть несколько цифр стоят на своих местах заранее. При этом решение головоломки с данными подсказками не обязательно единственное. Сколько нужно открыть цифр, чтобы решение наверняка было единственным? Только в прошлом году группа ирландских математиков смогла доказать, что подсказок должно быть не меньше 17. И сделано это было с помощью компьютерных вычислений. Кстати, общее число решений головоломки судоку - 6,670,903,752,021,072,936,960 - более шести с половиной секстиллионов.
Машины творят
Эти примеры объединены тем, что ученые использовали компьютер лишь в качестве инструмента, способного достаточно быстро производить громоздкие вычисления или осуществлять сложный перебор. За творческую часть отвечали живые математики. Но способен ли компьютер на самостоятельное творчество? Оказывается, да. В 1996 году американец Вильям Маккьюн представил доказательство сформулированной в 30-е годы XX века гипотезы Роббинса, выполненное автоматическим доказателем EQP. Видимо, это первый пример, когда компьютерная система смогла самостоятельно справиться с теоремой, которая оказалась слишком крепким орешком для людей.
Ясно, что компьютеры обладают базовым набором качеств, необходимых для поиска математических доказательств: они способны на логические построения, основанные на заранее заданных аксиомах, машины можно научить применять различные эвристические подходы, выбирать из набора гипотез те, что ведут в нужном направлении. Попытки построения автоматических систем, которые, как предполагалось, могли бы со временем полностью заменить людей при доказательстве математических утверждений, начались в середине прошлого века и поначалу были весьма активны. Исследования подогревал всеобщий энтузиазм по поводу искусственного интеллекта; казалось, мыслящие роботы - дело ближайшего будущего.
С самого начала в разработке автоматических доказателей боролись два противоположных подхода, человекоориентированный и машиннориентированный. Первый предполагал, что при доказательстве теоремы система должна по возможности близко повторять человеческую манеру рассуждать. Второй требовал от машины только одного: любыми способами построить логически строгую цепочку, которая соединила быаксиомы и нужное утверждение. Человекоориентированный автоматический доказатель Logic Theory Machine был создан Алленом Ньюелом и Гербертом Саймоном уже в 1956 году. Программа была способна доказывать элементарные теоремы и считается первой в истории системой искусственного интеллекта. Однако вскоре верх стал одерживать машиноориентированный подход. В 1965 году англичанин Джон Алан Робинсон предложил логический «метод резолюций», не имевший аналога в человеческих доказательных рассуждениях, но оказавшийся удивительно эффективным для компьютерных доказателей. Бум машинноориентированных систем продолжался до начала 70-х, года, когда было открыто существование так называемых NP-полных алгоритмических задач и стало понятно, что построить достаточно быстро (за полиномиальное время) работающий универсальный автоматический доказатель математических теорем в принципе невозможно.
На волне недолгого, но яркого взлета машинноориентированных систем попытки построения автоматических доказателей с псевдочеловеческой манерой рассуждения были почти полностью прекращены. Машинноориентированные автоматические доказатели, хоть и по-прежнему изредка используются в математике (доказательство гипотезы Робинсона - один из примеров), в основном применяются для решения задач информатики и промышленности. Основанные на них системы используются, например, для верификации и проверки интегральных плат и процессоров. Математикам они неинтересны: даже в тех редких случаях, когда компьютерная система способна доказать утверждение, не поддающееся человеку, живой математик не может понять ход ее рассуждений и использовать их логику и промежуточные результаты в будущих исследованиях.
Ответ корчевателя
Тимоти Гаверз и Мохан Ганесалингам утверждают, что у забытого человекоориентрированного подхода есть будущее. Построенная ими система обладает четырьмя качествами:
- удобный интерфейс ввода, не требующий формулирования утверждения в специальном формате;
- удобный формат результата, похожий на запись доказательства, какую мог бы сделать человек;
- информативность результата, то есть ясная и “человеческая” логика работы системы на каждом шаге;
- легкая расширяемость, то есть система легко может быть дополнена уже известными теоремами, методами доказательства и так далее.
Программа Гаверза и Ганесалингама умеет доказывать ряд несложных утверждений о метрических пространствах, которые пользователь может сформулировать на обычном английском языке. При этом результат работы программы - текст доказательства - выглядит таким образом, что его можно не редактируя публиковать в научном журнале. Авторы уверены, что человекоориентированный подход при автоматическом доказательстве не только более удобен для восприятия и использования, но и во многих случаях может оказаться более эффективным. Одна из главных проблем автоматических доказателей - так называемый комбинаторный взрыв: исходная задача приводит к необходимости решения нескольких других, каждая из которых раскладывается на еще несколько более простых задач и так далее, число утверждений, требующих доказательства, растет как снежный ком. Человек в такой ситуации изначально концентрируется на одном направлении и не увязает в бессмысленных второстепенных задачах. Как это происходит, мы не знаем, но чем ближе рассуждения автоматической системы будут соответствовать человеческим, тем больше шансов, что и машина приобретет своего рода человеческую интуицию.
Современные шахматные программы играют на равных с лучшими гроссмейстерами мира, естественно, в первую очередь за счет способности моментально просчитывать огромное количество позиций. Доказательство математических теорем куда больше, чем шахматы, зависит от интуиции и творческого озарения, способность к которым и отличает крупных ученых. Мы до сих пор мало знаем о природе нашего собственного сознания и не можем предсказать, возможно ли в принципе создать искусственную систему, обладающую настоящим разумом. Компьютерные вычисления при доказательстве некоторых теорем оказались необходимы, но автоматически доказатели в ближайшем будущем вряд ли смогут всерьез соперничать с математиками и тем более заменить их. Тем не менее, эксперимент Гаверза с читателями его блога показывает, что угадать нечеловеческое авторство научного текста будет все сложнее - даже если вы не редактор «Журнала научных публикаций аспирантов и докторантов» и речь в тексте идет не о корчевателе.
Радио Свобода