본 논문은 대규모 언어 모델(LLM)을 사용하여 자연어 계획과 예상되는 동작 간의 정렬을 평가하는 새로운 프레임워크를 소개합니다. 이 프레임워크는 자연어 계획을 크립키 구조와 선형 시간 논리(LTL)로 변환하고 모델 검증을 수행합니다. PlanBench 계획 검증 데이터세트의 단순화된 버전을 대상으로 체계적으로 평가하고 정확도, 정밀도, 재현율, F1 점수와 같은 지표를 보고합니다. 실험 결과 GPT-5가 96.3%의 F1 점수를 달성하며 훌륭한 분류 성능을 보였고, 거의 항상 구문적으로 완벽한 형식을 생성하여 보장 역할을 할 수 있음을 보여줍니다. 하지만 의미적으로 완벽한 형식 모델의 합성은 향후 연구 과제로 남아있습니다.
