기술 요약: Event-B 에이전트

문제 제기

"구축 시 정확성 (correct by construction)"을 갖춘 소프트웨어 개발은 형식적 방법론에 의존하며, 여기서 시스템 동작과 요구사항은 수학적으로 표현되어 정리 증명과 모델 체킹을 통해 검증됩니다. 그러나 가파른 학습 곡선과 수학적 전문성에 대한 요구는 이러한 방법론의 광범위한 채택을 저해해 왔습니다. 대규모 언어 모델 (LLM) 이 자동 형식화 (autoformalization) 에서 가능성을 보였음에도, 기존 접근법은 정리 증명 없이 형식화를 수행하거나 유한 모델 체킹 (bounded model checking) 으로만 검증된 모델 합성 등 고립된 작업에 크게 국한되어 있습니다.

중요하게도, 현재 LLM 기반 방법론은 형식 모델과 이에 수반되는 증명들의 반복적이고 공동적인 진화를 지원하지 못합니다. 실제로 형식적 개발에서는 정리 증명기가 증명 의무 (PO) 를 해결하지 못할 때, 시스템이 형식 모델과 그 증명 산출물 모두에 대한 수정을 허용해야 합니다. 기존 도구들은 고정된 모델을 가정하고 증명을 탐색하거나 (LLM 증명 보조 도구), 엄격한 증명 기반 검증 없이 모델을 구축 (자동 형식화) 합니다. 모델과 증명의 공동 상태 공간에 걸친 조정된 과정으로서 형식적 개발을 공식화하여 반복적 정제와 수정을 가능하게 하는 프레임워크는 부재합니다.

방법론: Event-B 에이전트

이러한 격차를 해소하기 위해 저자들은 종단 간 (end-to-end) 형식 모델 합성 및 수정을 위한 새로운 신경 - 심볼릭 (neurosymbolic) 프레임워크인 Event-B 에이전트를 제안합니다. 이 프레임워크는 자연어 요구사항을 받아 정제, 합성, 수정을 통합하는 반복적 과정을 통해 형식 Event-B 모델을 구축하도록 설계되었습니다.

방법론은 세 가지 주요 단계로 구성됩니다:

1. 정제 전략 계획

복잡한 시스템에 대한 자동 추론은 검색 공간의 급격한 성장으로 인해 어렵다는 점을 인식하여, Event-B 에이전트는 LLM 을 활용하여 정제 전략을 수립합니다.

• 분해: 에이전트는 자연어 요구사항 집합을 서로소 부분집합으로 분할하여 여러 정제 단계에 분배합니다.
• 결합 불변식 (Gluing Invariants): 각 정제 단계 간 전이에 대해 LLM 은 추상 변수와 구체 변수 간의 일관성을 보장하는 "결합 불변식"을 제안합니다.
• 검증: 이러한 불변식은 모델 체커를 이용한 반례 확인과 증명 시도 등을 통해 검증된 후 승인되며, 이를 통해 이전 단계에서 증명된 속성이 유지되도록 보장합니다.

2. 모델 합성

각 정제 단계에 대해 에이전트는 할당된 요구사항과 결합 불변식을 기반으로 형식 모델을 합성합니다.

• 스키마 기반 생성: LLM 생성에서 흔히 발생하는 구문 오류를 완화하기 위해 시스템은 Event-B 문법을 인코딩한 JSON 스키마를 사용합니다. 이는 필수 이벤트, 변수 선언 등 구조적 정확성을 보장합니다.
• 정형성 루프: 생성된 모델은 컴파일됩니다. 컴파일 오류 (예: 타입 불일치, 선언되지 않은 변수) 는 모델이 구문적으로 유효하고 타입이 정확해질 때까지 LLM 에게 피드백되어 반복적으로 수정됩니다.

3. 모델 및 증명 수정

이는 프레임워크의 핵심 기여로, 모델과 증명의 공동 진화를 처리하도록 설계되었습니다.

• 검증 루프: 합성된 모델은 먼저 모델 체커 (ProB) 를 통해 유한 상태 내 불변식 위반 여부를 확인합니다. 반례가 발견되면 모델이 수정됩니다.
• 정리 증명: 그 후 모델은 무한 상태 정리 증명에 노출됩니다. 증명이 실패하면 시스템은 증명 상태를 분석하여 문제를 진단합니다.
• 수정 규칙 추천: 시스템은 증명 상태를 특정 수정 규칙 (예: "모순된 목표", "존재적 목표", "양화 불변식 보존") 에 매핑하는 새로운 구성 요소를 사용합니다. 이러한 규칙은 수동 증명 해결 경험에서 경험적으로 도출됩니다.
• 원자적 수정 실행: "수정 전략 결정" LLM 이 원자적 수정 함수 (예: StrengthenGuard, AddInvariant, InstantiateHypothesis) 라이브러리에서 선택하여 실행합니다. 이는 LLM 의 수정을 타당하고 검증 가능한 작업으로 제한합니다.
• 타당성: 시스템은 모델 수정 후 모든 증명을 재실행하여 타당성을 보장합니다. SMT 솔버와 정리 증명기에 의해 검증된 목표 PO 를 해결하는 결합 효과가 있을 때만 수정이 승인됩니다.

