PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C

## Контекст Python является одним из самых популярных языков программирования для общего назначения, но при этом отсутствуют полноценные средства для его формального верификации. В случае языков программирования среды высокого уровня, таких как Python, формальная верификация является значительным вызовом из-за сложности языка и уровня абстракции, присущего его. Однако языки программирования среднего уровня, такие как C, поддерживают формальные методы верификации с помощью инструментов, таких как CBMC, которые позволяют проводить символьное рассуждение и уточнять место ошибки. Использование транспайлеров, таких как Cython, не дало желаемого результата в преодолении разрыва между Python и C в сфере верификации. PyVeritas предлагает решение этой проблемы, используя Large Language Models (LLMs) для транспиляции Python-кода в C, а также для достижения повышенной точности в формальной верификации и баг-локализации. ## Метод PyVeritas использует LLMs для получения высокого уровня абстракции при переводе Python-кода в C. Это позволяет сохранить информацию о структуре и логике программы в процессе транспиляции. Далее, PyVeritas применяет баунденд модельное проверяние (BMC) для генерируемого C-кода, чтобы выявлять ошибки. Максимальные модели MaxSAT используются для формальной локализации ошибок в коде. Эта методология позволяет использовать существующие инструменты верификации, разработанные для C-кода, для анализа Python-программ. Таким образом, PyVeritas упрощает процесс верификации и делает его более доступным для Python-программистов. ## Результаты Проведенные эксперименты демонстрируют, что LLM-based transpilation может достигать высокой точности в переводе Python-кода в C. Например, некоторые модели LLM показали до 80-90% точности в транспиляции. Верификационные инструменты, такие как CBMC, могут использоваться для эффективного анализа транспилированного C-кода. PyVeritas позволяет выявлять баги в Python-программах с помощью инструментов, разработанных для C-кода. Это демонстрирует мощные возможности нового фреймворка для более простого и точного верификации Python-программ. ## Значимость Предложенный подход может быть применен в различных областях, где необходима формальная верификация Python-программ, таких как централизованная библиотека или платформы для разработки программного обеспечения. PyVeritas позволяет применять существующие инструменты, разработанные для C-кода, для проверки Python-программ. Это может существенно упростить процесс верификации и повысить его точность. Кроме того, PyVeritas дает возможность интерактивного анализа ошибок, что помогает разработчикам быстро находить и исправлять баги в Python-программах. ##