# Learning to Coordinate Symbolic Tools: LLM Agents for Verified Sum-of-Squares Certificates

arXiv: https://arxiv.org/abs/2608.00326 · HTML: https://mlsanity.com/paper/2608.00326/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 21 of its 38 references that are in the map.
- First posted on arXiv 31 Jul 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 21 of 21)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [QLoRA: Efficient Finetuning of Quantized LLMs](https://mlsanity.com/paper/2305.14314/) (2023)
- [ToolLLM: Facilitating Large Language Models to Master 16000+ Real-world APIs](https://mlsanity.com/paper/2307.16789/) (2023)
- [τ-bench: A Benchmark for Tool-Agent-User Interaction in Real-World Domains](https://mlsanity.com/paper/2406.12045/) (2024)
- [Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks](https://mlsanity.com/paper/2211.12588/) (2022)
- [CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing](https://mlsanity.com/paper/2305.11738/) (2023)
- [API-Bank: A Comprehensive Benchmark for Tool-Augmented LLMs](https://mlsanity.com/paper/2304.08244/) (2023)
- [LLMs Get Lost In Multi-Turn Conversation](https://mlsanity.com/paper/2505.06120/) (2025)
- [The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity](https://mlsanity.com/paper/2506.06941/) (2025)
- [MINT: Evaluating LLMs in Multi-turn Interaction with Tools and Language Feedback](https://mlsanity.com/paper/2309.10691/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [InterCode: Standardizing and Benchmarking Interactive Coding with Execution Feedback](https://mlsanity.com/paper/2306.14898/) (2023)
- [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://mlsanity.com/paper/2406.14219/) (2024)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [Learning dynamic polynomial proofs](https://mlsanity.com/paper/1906.01681/) (2019)
- [LLM-Guided Quantified SMT Solving over Uninterpreted Functions](https://mlsanity.com/paper/2601.04675/) (2026)
- [Neural Sum-of-Squares: Certifying the Nonnegativity of Polynomials with Transformers](https://mlsanity.com/paper/2510.13444/) (2025)
- [From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates](https://mlsanity.com/paper/2605.15445/) (2026)

## Abstract (arXiv)

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.