Иногда ошибка в алгоритме обнаруживается быстро, иногда – только через очень длительное время. Как найти тот диапазон, в котором программа может "выйти из строя"? Команда с польскими компьютерщиками получила награду за решение этой проблемы для модели VASS.
Польско-немецко-британская команда компьютерных ученых получила награду за лучший доклад на 50-м Международном коллоквиуме по автоматам, языкам и программированию (ICALP) 2023. Конференция ICALP делится на два направления: алгоритмическое и логическое. Этот доклад относится к логическому треку. ICALP – одна из двух важнейших логических конференций в теоретической информатике.
Рекомендуем прочитать: Бизнес в Германии: Вызовы и возможности для украинских предпринимателей
Упомянутый доклад (препринт был подан на Arxiv) посвящен обнаружению ошибок в алгоритмах.
Какая польза от инновации польских разработчиков
"Наше решение объясняет, насколько хорошим может быть алгоритм для так называемой проблемы покрытия для модели VASS - как быстро он может работать, так и сколько времени ему нужно для правильной работы", – рассказывает один из авторов, доктор Филипп Мазовецкий из Варшавского университета, в интервью порталу PAP "Наука в Польше". "Если вы пишете программы, вы хотели бы автоматически проверять, может ли в результате возникнуть ошибка. В отделе компьютерных наук, которым я занимаюсь - формальной верификацией – я работаю с моделями, которые обнаруживают различные типы ошибок", – объясняет ученый.
Исследователи хотели, с одной стороны, показать, когда ошибка может произойти быстрее всего при выполнении определенного алгоритма. С другой стороны, они также хотели показать, сколько шагов необходимо сделать для того, чтобы все прошло без ошибок. То есть идея заключалась в том, чтобы выяснить, сколько шагов имеют самый короткий и самый длинный путь к ошибке.
Для воркшопа они взяли так называемую модель VASS. Какие проблемы решает этот алгоритм? Предположим, у нас есть 5 координат, каждая из которых описывает количество людей в комнате: у нас есть гостиная, ванная, кухня, коридор и спальня. Последовательными шагами разные люди входят в квартиру и перемещаются по комнатам (это называется переходами) по определенным правилам (это и есть VASS).
Например, войти в квартиру можно только через прихожую, из кухни можно попасть в гостиную, но не в спальню и тому подобное. Существует определенное количество переходов между комнатами. Проблема покрытия заключается в том, что мы хотим обнаружить переход, который соответствует правилам, но является нежелательным – это ошибка. Такой ошибкой может быть, например, когда два человека (или более) одновременно оказываются в ванной комнате (и в других комнатах тоже). Итак, началом пути, который исследователи изучали, будет человек, который первым вошел в квартиру, а концом пути – человек, который вошел в занятую ванную комнату. "Таким образом, мы рассматриваем, сколько движений должно пройти, прежде чем станет понятно, что самая быстрая ошибка может произойти. И как далеко от начала может возникнуть нежелательная ситуация" – объясняет компьютерный ученый из UW.
Это, конечно, упрощенный пример, но алгоритмы, работающие по подобным правилам, могут быть полезными, например, при распределении задач между компьютерами или процессорами. Можно представить, что может произойти ошибка, если два компьютера одновременно захотят выполнить одну задачу. Поэтому хорошо иметь возможность предвидеть, может ли такая ситуация возникнуть и когда. "И может быть огромное количество этапов, когда ошибка еще не произойдет, но она возможна все время", – говорит Филипп Мазовецкий.
Сложность алгоритма VASS
Уже в 1970-х годах сложность алгоритма VASS изучалась с точки зрения памяти, то есть, какой минимальный объем памяти компьютера нужен для решения задачи. Польско-немецкая исследовательская группа показала, какова сложность этого алгоритма с точки зрения времени.
Отвечая на вопрос о возможных применениях этой работы, Филипп Мазовецкий отмечает, что это теоретический результат. "Формальная верификация, по определению, должна давать ответы на такие вопросы, как почему что-то работает, а почему нет, где ошибки. Когда речь идет о таких вопросах, как машинное обучение – иногда слышишь, что эти алгоритмы работают, но никто не знает, почему и есть ли там ошибки. И действительно – они работают быстро, потому что они неточны.
Проблема с использованием формальных методов верификации заключается в том, что это замедляет подсчет", – говорит он. Но есть также сферы, где такая точность и безошибочность необходима. Он делает вывод, что, возможно, исследования в этой области не направлены непосредственно на решение проблем, стоящих перед человечеством, но не вся работа имеет целью это сделать. Здесь, скорее, речь идет об эстетике.
Авторами работы, получившей награду, являются Марвин Кюннеманнем (RPTU Кайзерслаутерн-Ландау, Германия), Филипп Мазовецкий (Варшавский университет, Польша), Лия Шютце (Институт программных систем Макса Планка, Германия), Генри Синклер-Бэнкс (Уорикский университет, Англия) и Кароль Венгжицкий (Саарский университет, Германия, ранее защищал докторскую диссертацию в Варшавском университете).
