[Перевод] Можно ли доверять компьютерам?

Это простое выражение на языке математического ПО Maple проверяет формулу, подсчитывающую количество целочисленных треугольников с заданным периметром.

Шалош Б. Эхад, соавтор нескольких работ, опубликованных в уважаемых математических журналах, известен своими лаконичными доказательствами теорем и тождеств, ранее требовавших многих страниц математических рассуждений. В прошлом году, когда его попросили подтвердить формулу для количества целочисленных треугольников с заданным периметром, Эхад провёл 37 вычислений менее, чем за секунду, и выдал ответ: правильно.

Шалош Б. Эхад – это компьютер. Точнее, это любой из используемых математиком Дороном Зейлбергером компьютеров – от Dell в его офисе в Нью-Джерси, до австрийского суперкомпьютера, чьё время он иногда арендует. Название, означающее на иврите «три Б один», отсылает к AT&T 3B1, первой версии Эхада.

«Душа – это софт», говорит Зейлбергер, пишущий свой код при помощи популярного математического инструмента для программирования Maple.

Дорон Зейлбергер

Усатый 62-летний профессор из Ратгерского университета, Зейлбергер находится в одном конце спектра мнений об использовании компьютеров в математике. Он указывает Эхада в качестве соавтора своих работ с конца 1980-х, «чтобы заявить, что компьютерам тоже должна доставаться заслуженная слава». Десятилетиями он сопротивляется человекоцентрическому фанатизму, присущему математикам: предпочтению доказательств, сделанных человеком на бумаге. Зейлбергер утверждает, что такие настроения завели прогресс в тупик. «И неспроста. Люди чувствуют, что потеряют работу».

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

Иначе говоря, нахождение доказательства, в котором компьютеры играют всё большую роль, не всегда является конечной целью математиков. «Многие математики считают, что создание теорий происходит с целью разобраться в математической вселенной», говорит Миньон Ким [Minhyong Kim], профессор математики из Оксфордского университета и Пхоханского университета науки и технологии в Южной Корее. Математики пытаются создать концептуальную платформу, определяющую новые объекты и выдвигающую новые гипотезы, а также доказывающую старые. Даже когда новая теория выдаёт важное доказательство, многие математики «чувствуют, что их больше интересует теория, чем доказательство», говорит Ким.

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

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

«Большую часть того, что делают люди, через 20-30 лет с лёгкостью будут делать компьютеры», говорит Зейлбергер. «Для некоторых разделов математики это уже случилось. Множество публикуемых работ, выполненных людьми, уже устарели и могут быть выполнены компьютерами. Некоторые сегодняшние задачи абсолютно неинтересны, но их делают, потому что они доступны людям».

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

«То время, когда некто мог делать настоящие математические исследования, достойные публикации, без использования компьютера, заканчивается», говорит Дэвид Бэйли [David Bailey], математик и специалист по информатике из Национальной лаборатории им. Лоуренса Бэркли, и автор нескольких книг по вычислительной математике. «А если вы этим занимаетесь, вы всё сильнее ограничиваете себя в определённых сильно специализированных областях».

Константин Телеман

Телеман изучает алгебраическую геометрию и топологии – в этих областях большинство исследователей сегодня не обходятся без компьютеров, как и в других подмножествах областей математики, связанных с алгебраическими операциями. Он концентрируется на проблемах, которые всё ещё можно решить без компьютера. «Занимаюсь ли я этой математикой потому, что не могу использовать компьютер, или же потому, что это лучшее из того, что я могу делать? Хороший вопрос». Несколько раз за свою 20-летнюю карьеру Телеман хотел бы, чтобы он умел программировать и смог подсчитать решение задачи. И каждый раз он решал потратить три месяца, которые, по его мнению, требуются для изучения программирования, на ручное решение. Иногда, по его словам, он «не касается подобных вопросов или даёт их студенту, умеющему программировать».

Если сегодня заниматься математикой без компьютера всё равно, что «бежать марафон без обуви», как обозначила это Сара Биллей [Sara Billey] из Вашингтонского университета, математическое сообщество разделилось на две толпы бегущих.

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

