Цифровой журнал «Компьютерра» № 214

Понятное дело, сценарий этот никогда, ни при каких условиях не будет реализован. Потребитель останется потребителем. И в роутерах будут водиться «черви», холодильники — рассылать спам, термостаты — следить за передвижениями хозяев. Вопрос, на который предстоит дать ответ: смогут ли производители как-то сгладить этот недостаток? Специалисты утверждают, что единственным практически полезным и применимым решением пока остаётся автоматическое обновление «умных» устройств, включенное по умолчанию, но с возможностью отключения. И даже так проблему полностью не устранить (в новых прошивках случаются глюки и несовместимости, старые модели быстро замещаться новыми на конвейере, но не в домах, и т. д.). Но все прочие варианты либо утопичны, либо просто смешны — вроде функции плановой перезагрузки, которую в Belkin гордо называют «самоизлечением»...

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

В статье использованы иллюстрации Matt Newman, Sean MacEntee, csiv.

К оглавлению

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

Опубликовано 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 раз больше времени при тех же машинных ресурсах.

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