用Transformer模型指导符号积分步骤搜索，实现正确可构造的自动积分。
AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs
- 用GPT风格模型学习积分规则选择策略，结合符号求解器逐步推理。
- 在合成数据上训练后，准确率与效率均优于数据生成器，搜索步数减少50%。
- 提出首个分步积分数据集，适合需要符号推理的AI数学研究者。
我们提出了首个基于学习的、正确可构造的分步数学积分系统。核心思想是训练一个由GPT式Transformer模型表示的策略，引导符号求解器寻找正确的积分规则。具体而言，我们设计了一个具有公理正确性的符号引擎，以及首个分步积分数据集。该模型在合成数据上训练后，展现出强泛化能力：其准确率和效率均超过自身数据生成器，在搜索步数上减少50%。实验还表明，仅对SOTA LLM进行问答对微调无法有效解决此类数学任务，凸显了将大模型与符号推理引擎结合的新方法的重要性，本工作即为此类探索的实例。
原文摘要 · Abstract (English)
We present the first correct-by-construction learning-based system for step-by-step mathematical integration. The key idea is to learn a policy, represented by a GPT transformer model, which guides the search for the right mathematical integration rule, to be carried out by a symbolic solver. Concretely, we introduce a symbolic engine with axiomatically correct actions on mathematical expressions, as well as the first dataset for step-by-step integration. Our GPT-style transformer model, trained on this synthetic data, demonstrates strong generalization by surpassing its own data generator in accuracy and efficiency, using 50% fewer search steps. Our experimental results with SoTA LLMs also demonstrate that the standard approach of fine-tuning LLMs on a set of question-answer pairs is insufficient for solving this mathematical task. This motivates the importance of discovering creative methods for combining LLMs with symbolic reasoning engines, of which our work is an instance.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。