본 논문은 대규모 언어 모델(LLM)이 수학적 증명 생성과 같이 엄격한 논리적 추론과 기호적 추론을 요구하는 형식적 영역에서 어려움을 겪는다는 문제를 해결하기 위해 신경 기호 접근 방식을 제안합니다. 기하학 문제를 중심으로, 유사 문제 검색 및 증명을 활용하여 LLM을 안내하고, 형식 검증기를 통해 생성된 증명을 평가하고 피드백을 제공하여 모델의 오류 수정을 돕는 2단계 접근 방식을 제시합니다. OpenAI의 o1 모델을 대상으로 실험한 결과, 증명 정확도가 58%-70% 향상되었으며, 유사 문제와 검증기 피드백 모두 성능 향상에 기여함을 보였습니다. 이는 증명 가능한 정확한 결론을 생성하는 LLM으로 전환함으로써 신뢰성, 정확성, 일관성을 크게 향상시켜 신뢰성이 필요한 복잡한 작업과 실제 응용 분야를 가능하게 할 수 있음을 시사합니다.
