FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

작성자

Haebom

카테고리

Empty

저자

Haoran Ding, Zhaoguo Wang, Haibo Chen

💡 개요

이 논문은 대규모 시스템의 코드 정확성을 강화하기 위해 LLM 기반의 호어 스타일 추론을 활용하는 FM-Agent라는 프레임워크를 제안합니다. FM-Agent는 LLM을 통해 함수 수준의 명세(specification)를 자동으로 생성하고, 자연어 명세를 이해하여 호어 스타일 추론을 수행하며, 잠재적 버그를 트리거하는 테스트 케이스를 자동 생성합니다. 평가 결과, FM-Agent는 2일 안에 143k LoC에 달하는 대규모 시스템에 대한 추론을 성공적으로 수행했으며, 기존 개발자들이 테스트했음에도 불구하고 522개의 새로운 버그를 발견했습니다.

🔑 시사점 및 한계

•

LLM을 활용하여 대규모 시스템에 대한 자동화된 구성 요소별 추론을 최초로 실현했습니다.

•

개발자의 의도를 반영하는 함수 명세를 LLM을 통해 자동으로 생성하고, 자연어 명세를 기반으로 추론할 수 있습니다.

•

522개의 새로운 버그를 발견하며 기존 테스트로는 탐지하기 어려운 심각한 오류를 효과적으로 찾아냈습니다.

•

LLM이 생성한 복잡한 코드의 의도 파악 및 명세 생성의 정확성이 추론 결과에 중요한 영향을 미칠 수 있으며, LLM의 환각(hallucination) 문제에 대한 고려가 필요합니다.

PDF 보기

Made with Slashpage