NeuroNL2LTL은 자연어(NL)를 선형 시제 논리(LTL)로 변환하는 신경기호 아키텍처로, 학습된 번역과 공식 검증을 통합한다. 항공우주·로보틱스·자율주행 등 10개 이상 도메인의 20만 건 이상 요구사항에서 28%의 의미 동등성과 86%의 검증 가능 출력을 달성했다. 검증기-인-더-루프 훈련 방식은 공식 검증 결과를 강화학습 보상으로 활용해 신경 컴포넌트가 형식적 정확성을 직접 최적화하도록 한다. 최소 편집 수정 메커니즘과 맥락 기반 설명 생성을 포함해, 비전문가도 LTL 명세를 검증할 수 있어 형식 검증의 접근성을 크게 높였다.

• •20만 건+ 요구사항에서 28% 의미 동등성, 86% 검증 가능 출력 달성 — 항공우주·로보틱스·자율주행 등 10개 이상 도메인 포함
• •검증기-인-더-루프 훈련: 공식 검증 결과를 강화학습 보상 신호로 사용해 통계적 자신감 아닌 논리적 보장 기반 신뢰성 확보
• •최소 편집 수정 메커니즘이 경계 출력을 다운스트림 도구 전달 전 자동 수정
• •LTL로부터 맥락 기반 설명 생성으로 비전문가도 명세 검증 가능