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

설계 및 개발 단계에서부터 신뢰성을 보장함으로써, 구축 시점부터 올바른 (correct by construction) 소프트웨어를 만드는 것은 소프트웨어 공학의 오랜 목표입니다. 형식 기법 (Formal methods)은 시스템의 동작과 요구사항을 수학적으로 표현할 수 있게 함으로써, 정리 증명 (theorem proving) 및 모델 검증 (model checking)을 포함한 형식 검증 (formal verification)을 통해 정확성을 보장하며 이러한 비전을 실현합니다. 그러나 가파른 학습 곡선과 수학적 전문 지식에 대한 요구는 형식 기법의 광범위한 도입을 저해합니다. 최근 대규모 언어 모델 (LLMs)은 자동 형식화 (autoformalization)를 통해 이러한 격차를 해소할 가능성을 보여주었습니다. 하지만 기존의 LLM 기반 접근 방식은 형식화 없는 정리 증명이나 불충분한 검증을 동반한 모델 합성 등 고립된 작업에 크게 국한되어 있습니다. 이러한 노력들은 가치가 있지만, 모델과 증명이 함께 진화하는, 즉 실제 개발 관행을 밀접하게 반영하는 보다 포괄적인 프레임워크의 잠재력을 완전히 활용하지 못하고 있습니다. 이러한 격차를 해소하기 위해, 우리는 소프트웨어 설계의 인터리브 (interleaved) 특성에서 영감을 얻은 새로운 프레임워크인 Event-B Agent를 제안합니다. 자연어 요구사항이 주어지면, Event-B Agent는 초기 모델을 구축하고 형식 검증 피드백을 사용하여 이를 반복적으로 수정 및 정제합니다. 정제 (Refinement)는 증명 방출 (proof discharge)을 단순화하며, 모델과 증명의 수정 (repair)은 각 정제 단계의 건전성 (soundness)을 보장합니다. 이 두 구성 요소는 서로를 강화하여 모델 품질을 점진적으로 향상시킵니다. 다양한 복잡도의 시스템에 대한 평가 결과, Event-B Agent는 합리적인 효율성을 유지하면서도 엔드 투 엔드 (end-to-end) 형식 모델 합성 및 수정 측면에서 베이스라인 모델들을 크게 능가함을 입증했습니다. 이러한 결과는 Event-B Agent가 구축 시점부터 올바른 (correct-by-construction) 형식 모델 합성 및 수정을 향한 유망한 단계임을 시사합니다.