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

要約

LEAN4 を使用した対話型自動定理証明用に Hunyuan 7B から微調整された言語モデル、HunyuanProver を紹介します。
データの疎性の問題を軽減するために、低コストでデータを反復合成するためのスケーラブルなフレームワークを設計します。
さらに、ガイド付きツリー検索アルゴリズムは、証明者の効果的な「システム 2 思考」を可能にするように設計されています。
HunyuanProver は、主要なベンチマークで最先端 (SOTA) のパフォーマンスを達成します。
具体的には、miniF2F テストでは、現在の SOTA 結果の 65.9% と比較して 68.4% の合格率を達成しています。
miniF2F テストで 4 つの IMO ステートメント (imo_1960_p2、imo_1962_p2}、imo_1964_p2、imo_1983_p6) を証明します。
コミュニティに利益をもたらすために、30,000 個の合成インスタンスのデータセットをオープンソース化します。各インスタンスには、自然言語による元の質問、自動形式化によって変換されたステートメント、および HunyuanProver による証明が含まれています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google