定理推理解释器作为合成数据生成的裁判
Theorem Prover as a Judge for Synthetic Data Generation
AI总结：
本研究提出TP-as-a-Judge和RLTPF方法，通过定理推理解释器提升LLM的合成数据生成与推理准确性。
摘要：
数学推理中合成数据的需求增加，因其能够提升大语言模型（LLMs）的数学能力。然而，确保中间推理步骤的有效性仍然是一个重大挑战，影响数据质量。虽然通过定理推理解释器进行形式验证可以有效验证LLM推理，但数学证明的自动形式化仍然容易出错。为此，我们引入了迭代自动形式化方法，通过迭代优化定理推理解释器的形式化来减少错误，从而将Lean推理解释器的执行率从60%提升到87%。在此基础上，我们提出了定理推理解释器作为裁判（TP-as-a-Judge）方法，该方法利用定理推理解释器的形式化来严格评估LLM的中间推理，有效将自动形式化与合成数据生成相结合。最后，我们提出了从定理推理解释器反馈中学习（RLTPF）框架，该框架在强化学习从人类反馈（RLHF）中用定理推理解释器反馈取代人工标注。在多个LLM上，应用TP-as-a-Judge和RLTPF仅需3508个样本，就实现了在MultiArith上Mistral-7B的5.56%准确率提升，在SVAMP上Llama-2-7B的6.00%提升，在AQUA上Llama-3.1-8B的3.55%提升。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
