Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

要約

大規模な言語モデル（LLMS）は、証明システム内で証明ステップ（\ textit {a.k.a。}戦術）を生成することにより、数学的定理を正式に証明できます。
ただし、可能な戦術のスペースは広大で複雑ですが、正式な証明のための利用可能なトレーニングデータは限られており、LLMベースの戦術生成に大きな課題を抱えています。
これに対処するために、象徴的な方法によってエンコードされたドメイン固有の洞察を使用して、LLMSによって学習された数学的直観を相乗化するニューロシンボリック戦術ジェネレーターを紹介します。
この統合の重要な側面は、数学的推論のどの部分がLLMSに最適であり、どの部分に象徴的な方法に適しているかを特定することです。
この論文では、神経 – 神経系統合の高レベルのアイデアはさまざまな数学的問題に広く適用されますが、特にオリンピックの不平等に焦点を当てています（図〜1）。
人間がこれらの問題を解決する方法を分析し、技術を2種類の戦術に蒸留する方法を分析します。（1）象徴的な方法で処理されるスケーリング、（2）LLMSによって処理される書き換え。
さらに、シンボリックツールとLLMSを組み合わせて、効率的な証明検索の証明目標を剪定してランク付けします。
複数の数学競争からの161の挑戦的な不平等に関するフレームワークを評価し、最先端のパフォーマンスを達成し、追加のトレーニングデータを必要とせずに既存のLLMと象徴的なアプローチを大幅に上回ります。

要約(オリジナル)

Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tactics is vast and complex, while the available training data for formal proofs is limited, posing a significant challenge to LLM-based tactic generation. To address this, we introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods. The key aspect of this integration is identifying which parts of mathematical reasoning are best suited to LLMs and which to symbolic methods. While the high-level idea of neuro-symbolic integration is broadly applicable to various mathematical problems, in this paper, we focus specifically on Olympiad inequalities (Figure~1). We analyze how humans solve these problems and distill the techniques into two types of tactics: (1) scaling, handled by symbolic methods, and (2) rewriting, handled by LLMs. In addition, we combine symbolic tools with LLMs to prune and rank the proof goals for efficient proof search. We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions, achieving state-of-the-art performance and significantly outperforming existing LLM and symbolic approaches without requiring additional training data.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google