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