HUNYUANPROVER: 자동 정리 증명을 위한 확장 가능한 데이터 합성 프레임워크 및 안내 트리 탐색

초록

우리는 LEAN4와 상호작용하는 자동 정리 증명을 위해 Hunyuan 7B에서 finetuned된 언어 모델인 HunyuanProver를 소개합니다. 데이터 희소성 문제를 완화하기 위해, 우리는 저비용으로 데이터를 반복적으로 합성하는 확장 가능한 프레임워크를 설계했습니다. 또한, 유도된 트리 탐색 알고리즘을 설계하여 증명자의 효과적인 "시스템 2 사고"를 가능하게 합니다. HunyuanProver는 주요 벤치마크에서 최신 기술 성능을 달성합니다. 구체적으로, 현재 SOTA 결과인 65.9%에 비해 miniF2F-test에서 68.4%의 통과율을 달성합니다. HunyuanProver는 miniF2F-test에서 imo_1960_p2, imo_1962_p2, imo_1964_p2 및 imo_1983_p6의 4개 IMO 문을 증명합니다. 커뮤니티에 이바지하기 위해, 우리는 각 인스턴스가 자연어로 된 원래 질문, 자동 형식화에 의해 변환된 문장, 그리고 HunyuanProver에 의한 증명이 포함된 30k 합성 인스턴스 데이터셋을 오픈 소스로 공개할 예정입니다.

English

We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesize data with low cost. Besides, guided tree search algorithms are designed to enable effective ``system 2 thinking`` of the prover. HunyuanProver achieves state-of-the-art (SOTA) performances on major benchmarks. Specifically, it achieves a pass of 68.4% on the miniF2F-test compared to 65.9%, the current SOTA results. It proves 4 IMO statements (imo_1960_p2, imo_1962_p2}, imo_1964_p2 and imo_1983_p6) in miniF2F-test. To benefit the community, we will open-source a dataset of 30k synthesized instances, where each instance contains the original question in natural language, the converted statement by autoformalization, and the proof by HunyuanProver.

HUNYUANPROVER: 자동 정리 증명을 위한 확장 가능한 데이터 합성 프레임워크 및 안내 트리 탐색

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

초록

Summary

Support