学习协调符号工具：用于验证平方和（SOS）证书的大语言模型（LLM）智能体
Learning to Coordinate Symbolic Tools: LLM Agents for Verified Sum-of-Squares Certificates
浏览论文内容
中文总结 AI 辅助
该研究开发结合领域训练、符号工具和验证反馈的LLM智能体，在加权SOS验证任务上达到78.96%成功率，为可精确检查输出领域的工具调用智能体设计提供案例。
中文摘要 AI 辅助
工具调用使大语言模型（LLM）在解决问题时能调用外部计算，这一能力在包括数学AI在内的多个领域十分有用。我们通过加权平方和（SOS）分解研究这一设置，这是一种可由机器检查的、用于证明多项式非负性及多项式不等式的途径。候选分解可被精确检查，但寻找候选分解需要在非唯一的重组中做出选择，并协调多种符号变换。我们开发了一种智能体，它结合代数任务训练、符号工具及基于验证器的优化来完成该任务。我们不仅在复合SOS任务上训练，还构建了135万个合成示例，涵盖8种辅助多项式任务及加权SOS分解。我们首先应用监督微调（SFT）来指导代数问题和模拟符号轨迹，随后使用带有特定任务符号奖励的分组相对策略优化（GRPO）。SFT语料库不含原生工具调用消息；在评估时，该智能体使用原生SymPy调用进行展开、合并、重排序和因式分解。每个最终SOS答案都通过精确展开和系数比较进行检查。在保留的、同一生成器的合成问题上，完整的SFT+GRPO+工具系统是四种评估配置中最强的，在加权SOS上达到78.96%的验证成功率，而使用相同工具的基础模型为44.73%；在9项多项式任务上的宏观准确率为91.75%。在这一受控环境中，我们的工作提供了一个结合领域特定技能训练、可执行工具及验证器反馈的案例研究，可能为其他具有可精确检查输出的领域的工具调用智能体设计提供参考。
英文摘要
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.
