본 논문은 대규모 언어 모델(LLM)이 수학적 증명 생성과 같이 엄격한 논리적 추론과 기호적 추론을 필요로 하는 형식적 영역에서 어려움을 겪는다는 문제를 해결하기 위해 신경 기호 접근 방식을 제안한다. 기하 문제를 중심으로, 유사 문제 검색 및 증명 가이드와 형식적 검증기를 통한 피드백 제공이라는 두 가지 접근 방식을 제시한다. OpenAI의 o1 모델을 대상으로 실험한 결과, 유사 문제와 검증기 피드백 모두 증명 정확도 향상(58%-70%)에 기여하는 것을 확인했다. 이러한 접근 방식은 증명 가능한 정확한 결론을 생성하는 LLM으로의 전환을 통해 신뢰성, 정확성 및 일관성을 크게 향상시켜, 신뢰성이 요구되는 복잡한 작업 및 실제 응용 프로그램을 가능하게 할 수 있다는 점을 시사한다.
