LLM роблять формальну верифікацію необхідною — Ethereum
Ethereum опублікувала гостьову серію дописів від провідного розробника Vyper (псевдонім big_tech_sux), у якій вказано, що розвиток LLM робить формальну верифікацію необхідною для безпеки смартконтрактів.
Ethereum у серпні 2026 року на офіційному акаунті опублікувала гостьову серію дописів від провідного розробника Vyper під псевдонімом big_tech_sux. У дописах висловлено думку, що з розвитком великих мовних моделей (LLM) формальна верифікація стає дедалі важливішою для захисту смартконтрактів.
У матеріалі пояснено, що формальна верифікація — це метод, який використовує математику для доведення коректності програми для всіх можливих варіантів виконання, а не тільки тих, що перевіряються тестами. Як ілюстрацію наведено просту функцію f(x) = x/2, для якої можна довести, що результат ніколи не перевищить вхідне значення. У дописі також зазначено: «Формальна верифікація може виявити один випадок із квадрильйона, який ніколи не проявиться під час тестування, але саме він може призвести до катастрофічного збою».
Автор описує, що раніше формальна верифікація вимагала великих команд експертів, які створювали формальні моделі коду та виконували складні доведення. За оцінкою автора, прогрес у LLM робить процес доведення більш доступним і частково автоматизованим, що може прискорити застосування методики в розробці смартконтрактів. Водночас у дописі наголошується, що перетворення програмного коду на формальну модель може містити помилки, а сам процес залишається ресурсомістким.
Матеріал також торкається впливу штучного інтелекту на безпеку: у дописі згадується випадок, коли ще не випущена модель виявила вразливості нульового дня. У тексті підкреслено різницю ролей захисників і нападників: «Тоді як нападникам достатньо знайти лише одну послідовність вхідних даних для злому системи, захисники можуть використовувати формальну верифікацію, щоб довести її стійкість до всіх можливих вхідних даних».
У дописі висловлено позицію, що для критичного програмного забезпечення, зокрема смартконтрактів, які оперують мільярдами доларів користувацьких коштів, формальна верифікація має стати обов’язковою умовою безпеки. У матеріалі також наведено посилання на попередні висловлювання співзасновника Ethereum Віталіка Бутеріна про застосування ШІ для формальної верифікації коду.
Матеріали на GNcrypto надаються виключно з інформаційною метою і не є фінансовою порадою. Ми намагаємось забезпечувати точність та актуальність даних, однак не можемо гарантувати їхню повну достовірність чи надійність. GNcrypto не несе відповідальності за можливі помилки, упущення або фінансові збитки, що можуть виникнути внаслідок використання цієї інформації. Усі дії ви здійснюєте на власний ризик. Завжди проводьте власне дослідження та звертайтесь до фахівців. Детальніше дивіться на наших сторiнках Умови, Політика конфіденційності та Дисклеймер.
Статті цього автора
