본 논문은 형식화 과정에서 요구사항의 논리적 구조를 일관성 있게 유지하는 '형식화를 통한 일관성'이라는 새로운 지침을 제안합니다. LLM을 활용한 추론 작업에서 구조화된 자연어를 중간 계층으로 활용할 때 이 지침이 특히 중요하다고 강조합니다. NASA의 FRET 도구를 분석하고 FRETish를 MTL로 자동 번역하여 모델 검증을 통해 동등성을 입증하고, 새로운 번역이 더 효과적임을 보여줍니다.