모델 기반 증명 스케치를 통한 형식 모델 구축

형식 모델링은 시스템의 정확성에 대한 강력한 보장을 제공하지만, 형식 모델을 개발하고 수정하는 과정은 여전히 노동 집약적이며 논리와 형식 추론에 대한 상당한 전문 지식을 요구합니다. 최근 LLM 기반 자동 형식화 에이전트들은 후보 형식 모델을 생성하고 형식 도구의 피드백을 사용하여 이를 수정함으로써 이러한 부담을 줄이고자 합니다. 하지만 기존 접근 방식들은 '생성 후 수정(generate-and-repair)' 패러다임을 따르며, 여기서 수정은 생성된 모델의 검증 실패에 의해 주도되므로 피드백의 세분성과 LLM의 수정 능력 모두에 크게 의존합니다. 결과적으로, 한 수준의 검증을 목표로 하는 수정이 다른 수준의 속성을 무효화할 수 있으며, 이는 전체 이벤트 가드(event guards) 집합에 대한 추론을 필요로 합니다. 이러한 한계를 해결하기 위해, 우리는 모델 기반 증명 스케치(model-based proof sketches)를 중심으로 하는 자동 형식화 방법인 Proof-Sketch-Guided Formal Model Synthesis (ProGS)를 제안합니다. 모델 기반 증명 스케치는 목표 형식 시스템의 증명 구조를 트리 형태로 나타냅니다. 내부 노드는 케이스 분할 및 귀납적 추론 단계를 포착하며, 리프 노드는 개별 하위 목표(subgoals)를 실현하는 구체적인 상태 전이 이벤트에 해당합니다. ProGS는 LLM을 사용하여 이러한 스케치를 생성하고 수정하며, 검증 실패는 특정 노드와 서브트리로 매핑되어 반복적인 수정을 위한 구조화된 지침을 제공합니다. 27개의 형식 시스템으로 구성된 벤치마크에서 수행한 우리의 평가는 ProGS가 구문적 유효성(syntactic validity), 연역적 검증 가능성(deductive verifiability), 그리고 행위적 정확성(behavioral correctness) 측면에서 최첨단 에이전트 형식 모델링 접근 방식보다 개선되었음을 보여주었으며, 이는 계층적 증명 스케치를 중심으로 형식 모델 구축을 조직하는 것의 이점을 입증합니다.