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

Abstract

Дана стаття присвячена порівняльному аналізу автоматичної генерації смартконтрактів на мові Solidity за допомогою великих мовних моделей на основі двох підходів: текстових описів природною мовою та формальних алгебраїчних специфікацій. У ході роботи було проаналізовано смарт-контракти, згенеровані великими мовними моделями (ChatGPT-4, Claude 3.7 Sonnet, DeepSeek-V3), а також інструментом на основі штучного інтелекту GitHub Copilot, з оцінкою їхньої синтаксичної коректності та відповідності початковим вимогам. Безпека смарт-контрактів оцінювалася за допомогою статичного аналізу з використанням інструменту Slither, для виявлення потенційних вразливостей, зокрема атак повторного входу та арифметичних переповнень. Для створення формальної моделі ми використовували інсерційне моделювання, яке дозволяє формально описувати поведінку смарт-контрактів через алгебраїчні специфікації. Для покращення інтерпретації великими мовними моделями алгебраїчних специфікацій, нами було запропоновано підхід промптингу з невеликою кількістю прикладів, який передбачає надання LLM демонстраційних прикладів алгебраїчних специфікацій і відповідного коду Solidity для покращення інтерпретації формальних моделей. Запропонований підхід дозволив підвищити точність трансляції формальних специфікацій у код, зменшити кількість синтаксичних помилок та забезпечити кращу відповідність до вихідної моделі. У ході дослідження було виявлено, що текстові запити є простішими для швидкої генерації, однак менш надійними. Через властиву їм двозначність вони частіше призводять до появи прихованих вразливостей. Натомість формальні моделі вимагають більше зусиль для налаштування великих мовних моделей та усунення помилок інтерпретації, проте дозволяють значно точніше відобразити логіку смарт-контракту, що забезпечує більш якісну генерацію контрактів зі складною поведінкою. This article presents a comparative analysis of automatic Solidity smart contract generation using large language models (LLMs) based on two approaches: natural language textual descriptions and formal algebraic specifications. The study analyzes smart contracts generated by LLMs (ChatGPT-4, Claude 3.7 Sonnet, DeepSeek-V3) as well as by the AI-based tool GitHub Copilot, evaluating their syntactic correctness, compliance with initial requirements, and security. The security of the smart contracts was assessed through static analysis using the Slither tool to identify potential vulnerabilities, including reentrancy attacks and arithmetic overflows. To create the formal specification, we applied the Insertion Modeling System (IMS), which enables formal descriptions of smart contract behavior using algebraic specifications. To improve the interpretation of these specifications by large language models, we proposed a few-shot prompting approach, which involves providing LLM with demonstration examples of algebraic specifications and the corresponding Solidity code to improve the interpretation of formal models. The proposed approach allowed us to increase the accuracy of translating formal specifications into code, reduce the number of syntax errors, and ensure better compliance with the original model. The study found that natural language prompts are easier to use for quick code generation but are less reliable, as their inherent ambiguity tends to produce hidden vulnerabilities. In contrast, formal models require additional effort to guide the LLM and eliminate interpretation errors, but they allow for a much more accurate representation of contract logic, resulting in higher-quality generation of contracts with complex behavior.