Техника - молодёжи 1993-10, страница 32

крывает ВСЕ типы входных данных, с которыми она может столкнуться.

Разработанная Бламом процедура ПР позволяет определить, тает ти программа, в которую ввели КОНКРЕТНЫЕ исходные данные, правильный ответ ИМЕННО ДЛЯ НИХ. «Принципиальная идея в том,— говорит он,— чтобы программа УБЕДИЛА вас в правильности ответа. Что на самом деле интересует компьютерщика? Если ответ неверен, выяснить, есть ли в ней ошибка, и выловить программного «клопа». Или же он должен получить сильное, убедительное свидетельство тому, что данный конкретный ответ абсолютно гочен,— пусть даже в самой программе полно багов».

Концептуально процесс не слишком отличается от упражнений старшеклассника, проверяющего вычисленный ответ путем подстановки его в исходное уравнение. Для иллюстрации метода Блама рассмотрим следующую задачу: имеются два, по виду совершенно разных, графа; требуется определить, не являются ли они гомоморфными — то есть, в сущности, одним и тем же графом. Напомним, что гомоморфизм есть отношение между двумя совокупностями объектов, при котором каждому объекту (и виду отношения) первой совокупности соотносится один и только один объект (вид отношения) второй совокупности. В нашем случае речь идет об узлах и ребрах (отношениях между узлами) графов: один граф, скажем, представляет схему электрической цепи, второй — узор соединений, фабрикуемых в силиконовом чипе, который должен ей соответствовать. Используя стандартную программу, инженер задает такой вопрос: но является ли ДА (НЕТ), вычисленное программой, правильным ответом?