Что ещё хуже, по мнению исследователей, так это отсутствие чётких правил использования компьютеров в математике. «Всё больше математиков учатся программировать; но стандарты проверки программы и установления факта её правильной работы – ну, их нет», говорит Джереми Авигад, философ и математик в университете Карнеги-Меллон.

В декабре Авигад, Бэйли, Билей и десятки других исследователей встретились в Институте вычислительных и экспериментальных исследований в математике, чтобы обсудить стандарты надёжности и воспроизводимости результатов. Из множества проблем возник один общий вопрос: в поисках финальной истины насколько мы можем доверять компьютерам?

Компьютеризированная математика

Математики используют компьютеры по-разному. Один из способов: доказательство измором. Доказательство описывается так, что утверждение верно, если оно выдерживает большое, но конечное количество проверок. Затем пишется программа, проверяющая все эти случаи.

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

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

Всё чаще компьютеры не только помогают искать гипотезы, но и доказывать их. Платформы для доказательства теорем, такие, как Z3 от Microsoft, могут проверять определённые типы утверждений, или быстро находить опровергающий их контрпример. Такие алгоритмы, как метод Уилфа-Цейльбергера (изобретённый Дороном Цейльбергером и Гербертом Уилфом в 1990) может проводить символьные вычисления, работать с переменными вместо чисел и выдавать точные результаты без ошибок округления.

С имеющимися сегодня вычислительными мощностями такие алгоритмы решают задачи, ответы которых выглядят как алгебраические выражения с десятками тысяч членов. «А затем компьютер упрощает это выражение до 5-10 членов,- говорит Бэйли. – Человек не только не смог бы этого сделать, он не смог бы сделать это без ошибок».

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

Телеман вспоминает, что в 1990-х специалисты по теоретической физике предсказали наличие «красивого ответа» на вопрос о поверхностях высшего порядка, относящихся к теории струн. Когда математики написали компьютерную программу для проверки гипотезы, они обнаружили, что она неверна. «Но программисты ошиблись, а физики действительно были правы,- говорит Телеман. – Это самая большая опасность использования компьютерных доказательств: что, если в них есть ошибка?».

Этот вопрос занимает Джона Хэнке [Jon Hanke]. Специалист по теории чисел и опытный программист, Хэнке считает, что математики привыкли чрезмерно доверять инструментам, которые ещё недавно не одобряли. Он считает, что ПО нельзя доверять, и нужно постоянно проверять. Но большую часть софта, используемого математиками, проверить нельзя. У самых популярных инструментов для математического программирования, Mathematica, Maple и Magma, стоящих по $1000 за профессиональную лицензию, код закрыт. И пользователи уже сталкивались с ошибками в каждом из них.

«Когда Magma выдаёт мне ответ 3,765, откуда я знаю, что он правильный? – задаётся вопросом Хэнке. – Я не знаю. Мне приходится ей доверять». Если математики хотят поддерживать давнюю традицию, по которой можно проверить каждый этап доказательства, то, по мнению Хэнке, они не могут использовать ПО с закрытым кодом.

Есть бесплатная альтернатива с открытым кодом, Sage, но в большинстве случаев она проигрывает по мощности. Она могла бы догнать конкурентов, если бы над её разработкой трудилось больше математиков, как над Википедией, говорит Хэнке – но академических побуждений к этому практически нет. «Я написал кучу ПО для квадратичных форм на C++ и Sage, и использовал их для доказательства теоремы», говорит Хэнке. «И вся эта работа над открытым кодом не получила признания». После закрытия возможности работы на постоянной должности в штате Университета Джорджии в 2011 году, Хэнке ушёл из науки в финансы.

Хотя многие математики осознают необходимость срочного появления новых стандартов, одну проблему они решить не смогут. Проверка чужого кода занимает время, и люди могут не захотеть этим заниматься. «Это как искать ошибку в коде, выполняющемся на твоём iPad,- говорит Телеман. – Кто её будет искать? Сколько пользователей iPad занимаются исследованием кода?»

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

