대규모 언어 모델(LLM)은 텍스트 생성, 분류, 질문 응답 등 다양한 작업에서 놀라운 능력을 보여주지만, 추론 능력은 여전히 논쟁의 대상입니다. 자연어(NL)의 내재된 모호성은 LLM의 검증 가능한 추론 능력을 제한하여 답변의 일관성과 신뢰성 있는 지원을 부족하게 만듭니다. 이러한 문제를 해결하기 위해, 본 논문에서는 Lean4를 사용하여 NL 수학 추론 능력을 향상시키는 새로운 프레임워크인 FANS: Formal ANswer Selection for Natural Language Math Reasoning Using Lean4를 제안합니다. FANS는 NL 수학 문제와 LLM이 생성한 답변을 Lean4 정리 명제로 변환하고, Lean4 증명기를 사용하여 증명을 시도하고 Lean4로 검증합니다. 최종적으로, FL 결과를 사용하여 답변 선택을 지원합니다. 본 프레임워크는 올바른 답변에 대한 컴퓨터 검증 가능한 솔루션을 제공함으로써 LLM의 NL 수학 능력을 향상시키고, 보상 모델을 넘어선 답변 선택의 대안을 제시합니다. 광범위한 실험 결과, 본 프레임워크가 MATH-500 데이터 세트에서 보상 모델이 향상된 LLM의 정확도를 최대 1.91%까지, AMC-23에서 최대 8.33%까지 향상시킬 수 있음을 보여주었습니다. Lean4 전문가들이 강점을 보이는 정수론과 같은 특정 분야에서는 모든 정답을 선택할 수도 있습니다. 질적 분석 결과 또한 본 프레임워크가 NL 결과를 Lean4 증명으로 공식적으로 뒷받침할 수 있음을 보여줍니다. 본 연구는 해당 분야의 선구적인 연구로서, 모든 모델과 데이터 세트를 공개하여 해당 분야의 발전을 더욱 촉진할 것입니다.
