HUNYUANPROVER：自動定理証明のためのスケーラブルなデータ合成フレームワークと誘導ツリーサーチ

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

December 30, 2024

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

cs.AI

要旨

Hunyuan 7B からファインチューニングされた言語モデル HunyuanProver を紹介します。LEAN4 を用いた対話型自動定理証明に使用されます。データの希少性の問題を緩和するため、低コストでデータを反復的に合成するスケーラブルなフレームワークを設計しています。さらに、「システム2の思考」を可能にするために、誘導された木探索アルゴリズムが設計されています。HunyuanProver は主要なベンチマークで最先端のパフォーマンスを達成しています。具体的には、現在の SOTA 結果である 65.9% に比べて、miniF2F-test で 68.4% の合格率を達成しています。miniF2F-test では imo_1960_p2、imo_1962_p2、imo_1964_p2、imo_1983_p6 の 4 つの IMO ステートメントを証明しています。コミュニティに貢献するために、30k の合成されたインスタンスのデータセットをオープンソースで公開します。各インスタンスには、自然言語での元の質問、自動形式化による変換された文、および HunyuanProver による証明が含まれています。

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.