Theorem Prover as a Judge for Synthetic Data Generation

要約

数学的推論における合成データの需要は、大規模な言語モデル（LLM）の数学的能力を高める可能性のために増加しています。
ただし、中間推論ステップの妥当性を確保することは、データの品質に影響を与える重要な課題のままです。
定理賞を介した正式な検証はLLMの推論を効果的に検証しますが、数学的証明の自動体系化はエラーが発生しやすいままです。
これに応じて、反復的なオートフォーマル化は、エラーを緩和するための定理プロバーの形式化を繰り返し改善するアプローチを導入し、それによりリーンプロバーの実行率が60％から87％に増加します。
その上に構築すると、定理を裁判官（TP-As-a-judge）として紹介します。これは、定理プーバーの正式化を採用してLLM中間推論を厳密に評価し、合成データ生成と自己形態化を効果的に統合する方法です。
最後に、人間の注釈を人間のフィードバック（RLHF）からの補強学習における定理プローバーフィードバックに置き換えるフレームワークである定理プローバーフィードバック（RLTPF）からの強化学習を提示します。
複数のLLMにわたって、TP-AS-A-A-A-JudgeとRLTPFを適用すると、3,508サンプルのみでベンチマークが向上し、Mistral-7Bで5.56％の精度増加を達成し、SVAMPでLlama-2-7Bで6.00％、Llama-on 3.55％を達成しました。
Aquaの3.1-8b。

要約(オリジナル)

The demand for synthetic data in mathematical reasoning has increased due to its potential to enhance the mathematical capabilities of large language models (LLMs). However, ensuring the validity of intermediate reasoning steps remains a significant challenge, affecting data quality. While formal verification via theorem provers effectively validates LLM reasoning, the autoformalisation of mathematical proofs remains error-prone. In response, we introduce iterative autoformalisation, an approach that iteratively refines theorem prover formalisation to mitigate errors, thereby increasing the execution rate on the Lean prover from 60% to 87%. Building upon that, we introduce Theorem Prover as a Judge (TP-as-a-Judge), a method that employs theorem prover formalisation to rigorously assess LLM intermediate reasoning, effectively integrating autoformalisation with synthetic data generation. Finally, we present Reinforcement Learning from Theorem Prover Feedback (RLTPF), a framework that replaces human annotation with theorem prover feedback in Reinforcement Learning from Human Feedback (RLHF). Across multiple LLMs, applying TP-as-a-Judge and RLTPF improves benchmarks with only 3,508 samples, achieving 5.56% accuracy gain on Mistral-7B for MultiArith, 6.00% on Llama-2-7B for SVAMP, and 3.55% on Llama-3.1-8B for AQUA.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google