Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs

기술 요약: 계층적 의미론적 분해를 통한 자연어와 형식 사양 간의 가교 형성

문제 정의
자연어(NL) 소프트웨어 요구사항을 선형 시제 논리(LTL)와 같은 형식 사양으로 정확하고 자동화된 방식으로 변환하는 것은 항공우주와 같은 안전 필수 산업 분야에서 형식 검증을 확장하는 데 있어 핵심적인 병목 구간이다. 현재의 산업 관행은 인간 전문가의 수동 번역에 크게 의존하고 있으며, 이 과정은 시간 소모적이고 오류가 발생하기 쉽다. 규칙 기반 시스템부터 학습 기반 방법까지 다양한 기존 자동화 접근 방식들이 자동화를 제공하긴 하지만, 상당한 한계에 직면해 있다. 규칙 기반 방법은 유연성이 부족하고 자연어의 가변성에 대응하기 어려우며, 학습 기반 방법은 훈련 데이터 이상의 일반화에 실패하는 경우가 많다. 최근의 대규모 언어 모델(LLM)은 의미 추출 능력은 뛰어나지만, 실제 산업용 요구사항에 내재된 암시적 시제 의미론, 깊게 중첩된 논리 구조, 그리고 문맥 특화된 제약 조건들을 다루는 데 어려움을 겪는다. LLM을 직접 적용할 경우, 오류 누적과 구조적 검증의 부재로 인해 생성된 공식이 구문적으로는 유효하지만 의미론적으로는 틀린 "침묵의 실패(silent failures)"가 발생하곤 한다.

방법론: REQ2LTL 프레임워크
저자들은 이러한 과제를 해결하기 위해, 새로운 계층적 중간 표현인 OnionL을 통해 자연어와 LTL을 연결하는 모듈형 프레임워크인 REQ2LTL을 제안한다. 이 프레임워크는 LLM의 의미 추출 능력과 결정론적 규칙 기반 합성의 구조적 보장을 결합한 2단계 파이프라인을 통해 작동한다.

1. 중간 표현 (OnionL):
   OnionL은 시제 의미론, 범위(scope), 논리적 관계를 명시적으로 인코딩하도록 설계된 트리 구조의 중간 언어이다. 이는 요구사항을 세 가지 구성 요소로 분해한다:

   • 원자 명제 (Atomic Propositions, APs): 의미론적 하위 필드(구성 요소, 변수, 관계, 공식)가 주석 처리된 술어 수준의 사실.
   • 범위 (Scopes): 단항 연산자(예: Globally, Eventually, Next) 또는 모드 기반 전제 조건에 대응하는 문맥적 경계.
   • 관계 (Relations): 하위 공식들을 연결하는 논리적 또는 시제적 의존성 (예: And, Or, Implies, Until).
     이 구조는 LTL의 구성적 구문을 반영하며, LLM이 국소적인 의미 파싱에 집중하고 글로벌 논리 구성을 규칙 기반 메커니즘에 위임할 수 있도록 하는 의미론적 가교 역할을 한다.

2. 1단계: REQ2ONIONL (의미론적 분해):
   이 모듈은 프롬프트 가이드형 LLM을 사용하여 자유 형식의 자연어 요구사항을 구조화된 OnionL 트리로 변환한다. 이는 BUILDING-ONIONL이라는 특정 사고 사슬(Chain-of-Thought) 알고리즘을 사용하며, 두 단계로 작동한다:

   • 매크로 구조 추출: 글로벌 시제 또는 모드 기반 범위를 식별하여 최상위 노드를 구축한다.
   • 재귀적 절 분해: 절을 중첩된 범위, 관계 및 정규화된 원자 명제로 재귀적으로 분해한다.
     이 과정은 OnionL의 재귀적 문법을 정의하는 지식 저장소에 의해 가이드되며, 산업 패턴에 대한 퓨샷(few-shot) 예시에 의해 강화된다.

