LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
Created by
Haebom
저자
Junyu Lai, Jiakun Zhang, Shuo Xu, Taolue Chen, Zihang Wang, Yao Yang, Jiarui Zhang, Chun Cao, Jingwei Xu
개요
본 논문은 대규모 언어 모델(LLM)을 이용한 자동 정리 증명 분야에서, LLM 기반 단계적 증명기를 트리 탐색에 통합하는 기존 연구를 발전시킨 새로운 증명 상태 탐색 접근법을 제시합니다. 다양한 중간 증명 상태에서 다양한 전략을 생성하는 훈련 데이터 합성 방법을 통해 LLM을 정책 모델로 효과적으로 원샷 미세 조정할 수 있도록 설계되었습니다. 또한, 데이터 합성 방법을 효과적으로 활용하고 트리 탐색 중 탐색과 활용 간의 균형을 이루는 적응형 빔 크기 전략을 제안합니다. MiniF2F 및 ProofNet 벤치마크에 대한 평가 결과, 엄격한 Pass@1 지표에서 강력한 기준 모델보다 우수한 성능을 보이며, MiniF2F에서 평균 통과율 60.74%, ProofNet에서 21.18%를 달성했습니다. 이러한 결과는 대규모 합성 데이터가 자동 정리 증명 발전에 미치는 영향을 강조합니다.
시사점, 한계점
•
시사점:
◦
다양한 중간 증명 상태에서 다양한 전략을 생성하는 훈련 데이터 합성 방법을 통해 LLM 기반 자동 정리 증명의 성능 향상 가능성을 제시.
◦
적응형 빔 크기 전략을 통해 트리 탐색의 효율성을 높임.
◦
MiniF2F 및 ProofNet 벤치마크에서 기존 방법 대비 우수한 성능을 달성, 대규모 합성 데이터의 중요성을 입증.
•
한계점:
◦
제시된 방법의 일반화 성능에 대한 추가적인 연구가 필요.
◦
특정 벤치마크에 대한 성능 향상이 다른 벤치마크에도 적용될 수 있는지에 대한 검증 필요.
◦
Pass@1 지표만 사용하여 평가되었으므로, 다른 평가 지표를 사용한 추가적인 실험이 필요.
