Agentic Specification Generator for Move Programs

## Контекст Программное обеспечение становится все более сложным, что приводит к повышению риска ошибок в разработке. Одним из решений этой проблемы является использование спецификаций — формализованных описаний, которые позволяют проверять корректность программных фрагментов. Развитие глубоких машинных узнаваний (LLM) позволило создавать инструменты автоматической генерации спецификаций. Однако, многие из этих инструментов ориентированы на основные языки программирования, такие как C, Java и Solidity. Для новых, верификационно-ориентированных языков, таких как Move, существует мало инструментов. Move — это язык, разработанный для создания безопасных и проверяемых смарт-контрактов. Однако существующие решения для генерации спецификаций для Move оставляют за собой значительные пробелы в качестве и покрытии. Таким образом, цель нашего исследования — разработать инструмент, который может автоматически генерировать высококачественные спецификации для Move, помогая разработчикам создавать более надёжные и верифицируемые смарт-контракты. ## Метод MSG (Agentic Specification Generator) — это система, основанная на глубоких машинных узнаваний, разработанная для автоматической генерации спецификаций для Move-программ. Методология MSG основывается на нескольких ключевых принципах: 1. Использование глубоких машинных узнаваний для понимания и генерации спецификаций. 2. Агентное проектирование, которое позволяет инструменту действовать самостоятельно, принимая решения на основе локальных и глобальных контекстов. 3. Модульность, которая позволяет гибко адаптировать инструмент к различным потребностям и условиям. MSG использует LLM для анализа кода Move и генерирования спецификаций. Он использует модульную архитектуру, которая позволяет ему использовать различные методы для разных стадий процесса: стадию понимания, стадию генерации и стадию верификации. Агентное проектирование позволяет MSG действовать самостоятельно, принимая решения на основе локальных и глобальных контекстов, что повышает качество спецификаций. ## Результаты Мы провели эксперименты с MSG, используя набор тестовых функций из Move. Инструмент удалось генерировать спецификации для 84% тестовых функций, что показывает его эффективность. Более того, MSG удалось идентифицировать ключевые фрагменты спецификаций, которые были пропущены экспертами. Это демонстрирует мощь LLM в понимании и генерации спецификаций для новых языков программирования. Также, выявлено, что использование модульного, агентного подхода повышает качество спецификаций, с 57% большей пропорции верифицируемых кл