Весомое доказательство: доверять ли компьютеру, если человек не в силах проверить его решения? Андрей Васильков

Весомое доказательство: доверять ли компьютеру, если человек не в силах проверить его решения?

Андрей Васильков

Опубликовано 25 февраля 2014

Мощный резонанс в СМИ вызвала недавняя работа математиков Алексея Лисицы и Бориса Конева, выполненная в Ливерпульском университете. Многие сочли её появление знаковым событием и даже усмотрели в нём признак приближающегося превосходства искусственного интеллекта над человеческим. Что же послужило причиной таких выводов?

Ещё в тридцатых годах прошлого века венгерский математик Пал Эрдёш предположил, что для любого натурального числа C в бесконечной последовательности (x_n), состоящей только из чисел «1» и «-1», существует субпоследовательность x_d, x_{2d}, ... , x_{kd} с некоторыми положительными целыми числами k и d. Такими, что |x_d + x_{2d} + ... + x_{kd}|> C.

Гипотеза получила известность под названием задачи несоответствия Эрдёша. Её доказательство стало одной из основных проблем в комбинаторной теории чисел. 

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

Алексей Лисица и Борис Конев использовали Plingeling — модификацию программы Lingeling, допускающую распределённые вычисления. Её авторы получили награды в семи номинациях на конкурсе SAT 2013. Он проводился среди разработчиков программ класса SAT-solvers, проверяющих условие выполнимости булевых формул по заданным параметрам и применяющихся для проверки математических гипотез.

_{Алексей Лисица и Борис Конев (фото: news.liv.ac.uk).}

В своей работе Лисица и Конев применяли обычный настольный компьютер с процессором Core i5-2500K (работающим на частоте 3,3 ГГц) и 16 ГБ ОЗУ. Итерационно увеличивая длину набора чисел, они установили, что для расхождения 2 можно получить последовательность длиной 1 160. При С=2 не существует последовательности длиной 1 161, удовлетворяющей условиям задачи. Иными словами, было получено частичное решение задачи несоответствия Эрдёша.

Объём сгенерированного программой файла, содержащего доказательство, составил примерно 13 ГБ. Именно это и стало поводом для сенсации. Читая о подобных достижениях, люди часто видят дилемму — принимать такие доказательства на веру или отказаться от них в силу невозможности проверить вручную.   Это проблема не науки, а нашего восприятия. Тринадцать гигабайт — действительно много для частичного доказательства, однако не удивительно само по себе. SAT-solvers и эвристические алгоритмы способны быстро выдавать решение из множества допустимых, но редко оно оказывается самым оптимальным.

Логи размером в пару гигабайт тоже никто не проверяет вручную. Для проверки утверждения, что ни одна последовательность чисел «1» и «-1» длиной 1 161 не имеет расхождения 2, использовалась программа Glucose. Она применяет совершенно другой алгоритм, работа которого требует в 27 раз больше времени при тех же машинных ресурсах.

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

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

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

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

Согласно работам Вернадского, Неймана и Винджа, само появление программ класса SAT-solvers можно рассматривать как малый предвестник технологической сингулярности — момента истории, в который технический прогресс из-за своей скорости становится недоступным пониманию человека. 

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

К оглавлению