본 논문은 자연어 처리(NLP)와 대규모 언어 모델(LLM)의 발전을 활용하여, 자연어 문장을 형식 논리로 자동 변환하는 새로운 프레임워크를 제시한다. 이 프레임워크는 소프트웨어 시스템의 자동 추론, 디버깅, 루프 불변식 찾기, 명세 준수를 돕기 위해 설계되었다. 특히, LLM의 환각(hallucination) 문제를 해결하기 위해, 영어 문장을 논리식으로 변환하고, 이를 다시 CNF(Conjunctive Normal Form)로 변환하여 만족성 문제를 해결한다. 클래식 NLP 기술, 자체 정의 문법, 기호 계산 라이브러리, 그리고 미세 조정된 언어 모델을 활용하여 환각을 줄이고 신뢰성 있는 CNF 생성을 목표로 한다.
