FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4
Created by
- Haebom
Category
Empty
저자
Jiarui Yao, Ruida Wang, Tong Zhang
개요
본 논문에서는 대규모 언어 모델(LLM)의 수학적 추론 능력 향상을 위한 새로운 프레임워크인 FANS(Formal ANswer Selection for Natural Language Math Reasoning Using Lean4)를 제안합니다. FANS는 자연어 수학 문제와 LLM이 생성한 답변을 Lean4 정리 명제로 변환하고, Lean4 증명 검증기를 사용하여 증명을 시도하고 검증합니다. 최종적으로 Lean4의 결과를 이용하여 답변을 선택합니다. 이는 LLM의 정답에 대한 컴퓨터 검증 가능한 해결책을 제공하고, 보상 모델을 넘어서는 대안적인 답변 선택 방법을 제시합니다. MATH-500 및 AMC-23 데이터셋에서 기존 강력한 보상 모델 기반 LLM의 정확도를 최대 1.91% 및 8.33% 향상시키는 효과를 보였으며, 특히 Lean4 전문가 영역인 정수론 분야에서는 모든 정답을 선택할 수 있었습니다. 본 연구는 모든 모델과 데이터셋을 공개하여 관련 분야의 발전을 촉진할 예정입니다.
시사점, 한계점
•
시사점:
◦
Lean4를 활용하여 LLM의 자연어 수학 추론 능력을 향상시키는 새로운 프레임워크 제시.
◦
LLM의 답변에 대한 컴퓨터 검증 가능한 해결책 제공.
◦
보상 모델에 의존하지 않는 대안적인 답변 선택 방법 제시.
◦
MATH-500 및 AMC-23 데이터셋에서 기존 LLM 성능 향상 확인.
◦
모든 모델과 데이터셋 공개를 통한 분야 발전 촉진.
•
한계점:
◦
Lean4 전문가 영역에 국한된 성능 향상 효과. (정수론 분야에서 높은 정확도 달성)
◦
Lean4로의 변환 및 증명 과정의 복잡성 및 계산 비용.
◦
모든 유형의 수학 문제에 대한 일반화 가능성 제한.
