Solving Inequality Proofs with Large Language Models
Created by
- Haebom
Category
Empty
저자
Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, Pan Lu
개요
부등식 증명은 다양한 과학 및 수학 분야에서 중요한 역할을 하며, 엄밀한 경계 발견과 전략적 정리를 적용하는 등 고급 추론 기술을 테스트합니다. 본 논문은 LLM(Large Language Model)이 이 분야에서 어려움을 겪는다는 점에 주목하여, 부등식 증명 문제를 자동으로 검증 가능한 두 개의 하위 작업(경계 추정 및 관계 예측)으로 재구성하는 비공식적인 작업 방식을 제안합니다. 올림피아드 수준의 부등식을 포함하는 전문가가 큐레이션한 데이터세트인 IneqMath를 공개하며, 단계별 솔루션과 정리 주석이 포함된 테스트 세트와 훈련 코퍼스를 제공합니다. 또한 최종 답변 판단과 일반적인 추론 결함을 감지하기 위한 4개의 단계별 판단을 결합한 새로운 LLM-as-judge 평가 프레임워크를 개발했습니다. 29개의 선도적인 LLM에 대한 체계적인 평가 결과, o1과 같은 최고 모델조차 단계별 검토 하에서 10% 미만의 정확도를 보이며 최종 답변 동등성만 고려할 때 최대 65.5% 감소하는 것을 발견했습니다. 이는 현재 LLM이 답을 찾는 것과 엄격한 증명을 구성하는 것 사이의 중요한 격차를 보여줍니다.
시사점, 한계점
•
시사점:
◦
LLM의 부등식 증명 능력은 최종 답의 정확도만으로는 과대평가될 수 있으며, 단계별 추론의 정확성을 평가하는 것이 중요합니다.
◦
현존하는 LLM은 부등식 증명에서 취약한 추론 능력을 보이며, 이는 정리 기반 추론 및 자기 개선과 같은 연구 방향의 필요성을 제시합니다.
◦
모델 크기 증가 및 테스트 시간 계산량 증가는 전체 증명 정확도 향상에 제한적인 효과를 보입니다.
•
한계점:
◦
논문 자체에서 구체적인 한계점은 제시되지 않았습니다.
