Daily Arxiv

전 세계에서 발간되는 인공지능 관련 논문을 정리하는 페이지 입니다.
본 페이지는 Google Gemini를 활용해 요약 정리하며, 비영리로 운영 됩니다.
논문에 대한 저작권은 저자 및 해당 기관에 있으며, 공유 시 출처만 명기하면 됩니다.

HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

Created by
  • Haebom
Category
Empty

저자

Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, Haitao Mi

개요

Hunyuan 7B를 기반으로 LEAN4를 사용한 대화형 자동 정리 증명을 위해 미세 조정된 언어 모델 HunyuanProver를 소개합니다. 데이터 부족 문제를 완화하기 위해 저렴한 비용으로 데이터를 반복적으로 합성하는 확장 가능한 프레임워크를 설계했습니다. 또한, 증명자의 효과적인 "시스템 2 사고"를 가능하게 하는 안내 트리 검색 알고리즘을 설계했습니다. HunyuanProver는 주요 벤치마크에서 최첨단(SOTA) 성능을 달성합니다. 구체적으로, miniF2F-test에서 현재 SOTA 결과인 65.9%에 비해 68.4%의 통과율을 달성했습니다. miniF2F-test에서 4개의 IMO 명제(imo_1960_p2, imo_1962_p2, imo_1964_p2, imo_1983_p6)를 증명했습니다. 커뮤니티에 도움이 되도록 자연어로 된 원래 질문, 자동 공식화에 의해 변환된 명제, HunyuanProver에 의한 증명을 포함하는 30,000개의 합성 인스턴스 데이터셋을 오픈 소스로 공개할 예정입니다.

시사점, 한계점

•
시사점:
◦
저렴한 비용으로 데이터를 반복적으로 합성하는 확장 가능한 프레임워크를 통해 데이터 부족 문제를 효과적으로 해결했습니다.
◦
안내 트리 검색 알고리즘을 통해 효과적인 "시스템 2 사고"를 가능하게 하여 정리 증명 성능을 향상시켰습니다.
◦
주요 벤치마크에서 최첨단(SOTA) 성능을 달성했습니다. 특히 miniF2F-test에서 68.4%의 통과율을 기록했습니다.
◦
4개의 IMO 명제 증명 성공.
◦
30,000개의 합성 인스턴스 데이터셋 오픈 소스 공개를 통해 연구 커뮤니티에 기여합니다.
•
한계점:
◦
논문에서는 구체적인 한계점이 언급되지 않았습니다. 향후 연구를 통해 추가적인 개선이 필요할 수 있습니다. 예를 들어, 더욱 복잡한 정리에 대한 증명 성능 개선, 다른 정리 증명 시스템과의 비교 분석 등이 추가 연구 과제로 고려될 수 있습니다.
👍
Made with Slashpage