学习协调符号工具：LLM Agent生成可验证的平方和证书

工具调用允许大语言模型（LLMs）在解决问题过程中调用外部计算，这是在人工智能领域（特别是数学）中各种应用中一个有用的特性。我们通过权重和平方和（SOS）分解来研究这一场景，这是一种机器可验证的证明多项式非负性的方法，因此可以证明多项式不等式。候选的分解可以被精确检查，但找到一个需要选择非唯一的分组和协调多个符号变换。我们开发了一个代理，它结合了代数任务训练、符号工具和验证反馈优化，用于这个任务。而不是只在复合的SOS任务上训练，我们构建了1.35百万个合成示例，涵盖八个支持的多项式任务和权重SOS分解。我们首先使用监督微调（SFT）直接处理代数问题和模拟符号轨迹，然后使用任务特定的符号奖励进行Group Relative Policy Optimization（GRPO）。SFT数据集没有原始工具调用消息；在评估时，代理使用SymPy调用来展开、收集、重新排序和因式分解。最终的SOS答案被精确展开和系数比较所检查。在保留的合成问题上，全SFT+GRPO+工具系统在四个评估配置中表现最强，达到78.96%的验证成功，而使用相同工具的基模型为44.73%，在九个多项式任务上达到91.75%的宏观准确率。在这一控制的设置下，我们的工作提供了一个结合领域特定技能训练、可执行工具和验证反馈的案例研究，可能为其他具有可验证输出的领域提供工具调用代理的设计灵感。