Event-B Agent: 형식 모델 합성 및 수정을 위한 LLM 에이전트를 향하여

요약

Event-B Agent는 자연어 요구사항을 바탕으로 형식 모델을 구축하고, 형식 검증 피드백을 통해 이를 반복적으로 수정 및 정제하는 새로운 프레임워크입니다. 기존 LLM 기반 접근 방식이 개별 작업에 국한되었던 것과 달리, 모델과 증명을 상호 보완적으로 진화시켜 소프트웨어 설계의 신뢰성을 높입니다. 실험 결과, 다양한 시스템 환경에서 기존 베이스라인 모델보다 뛰어난 엔드 투 엔드 형식 모델 합성 및 수정 성능을 입증했습니다.

핵심 포인트

• 형식 기법(Formal methods)의 높은 진입 장벽을 LLM을 통해 완화하는 것을 목표로 함
• 모델 구축과 검증 피드백이 결합된 인터리브(interleaved) 방식의 프레임워크 제안
• 정제(Refinement)와 모델/증명 수정(Repair) 과정을 통해 모델의 건전성(soundness) 보장
• 기존 모델 대비 엔드 투 엔드 형식 모델 합성 및 수정 측면에서 우수한 성능 확인