Доказательство доказательства

В 1998 Томас Хэйлс [Thomas Hales] удивил мир, использовав компьютер для решения 400-летней гипотезы Кеплера. Она утверждает, что наиболее плотным методом упаковки шаров является метод хранения, используемый для апельсинов – упаковка под названием гранецентрированная кубическая упаковка. Она известна всем уличным торговцам, но ни один математик не мог этого доказать. Хэйлс решил задачу, обозначив сферы как вершины графа, и соединив их рёбрами. Он уменьшил бесконечное количество возможностей до списка из нескольких тысяч наиболее плотных графов и провёл «доказательство измором». «Затем мы использовали линейное программирование, чтобы показать, что ни одна из возможностей не была контрпримером», говорит Хэйлс, математик в Питтсбургском университете. Иначе говоря, ни один из графов не оказался более плотным, чем граф, соответствовавший упаковке апельсинов в ящике. Доказательство состоит из 300 страниц текста и 50000 строк кода.

Хэйлс отправил доказательство в Annals of Mathematics, самый престижный журнал, в результате чего через четыре года рецензенты сообщили, что не смогли подтвердить правильность его кода. В 2005 году журнал опубликовал сокращённую версию доказательства на основе уверенности в правильности письменной части доказательства.

Согласно Петеру Сарнаку, математику из Института передовых исследований, до января работавшего редактором Annals of Mathematics, проблемы, вскрытые доказательством Хэйлса, неоднократно появлялись за последние 10 лет. Зная, что в будущем доказательства с помощью компьютера будут появляться всё чаще, совет редакторов решил прислушиваться к таким доказательствам. «Однако в тех случаях, когда код очень сложно проверить в одиночку, мы не будем делать заявлений о его правильности,- писал Сарнак. – Мы надеемся, что в случае достаточно важных результатов другие люди напишут сходный, но независимый код, и проверят сделанные утверждения».

По мнению коллег Хэйлса, его ответ на дилемму рецензентов может изменить будущее математики. «Том – удивительный человек. Он ничего не боится,- говорит Авигад. – Узнав, что у людей возникли сомнения по поводу его доказательства, он сказал, ‘ОК, следующая задача – создать формально проверенную версию доказательства’. У него не было никакого опыта в этой сфере, и он начал общаться со специалистами по информатике и учиться тому, как это делается. И сейчас этому проекту до завершения осталось несколько месяцев».

Чтобы показать безупречность доказательства, Хэйлс считает необходимым воссоздать его с использованием основных элементов математики – логики и аксиом. Такие очевидные вещи, как х = х, служат набором правил для математиков, так же, как грамматика управляет языком. Хэйлс вознамерился использовать технику под названием «подтверждение формального доказательства», в которой компьютерная программа использует логику и аксиомы для оценки каждого шага доказательства. Процесс может быть медленным и кропотливым, но в качестве награды вы получаете уверенность. Компьютер «ничего вам не прощает», говорит Авигад, формально проверивший теорему о простых числах в 2004. «Он следит за всем, что вы делаете. Он напоминает вам, что есть ещё какой-то случай, который нужно учесть».

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

Альтернативная логика

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

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

Некоторые исследователи считают это единственным решением проблемы усложнения математики.

«Подтверждение работы сравнялось по сложности с написанием работы,- говорит Воеводский. – За написание вы получаете награду – например, повышение – но никто не получает наград за проверку чужой работы. Так что мы мечтаем, что работа будет поступать в журнал вместе с файлом, написанным на этом формальном языке, и рецензенты просто будут проверять утверждение теоремы и его ценность для читателей».

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

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

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

Даже самый пылкий фанат компьютеров среди математиков признаёт наличие трагедии в том, чтобы сдаться превосходящей логике Шалоша Б. Эхада, и принять роль поддерживающего звена в поисках математической истины. Это же всего лишь люди. «Я получаю удовлетворение от того, что понимаю в доказательстве всё от начала до конца,- говорит Зейлбергер. – С другой стороны, это жизнь. А жизнь – сложная штука».