SpecAgent: 형식 프로그램 명세의 에이전트적 합성으로 프로그램 검증 역량 강화

요약

본 논문은 복잡한 C 프로그램에 대한 형식 명세(Formal specifications)를 자동으로 합성하는 에이전트적 프레임워크 SpecAgent를 제안합니다. 기존 방식의 한계를 극복하기 위해 의존성 인식 계획, RAG, 에이전트적 수정 및 비평 기능을 통합했습니다. 평가 결과, SpecAgent는 높은 정확도와 재현율로 고품질 명세 합성 및 프로그램 검증에 성공함을 입증했습니다.

핵심 포인트

• SpecAgent: 형식 명세 자동 합성을 위한 에이전트 프레임워크 제시
• 의존성 인식 계획과 RAG를 통합하여 명세 합성 능력 강화
• 에이전트적 수정/비평 기능을 통해 연쇄적인 검증 실패 해결
• 실제 C 프로그램 검증 작업에서 기존 모델 대비 우수한 성능 입증