Порівняльний аналіз генерації смарт-контрактів Solidity за допомогою великих мовних моделей на основі формальних алгебраїчних специфікацій

Дана стаття присвячена порівняльному аналізу автоматичної генерації смартконтрактів на мові Solidity за допомогою великих мовних моделей на основі двох підходів: текстових описів природною мовою та формальних алгебраїчних специфікацій. У ході роботи було проаналізовано смарт-контракти, згенеровані великими мовними моделями (ChatGPT-4, Claude 3.7 Sonnet, DeepSeek-V3), а також інструментом на основі штучного інтелекту GitHub Copilot, з оцінкою їхньої синтаксичної коректності та відповідності початковим вимогам. Безпека смарт-контрактів оцінювалася за допомогою статичного аналізу з використанням інструменту Slither, для виявлення потенційних вразливостей, зокрема атак повторного входу та арифметичних переповнень.
Для створення формальної моделі ми використовували інсерційне моделювання, яке дозволяє формально описувати поведінку смарт-контрактів через алгебраїчні специфікації. Для покращення інтерпретації великими мовними моделями алгебраїчних специфікацій, нами було запропоновано підхід промптингу з невеликою кількістю прикладів, який передбачає надання LLM демонстраційних прикладів алгебраїчних специфікацій і відповідного коду Solidity для покращення інтерпретації формальних моделей. Запропонований підхід дозволив підвищити точність трансляції формальних специфікацій у код, зменшити кількість синтаксичних помилок та забезпечити кращу відповідність до вихідної моделі.
У ході дослідження було виявлено, що текстові запити є простішими для швидкої генерації, однак менш надійними. Через властиву їм двозначність вони частіше призводять до появи прихованих вразливостей. Натомість формальні моделі вимагають більше зусиль для налаштування великих мовних моделей та усунення помилок інтерпретації, проте дозволяють значно точніше відобразити логіку смарт-контракту, що забезпечує більш якісну генерацію контрактів зі складною поведінкою.