주요 기여

본 논문은 세 가지 주요 기여를 제시합니다:

1. 프레임워크: Event-B 에이전트는 조정된 모델 구축과 증명 유도를 지원하는 정제 기반 개발을 가능하게 하는 최초의 종단 간 형식 모델 합성 및 수정 프레임워크로, 구축 시 정확성 원칙을 구현합니다.
2. 도구: ProB 를 활용한 모델 체킹과 표준 Rodin 증명기를 활용한 정리 증명을 지원하는 Rodin IDE(Event-B 의 표준 환경) 에 통합된 개념 증명 도구입니다.
3. 평가: 단순한 것부터 복잡한 것까지 27 개의 형식 시스템에 대한 포괄적 평가로, 베이스라인 (LLM + 자동 증명기, Cursor, PAT-Agent) 과의 비교, 제거 실험 (ablation studies), 효율성 분석을 포함합니다.

실험 결과

이 프레임워크는 시스템당 평균 182.41 개의 증명 의무를 가진 27 개의 형식 시스템에서 평가되었습니다. 결과는 베이스라인 (LLM + 자동 증명기, Cursor, PAT-Agent) 대비 상당한 개선을 보여줍니다:

• 일관성 (증명 의무 해결률 - PDR): Event-B 에이전트는 **97.86%**의 PDR 을 달성하여 베이스라인 (89.20%~95.56%) 을 크게 앞섰습니다. 모든 복잡도 수준에서 97.0% 이상의 PDR 을 유지한 반면, 베이스라인은 복잡도가 증가함에 따라 더 큰 변동성과 성능 저하를 보였습니다.
• 정확성 (요구사항 커버리지 - RC 및 충족 - RF):
  • RC: Event-B 에이전트는 **97.13%**를 달성하여 두 번째로 좋은 방법보다 4.63% 높았습니다.
  • RF: Event-B 에이전트는 **93.79%**를 달성하여 두 번째로 좋은 방법보다 18.01% 높았습니다.
  • RF/RC 비율 (0.97) 은 요구사항이 포착되면 에이전트가 관련 증명을 성공적으로 해결함을 나타내며, 베이스라인에서는 포착된 요구사항이 종종 증명되지 않은 채 남아있던 것과 대조됩니다.
• 효율성: 시스템을 합성하고 수정하는 데 걸린 평균 시간은 74.45 분이었습니다. 단일 PO 해결을 시도하는 데 걸린 평균 시간은 0.24 분이었으며, 이는 수정 오버헤드가 시스템 복잡도에 따라 폭발적으로 증가하는 것이 아니라 PO 수에 비례하여 선형적으로 증가함을 시사합니다.
• 제거 실험 (Ablation Studies): 정제 전략이나 수정 가이드 구성 요소 중 하나를 제거하면 성능이 저하되어, 이 두 구성 요소가 상호 보완적임을 확인했습니다. 정제는 증명 복잡도를 줄이는 반면, 수정 가이드는 정제 단계의 정확성을 보장합니다.

의의 및 주장

저자들은 Event-B 에이전트가 실용적이고 타당한 LLM 지원 형식 개발을 향한 유망한 단계라고 주장합니다. 형식적 개발을 모델과 증명의 공동 상태 공간으로 간주함으로써, 이 프레임워크는 고립된 자동 형식화나 정리 증명의 한계를 극복합니다.

논문은 다음 사항을 강조합니다:

• 정제는 복잡성 관리에 필수적이며, 에이전트가 어려운 문제를 관리 가능한 단계로 분해하면서도 정확성을 유지할 수 있게 합니다.
• 증명 기반 수정은 필수적입니다. 유한 모델 체킹만으로는 일반적인 정확성을 보장하기에 부족하며, 무한 정리 증명이 필요하지만 자동 추론이 실패할 때 모델과 증명 모두를 수정할 수 있는 메커니즘이 필요하기 때문입니다.
• 신경 - 심볼릭 접근법은 LLM 의 의미적 유연성과 심볼릭 검증 도구의 엄격한 타당성을 성공적으로 결합합니다.

저자들은 현재 범위에 대해 겸손한 태도를 보이며, 수정 규칙 라이브러리가 경험적으로 도출된 것으로 포괄적이지 않으며, 일관되지 않은 자연어 요구사항 처리는 향후 과제로 남아있음을 지적합니다. 그러나 결과는 제안된 프레임워크가 자연어 요구사항과 구축 시 정확성을 갖춘 형식 모델 간의 격차를 효과적으로 메우고 있음을 시사합니다.