Boosting Skeleton-Driven SMT Solver Fuzzing by Leveraging LLM to Produce Formula Generators

#### Контекст Satisfiability Modulo Theory (SMT) solvers являются ключевыми инструментами в области исследований по системам и программированию. Они лежат в основе таких задач, как символьное выполнение и автоматическая проверка. Их достоверность и качество тестовых формул, используемых для выявления ошибок, играют ключевую роль в обеспечении надежности этих систем. Однако современные SMT-решатели постоянно развиваются, что сильно усложняет создание качественных тестов. Ранее разработанные методы показали эффективность на более старых версиях систем, но не могут справиться с новыми функциями, добавляемыми в развивающиеся решатели. Данное исследование ориентировано на решение этой проблемы с помощью нового подхода, использующего Large Language Models (LLM) для генерации тестовых формул. #### Метод Предлагаемый подход, Chimera, представляет собой новую LLM-ориентированную стратегию для fuzzing SMT-решателей. Он отличается двумя основными инновациями. Во-первых, Chimera автоматически извлекает контекст-фри грамматики (CFG) из документации для SMT-теорий, включая расширения, специфичные для каждого способа. Во-вторых, Chimera использует генераторы логических выражений, генерируемые LLMs, для создания термов (логических выражений), которые соответствуют этим грамматикам. Эти термы последуют размещаться в уже существующие структурные шаблоны формул, чтобы обеспечить их синтаксическую корректность и нормативность. Этот подход снижает количество ложных срабатываний и позволяет держать высокую скорость генерации формул. Заметно, что Chimera использует LLMs только один раз в начале, чтобы сгенерировать грамматики, чтобы уменьшить накладные расходы на вычислительной мощности. #### Результаты За счет нового подхода, Chimera позволил выявить 43 багов в двух ведущих SMT-решателях: Z3 и cvc5. Из этих 43, 40 багов уже исправлены разработчиками. Эксперименты показали, что Chimera не только увеличил эффективность тестирования, но и повысил качество тестовых формул, при этом существенно сократив время вычислений. Таким образом, Chimera является эффективным инструментом для тестирования и совершенствования существующих SMT-решателей. #### Значимость Полученные результаты важны для многих областей, таких как формальные методы, автоматизированная проверка, и системы символьного вычисления. Улучшенные методы тестирования могут привести к более надежным и производительным системам. Благодаря инновационной интеграции LLMs, Chimera демонстрирует повышенную эффективность в проверке и генерации тестовых формул. Это позволяет