Локальный успех не складывается: оценка крупных языковых моделей в задачах композиционной формальной верификации

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification

September 27, 2025

Авторы: Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan

cs.AI

Аннотация

Мы представляем DafnyCOMP — эталонный набор для оценки больших языковых моделей (LLM) в задаче генерации композиционных спецификаций на языке Dafny. В отличие от предыдущих эталонов, которые сосредоточены на задачах с одной функцией, DafnyCOMP ориентирован на программы, состоящие из нескольких взаимодействующих функций с зависимостями данных, что требует рассуждений за пределами отдельных компонентов. Набор включает 300 автоматически синтезированных программ с несколькими функциями. Мы оцениваем несколько современных семейств LLM и обнаруживаем, что, хотя они хорошо справляются с верификацией отдельных функций, их производительность резко снижается на композиционных задачах. Анализ выявляет систематические ошибки в межфункциональных рассуждениях, включая хрупкие спецификации, несоответствие между реализациями и доказательствами, а также неустойчивые рассуждения. Таким образом, DafnyCOMP предоставляет диагностический инструмент для измерения прогресса в направлении надежной, верифицируемой и композиционной генерации кода с использованием LLM.

English

We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-function tasks, DafnyCOMP targets programs composed of multiple interacting functions with data dependencies, requiring reasoning across component boundaries. The benchmark consists of 300 automatically synthesized multi-function programs. We evaluate several state-of-the-art LLM families and find that, while they perform well on single-function verification, their performance drops sharply on compositional tasks. Analysis reveals systematic failures in cross-functional reasoning, including fragile specifications, misalignment between implementations and proofs, and unstable reasoning. DafnyCOMP thus provides a diagnostic tool for measuring progress toward reliable, verifiable, and compositional code generation with LLMs.