3. 2단계: ONIONL2LTL (규칙 기반 합성):
   이 모듈은 검증된 OnionL 트리를 표준화된 LTL 공식으로 결정론적이고 규칙 기반으로 번역한다.

   • 검증: 번역 전, 시스템은 깊이 우선 탐색을 수행하여 구조적 적절성(예: 연산자의 올바른 인수 개수, 유효한 범위 중첩)을 검증한다. 안전 필수 애플리케이션을 위해, 본 프레임워크는 엔지니어가 검사 및 수정을 할 수 있도록 OnionL 구조를 시각화(Mermaid 다이어그램 활용)하는 "휴먼 인 더 루프(human-in-the-loop)" 메커니즘을 지원한다.
   • 번역: 후위 순회(post-order traversal)를 통해 각 노드를 그에 상응하는 LTL 구문으로 변환한다(예: Globally를 $G$로 매핑, Implies를 $\rightarrow$로 매핑). 이 과정은 모든 출력이 설계에 의해 구문적으로 유효함을 보장한다.

주요 기여

• OnionL 중간 표현: 시제 의미론과 논리적 관계를 명시적으로 인코딩하여 자연어와 LTL 사이의 견고한 의미론적 가교 역할을 하는 계층적 언어.
• 계층적 의미론적 분해: 요구사항을 체계적으로 분해하여 구조적 무결성과 의미론적 정확도를 크게 향상시키는 프롬프트 기반의 2단계 알고리즘 (BUILDING-ONIONL).
• REQ2LTL 프레임워크: LLM 기반의 분해와 결정론적 규칙 기반 번역 및 검증을 결합한 자동화된 파이프라인. 이는 기존 방식들보다 우수한 정확도와 완벽한 구문적 정확성을 달sq성한다.

실험 결과
저자들은 학술적 벤치마크(Circuit, Navigation, Office Email)와 112개의 항공우주 요구사항으로 구성된 실제 산업 데이터셋을 통해 REQ2LTL을 평가하였다.

• 산업 성능: 항공우주 데이터셋에서 REQ2LTL은 88.4%의 의미론적 정확도(Exact Match)와 100%의 구문적 정확성을 달성했다. 이는 중첩된 논리와 암시적 시제 단서 처리에 어려움을 겪으며 55%에서 65% 사이의 Exact Match율을 보인 최신 기술(SOTA) 베이스라인(예: NL2SPEC, NL2LTL, NL2TL)을 크게 상회하는 결과이다.
• 학술 성능: 학술적 벤치마크에서 REQ2LTL은 일관되게 높은 성능(Binary Accuracy >94%, BLEU >0.97)을 보였으며, 모호함이 적은 환경에서도 효과적으로 일반화되었다.
• 절제 연구 (Ablation Studies): 실험을 통해 구조화된 모델링(OnionL), 단계별 프롬프팅, 그리고 검증 피드백의 조합이 필수적임을 확인했다. 구조화된 중간 표현을 제거하면 의미론적 정확도가 65.2%로 떨어졌고, 단계별 프롬프팅을 제거하면 58.9%로 감소했다.
• 오류 분석: 프레임워크는 제로샷(zero-shot) 및 기타 베이스라인 방법들에서 빈번하게 나타났던 시제 오해, 조건 혼동, 중첩 손실 관련 오류를 효과적으로 제거했다. 남은 오류들은 주로 입력 요구사항 자체의 내재적인 언어적 모호성에 기인했다.

의의 및 주장
본 논문은 REQ2LTL이 비형식적인 자연어 요구사항과 형식 사양 사이의 간극을 효과적으로 메워, 안전 필수 산업 시스템에서 확장 가능한 채택을 위한 실질적인 토대를 제공한다고 주장한다. 구조화된 중간 표현과 LLM-규칙 기반 하이브리드 아키텍처를 도입함으로써, 본 프레임워크는 직접적인 LLM 번역의 한계, 특히 암시적 시제 의미론과 깊은 논리 중첩 문제를 해결한다. 저자들은 규칙 기반 합성을 통해 100%의 구문적 정확성을 보장하는 동시에 높은 의미론적 충실도를 확보하는 REQ2LTL의 능력이 산업 검증 워크플로우의 유효한 도구가 된다는 점을 강조한다. 또한, 시각화된 휴먼 인 더 루프 검증 단계의 포함은 언어적 모호성 문제를 해결하여, 엔지니어가 자동화 파이프라인을 깨뜨리지 않고도 의미론적 오류를 효율적으로 수정할 수 있게 한다. 저자들은 현재 작업이 LTL에 집중하고 있으나, 향후 신호 시제 논리(STL)나 메트릭 시제 논리(MTL)와 같이 더 표현력이 풍부한 시제 논리로 확장될 수 있음을 언급하였다.