NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic

Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28\% semantic equivalence with reference specifications while ensuring 86\% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.

한 줄 요약

**[NL→LTL / Neurosymbolic]** NeuroNL2LTL이 자연어→LTL 변환을 verifier-in-the-loop RL로 학습 — structure-preserving 중간표현·SAT/non-triviality 검사·minimal-edit repair로 200,000+ 요구사항에서 28% semantic equivalence·86% verified satisfiable.

핵심 기여도

자연어(NL)와 Linear Temporal Logic(LTL) 같은 formal logic 간 효과 변환에 전문성이 필요해 안전 critical 개발에서 formal verification의 reach가 제한됨을 진단. Template 기반 접근은 expressiveness를 sacrifice하고 reliability를 얻지만, neural method는 fluency를 달성하나 correctness 보장 부재.
NeuroNL2LTL 제시 — 학습된 변환과 formal verification을 unify하는 neurosymbolic 아키텍처.
변환을 intermediate representation을 통해 route, 그 LTL로의 mapping이 structure-preserving by construction. 생성된 specification은 satisfiability·non-triviality 검사 거치고, minimal-edit repair 메커니즘이 near-miss output을 downstream tool에 도달 전 교정.
핵심 혁신은 verifier-in-the-loop training — verification outcome이 RL reward signal로 작용해 formal correctness에 직접 최적화하는 neural 컴포넌트 생성. 항공우주·로봇·자율주행 등 10+ 추가 도메인의 200,000+ requirement에서 NeuroNL2LTL이 reference specification과 28% semantic equivalence 달성·output의 86%가 verified satisfiable. LTL에서 contextually grounded 설명도 생성해 도메인 전문가가 specialized 학습 없이 specification validate 가능.

핵심 아이디어

자연어→LTL 변환의 신뢰성·유창성 trade-off는 formal verification을 학습 objective와 runtime filter로 동시 활용하는 neurosymbolic 디자인으로 해소 가능하며, structure-preserving 중간표현·minimal-edit repair·verifier-in-the-loop RL이 핵심 메커니즘이다.

기술적 접근법

**방법론**: NeuroNL2LTL — neurosymbolic + verifier-in-the-loop RL training.
**핵심 기법**: (1) Structure-preserving 중간표현으로 변환 route, (2) SAT·non-triviality 검사로 spec validation, (3) Minimal-edit repair로 near-miss output 교정, (4) Verifier 결과를 RL reward로 사용해 formal correctness 직접 최적화, (5) LTL에서 contextually grounded 자연어 설명 생성.

주요 결과

항공우주·로봇·자율주행 등 10+ 도메인 200,000+ requirement 평가.
Reference specification과 28% semantic equivalence.
Output의 86%가 verified satisfiable.
Domain expert의 specialized 학습 없는 specification validation 가능.

의의 및 한계

**의의**: Formal verification을 training·runtime 양쪽 활용하는 neurosymbolic 패러다임, 200,000+ requirement 대규모 검증, 도메인 전문가용 설명 생성으로 채택 장벽 낮춤, 안전 critical 개발의 reach 확대. **한계**: 28% semantic equivalence는 still 낮음(개선 여지), LTL에 한정·다른 formal logic(CTL·µ-calculus 등) 일반화 별도, minimal-edit repair의 부적합 case 존재.

실용적 활용

안전 critical 시스템(자율주행·항공·의료)의 formal specification 자동화.
도메인 전문가의 verification 도구 진입 장벽 감소.
Neurosymbolic AI의 안전성 보장 설계 일반 패턴.