Великі мовні моделі (LLM) стрімко змінюють те, як пишуть код: дедалі більше розробників делегують генерацію фрагментів програм ШІ-асистентам. У розмові на каналі The Pragmatic Engineer автор книжки Designing Data-Intensive Applications Мартін Клеппманн пояснює, чому така зміна підходу робить формальні методи й автоматичну перевірку коректності коду не просто бажаними, а необхідними.
«Vibe coding»: коли код пише ШІ
Поширення LLM призводить до явища, яке Клеппманн називає «vibe coding»: розробник описує бажану поведінку системи, а модель генерує код, що «відчувається» правильним за стилем і структурою.
Такий підхід різко збільшує обсяг коду, який з’являється без детального ручного проєктування. Це зручно, але створює нову проблему: якщо кожен згенерований фрагмент доведеться ретельно перевіряти людині, саме рев’ю стане вузьким місцем у процесі розробки.
Людський код-рев’ю більше не масштабується
Традиційно якість програмного забезпечення забезпечували через:
- код-рев’ю колегами;
- тестування (юнiт-, інтеграційні, end-to-end тести);
- статичний аналіз.
У світі, де LLM можуть генерувати величезні обсяги коду за лічені хвилини, покладатися лише на людське рев’ю стає нереалістично. Якщо кожен рядок, створений ШІ, має пройти через розробника, виграш від автоматизації просто зникає.
Отже, щоб справді отримати переваги від використання LLM, потрібні інструменти, які автоматично й надійно перевіряють коректність згенерованих програм.
Безпека як головний аргумент
Проблема особливо гостра в контексті безпеки. Достатньо однієї дрібної помилки, щоб:
- відкрити вразливість;
- скомпрометувати всю систему;
- зруйнувати її модель загроз.
У безпекових компонентах — криптографії, автентифікації, контролі доступу — навіть незначний баг може мати непропорційно великі наслідки. Якщо такі частини коду генерує LLM, а перевірка обмежується поверхневим переглядом, ризики різко зростають.
Тому автоматизовані, формально обґрунтовані методи перевірки стають критично важливими: вони дозволяють не просто «довіряти» коду, а мати формальний доказ його коректності щодо заданих властивостей.
Формальні методи: від нішевого інструмента до масового
Формальна верифікація — це підхід, коли властивості програми (наприклад, відсутність певного класу помилок) доводяться математично. Історично такі методи вважалися:
- занадто складними для більшості команд;
- надто дорогими з погляду часу й ресурсів;
- придатними лише для вузьких доменів (авіація, космос, критичні системи).
Клеппманн висловлює надію, що LLM змінять цю ситуацію. Якщо моделі навчаться:
- допомагати формулювати специфікації;
- генерувати формальні моделі;
- асистувати у створенні доказів,
то вхідний бар’єр для формальної верифікації може суттєво знизитися. Те, що раніше вимагало глибокої спеціалізованої підготовки, стане доступнішим для ширшого кола інженерів.
У підсумку поєднання LLM та формальних методів може виглядати так:
- LLM генерує код і допомагає описати очікувану поведінку;
- формальні інструменти автоматично перевіряють, чи відповідає код цим вимогам;
- розробник фокусується не на ручному пошуку багів, а на постановці правильних специфікацій.
Це не скасовує потреби в людському контролі, але зміщує акцент з перевірки кожного рядка на перевірку властивостей системи загалом.
Джерело
Martin Kleppmann: Vibe coding → more demand for formal methods — The Pragmatic Engineer