В случае, когда оба графа действительно гомоморфны, у контролера есть стандартный, хорошо известный метод подтверждения (верификации) ответа ДА. Если же получен ответ НЕТ, контролер проделывает специфический трюк, с помощью которого можно доказать, что у программы не было никаких оснований для отрицательного ответа. Делается это следующим образом. Он вводит в программу первый граф (А), а затем либо новую версию (А', А", А'"...) того же графа — где узлы переименованы случайным образом, но все соединения остаются неизменными; либо одну из полученных гем же способом версий (В\ В", В'"...) второго графа (В). Дальше начинается самое интересное!

Если программа (и все прочее) функционирует нормально, она ОБЯЗАНА лля любой пары типа (А, А¹) выдавать неизменное ДА, а для любой пары типа (А, В¹) — столь же неизменное НЕТ. Появление хотя бы одного «не того» ответа неумолимо обличает программное (возможно, и аппаратное) обеспечение. Поскольку контролер предъявляет ту или иную пару графов в случайном порядке и проделывает это несколько десятков раз, шансы программы случайно угадать ВСЕ правильные ответы (тем самым надув его) чсче-зающе малы, хотя вероятность подобного исхода теоретически существует

Методика Блама проверена на практике, но пока еще в скромных масштабах Сам Блам рассказывает об эпизоде, случившемся при работе с программой, производящей расчеты для нужд криптогра

фии. Он подключил свою схему ПП-ПР к числовому выходу — и совсем забыл об этом, пока через несколько часов не прозвучал неожиданный сигнал: «контролер» обнаружил проблему... Хотя криптографическая программа успешно справилась с огромным количеством пар 10-разрядных чисел, на одной она все же допустила ошибку! После тщательной проверки выяснилось, что автор-программист всадил-таки по невнимательности баг, проявившийся лишь в специфических обстоятельствах.

Специалисты полагают, что схема ПП-ПР довольно быстро принесет практическую выгоду: ведь с ее помощью даже от зараженных багами компьютерных систем можно получить железную гарантию правильности конкретных результатов.

Разумеется, Мануэль Блам работал не в изоляции — немалый вклад внесли специалисты по компьютерам, ТЧМ-математики, студенты и профессора университетов, в том числе уже упомянутый Ласло Бабаи и Леонид Левин (Бостонский университет). Посредством «электронной почты» полное энтузиазма сообщество непрерывно обменивалось идеями, озарениями и полученными результатами. Добровольные помощники взяли на себя несколько смежных проблем — в частности, оценку гого, насколько быстро могут быть проведены процедуры ПП-ПР (и прочие подобные) по сравнению с непосредственным выполнением компьютерных расчетов.

Столь насыщенная интеллектуальная атмосфера не могла не дать «драматических практических последствий» (по выражению Левина). Идею интерактивного доказательства вместе с логически увязанным с ней концептом проверки программы-результата подхватили и разработали Бабаи, его коллега Ланс Форгноу и Карстен Лунд (тогда еще студент Чика1ского университета). Они пришли к блестящему выводу: хотя обычный персональный компьютер не в состоянии выполнять длиннейшие, разветвленные вычисления (они под силу лишь суперкомпьютеру), он способен перескочить через это препятствие! Достаточно иметь возможность задавать вопросы двум суперкомпьютерам, работающим над одной и той же проблемой: за вполне мыслимое время ПК определит, верны ли ответы. «Сущее гвует математический способ провести допрос таким образом, что при наличии ошибки суперкомпьютеры станут противоречить друг другу,» — поясняет Бабаи.

Начала вырисовываться глубинная связь между проблемой верификации доказательства и проклятой проблемой практической невозможности получить ответы на задачи определенных типов. И вот процесс конвергенции идей завершился: все сошлось в одну точку... Тогда исследовательская группа в составе Бабаи, Левина, Форт-ноу и Шегеди предложила ГОЛОГРАФИ-ЧЕСКОЕ ПРЕДСТАВЛЕНИЕ математического доказательства (или цепочки вычислений), в котором должны проявиться (и даже усилиться) все он лбки оригинала!

Метод трансформации цепочки математических выкладок или вычислений в «прозрачную форму» уже существует: эта техника требует. чтобы «оригинал» был записан в виде серии формальных математических утверждений, которые затем специфическим образом «складываются». Ошибка даже в одном из таких утверждений проявится в большей части результирующих сумм! И вот контролер получает возможность (с помощью все гого же скромного ПК) верифицировать трансформированную калькуляцию (или доказательство) — проверив лишь относительно небольшое количество полученных сумм.

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

Что задерживает дело? Внушительная длина «прозрачного» варианта исходных выкладок... Ведь оригинал, написанный на человеческом (пусть и математическом!) языке, переводится на формализованный язык эксплицитно (явным образом) выраженных логических правил, не оставляющий никакой недоговоренности и возможности трактовать высказывание более чем одним способом «Мы пытаемся уменьшить размер подобного представления, и когда— как мы надеемся — его удастся свести к разумному уровню, появится возможность практических приложений»,— продолжает Бабаи. Специалисты по компьютерам тем временем исследуют, сколько времени понадобится на «прозрачную» трансформацию, на проверку некоторой части голограммы... и т.д. и т.п.

Что же до ожидаемых приложений... Наверное, достаточно предъявить для самостоятельных раздумий только одну мысль: если правильность цепочки выкладок проверяется по относительно небольшой ее части... то, может быть, не обязательно доводить дело до конца?

А вместо шилога обрисуем совершенно нетипичную ситуацию.

Через несколько лет (месяцев, недель, дней) навязчивых размышлений на Исаака (Айзека) Фермакса нисходит просветление (после дружеских посиделок или просто от избытка невостребованных способностей). Вскричав: «Я предположил! Меня озарило!», он бежит по нужному адресу, где излагает личное мнение: ЭТО (математическое выражение) равно ЭТОМУ (математическому выражению) при условии, что (математическое выражение)... ИКС ИГРЕК ЗЕТ!

Предполагаемый ТОЧНЫЙ ответ подставляют в исходную формулу, машина считает какое-то время (не до конца света), полученный фрагмент цепочки выкладок переводят в голограмму, проверяют — и⁹ Что же, отрицательный ответ — тоже ценная информация...

По материалам журнала «Science News»

29