让大模型学会调用符号工具，自动证明多项式不等式并验证结果。
Learning to Coordinate Symbolic Tools: LLM Agents for Verified Sum-of-Squares Certificates
- 通过合成数据训练模型掌握多项式重组与符号变换技能。
- 在可控测试中实现78.96%的可验证成功率达基线两倍以上。
- 适合研究数学自动证明或工具调用智能体的开发者参考。
工具调用使大语言模型在求解过程中调用外部计算，这一能力在数学人工智能等领域具有价值。本文以加权和平方（SOS）分解为研究场景，这是一种可机器验证的多项式非负性证明方法。候选分解可精确验证，但寻找有效分解需在非唯一分组中选择并协调多个符号变换。我们构建了一个结合代数任务训练、符号工具与验证器反馈优化的智能体。通过生成135万条合成数据，覆盖八项支持性多项式任务及加权SOS分解。先进行监督微调（SFT），使用代数问题和模拟符号追踪；再采用分组相对策略优化（GRPO），引入任务特定符号奖励。SFT语料中无原生工具调用指令；评估时，智能体原生调用SymPy执行展开、合并、重排与因式分解。所有最终答案均通过精确展开与系数对比验证。在同源生成的保留测试集上，完整系统（SFT+GRPO+工具）在加权SOS任务中达到78.96%可验证成功率，远超基础模型的44.73%，九项多项式任务总体准确率达91.75%。本工作展示了领域专用技能训练、可执行工具与验证反馈结合的有效性，可为其他具备精确可验证输出的领域提供智能体设计参考。
原文摘要 · Abstract (English)
Tool calling allows large language models (LLMs) to invoke external computation during problem solving, a useful capability in various fields including AI for mathematics. We study this setting through weighted sum-of-squares (SOS) decomposition, a machine-checkable route to proving polynomial nonnegativity and hence polynomial inequalities. A candidate decomposition can be checked exactly, but finding one requires choosing among non-unique regroupings and coordinating multiple symbolic transformations. We develop an agent that combines algebraic task training, symbolic tools, and verifier-grounded optimization for this task. Rather than training only on the composite SOS task, we construct 1.35 million synthetic examples covering eight supporting polynomial tasks together with weighted-SOS decomposition. We first apply supervised fine-tuning (SFT) to direct algebra problems and simulated symbolic traces, and then use Group Relative Policy Optimization (GRPO) with task-specific symbolic rewards. The SFT corpus contains no native tool-calling messages; at evaluation, the agent uses native SymPy calls for expansion, collection, reordering, and factorization. Every final SOS answer is checked by exact expansion and coefficient comparison. On held-out, same-generator synthetic problems, the full SFT+GRPO+tools system is the strongest of four evaluated configurations, reaching 78.96% verified success on weighted SOS, compared with 44.73% for the base model with the same tools, and 91.75% macro accuracy across nine polynomial tasks. Within this controlled setting, our work provides a case study of combining domain-specific skill training, executable tools, and verifier feedback, and may inform the design of tool-calling agents in other domains with exactly checkable outputs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。