TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models

要約

自動定理証明 (ATP) は、最近成功を収めた生成言語モデルの推論能力を調査するための魅力的な分野となっています。
ただし、現在の ATP ベンチマークは主に記号推論に焦点を当てており、複素数の組み合わせ推論の理解を必要とすることはほとんどありません。
この研究では、ATP ベンチマークである TRIGO を提案します。このベンチマークでは、段階的な証明で三角関数の式を簡略化するモデルを必要とするだけでなく、数式に関する生成 LM の推論能力と、操作、グループ化、因子数を操作する能力も評価します。
条項。
私たちは三角関数の式とその縮約形式を Web から収集し、簡略化プロセスに手動で注釈を付け、それをリーン形式言語システムに翻訳します。
次に、アノテーション付きサンプルから追加のサンプルを自動的に生成して、データセットを拡張します。
さらに、モデルの一般化能力を徹底的に分析するために、さまざまな難易度や分布のデータセット分割を作成するための Lean-Gym に基づく自動ジェネレーターを開発します。
私たちの広範な実験は、私たちが提案した TRIGO が、かなりの量のオープンソース形式定理証明言語データで事前トレーニングされた GPT-4 を含む高度な生成 LM に新たな課題を提起し、生成 LM の能力を研究するための新しいツールを提供することを示しています。
形式的推論と数学的推論の両方について。

要約(オリジナル)

Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchmarks mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM’s reasoning ability on formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model’s generalization ability. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM’s including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM’s ability on both formal and mathematical reasoning.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google