LiveFMBench: 명시 생성에서의 에이전트 기반 워크플로우의 잠재력과 한계 분석

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation

형식적인 명세는 엄격한 프로그램 검증에 필수적이지만, 정확한 명세를 작성하는 것은 비용이 많이 들고 자동화하기 어렵습니다. 대규모 언어 모델(LLM)과 에이전트가 유망한 발전을 보여주고 있지만, 그들의 실제 능력과 실패 사례는 여전히 명확하지 않습니다. 본 연구에서는 C 프로그램에 대한 LLM 및 에이전트 기반 형식 명세 생성을 위한 최초의 체계적이고 오염 방지 연구를 제시합니다. 360개의 새로운 사례를 포함하여 데이터 유출을 완화하도록 설계된 630개의 ACSL(ANSI/ISO C Specification Language) 주석이 달린 C 프로그램으로 구성된 지속적으로 발전하는 벤치마크인 LiveFMBench를 소개합니다. 이 벤치마크를 사용하여 다양한 샘플링 크기, 추론 기능(사고 모드)을 활용한 추론, 에이전트 기반 파이프라인을 평가하고, 세밀한 실패 분석을 수행했습니다. 실험 결과는 직접 프롬프팅 방식으로 모델을 평가할 때 성능이 과대평가되는 경향이 있음을 보여줍니다. 이는 모델이 자동 증명기를 속이거나 코드 컨텍스트 제약을 무시하는 등, 진실되지 않은 동작을 보일 수 있기 때문입니다. 이러한 사례를 제외한 후, 실제 명세 생성 정확도는 약 20% 감소합니다. 또한, 샘플링 크기를 늘리고 사고 모드를 활용하면 성공률이 크게 향상되며, 특히 작은 모델이 사고 모드로부터 더 큰 이점을 얻는 것으로 나타났습니다. 에이전트 기반 파이프라인은 낮은 샘플링 예산과 어려운 데이터 세트에서 특히 효과적입니다. 실패 분석 결과, 잘못된 루프 불변식이 가장 흔한 오류 유형이며, 에이전트 기반 파이프라인은 어설션 오류를 현저히 줄이는 것으로 나타났습니다. 이러한 결과는 현재 LLM 기반 접근 방식의 근본적인 한계를 드러내며, 이러한 방식이 인간이 작성한 형식 명세를 대체하기에는 아직 멀다는 것을 시사합니다. LiveFMBench는 https://huggingface.co/datasets/fm-universe/Live-FM-Bench 에서 제공되며, 향후 연구를 지원하기 위해 모든 평가 자료를 공개합니다.

Formal specification is essential for rigorous program verification, yet writing correct specifications remains costly and difficult to automate. Although large language models (LLMs) and agents have shown promising progress, their true capabilities and failure modes remain unclear. We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs. We introduce LiveFMBench, a continuously evolving benchmark of 630 ACSL (ANSI/ISO C Specification Language)-annotated C programs, including 360 newly collected cases designed to mitigate data leakage. Using this benchmark, we evaluate direct prompting with different sampling sizes, reasoning-enabled (thinking mode) inference, the agentic pipeline, and perform a fine-grained failure analysis. Experimental results reveal that naive evaluation substantially overestimates performance because models under direct prompting may exhibit unfaithful behaviors, such as deceiving automated provers or ignoring code-context constraints; after excluding such cases, the true specification generation accuracy drops by approximately 20\%. We further find that both increased sampling and thinking mode significantly improve success rates, with smaller models benefiting more from thinking mode. Agentic pipelines are particularly effective under low sampling budgets and on harder datasets. Failure analysis further shows that incorrect loop invariants are the dominant error type, while agentic pipelines notably reduce assertion errors. These results expose fundamental limitations in current LLM-based approaches and suggest they remain far from replacing human-authored formal specifications. We release LiveFMBench at https://huggingface.co/datasets/fm-universe/Live-FM-Bench and all evaluation artifacts to support future research.