Pith. sign in

REVIEW 2 major objections 3 minor 42 references

A language model can be post-trained to coordinate exact symbolic tools and find verified sum-of-squares certificates: the full system succeeds on 78.96% of held-out synthetic problems, versus 44.73% when the same base model is given the sa

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-04 00:42 UTC pith:NVRAO7N6

load-bearing objection A solid, honestly scoped controlled case study of tool-coordination training for SOS certificates, with a credible exact-verified headline result but an aggregate metric that doesn't yet isolate the coordination claim. the 2 major comments →

arxiv 2608.00326 v1 pith:NVRAO7N6 submitted 2026-07-31 cs.AI

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

Bohan Chen , Shivam N. Patel , Richard Hoffmann , Sam Looi , Tony Yue Yu This is my paper
classification cs.AI
keywords weighted sum-of-squares certificatesLLM tool callingsymbolic computation agentsverifier feedbackGRPOsynthetic curriculumpolynomial nonnegativityexact verification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper argues that giving a language model exact symbolic tools is not enough: the agent must also learn which operations to request, in what order, and when to stop. The authors make this concrete with weighted sum-of-squares (SOS) decomposition, a certificate of the form f = sum_j c_j p_j^2 with positive rational weights, where checking a candidate is exact polynomial expansion but finding one requires strategic regrouping and multi-step search. They build a 1.35-million-example synthetic curriculum over nine polynomial tasks, first fine-tune on direct algebra and simulated symbolic traces, then optimize the policy with verifier-grounded reinforcement learning (GRPO). On held-out same-generator problems, the complete system reaches 78.96% verified SOS success versus 44.73% for the same base model given the same native tools, and 91.75% macro accuracy across the nine tasks. The authors stress that this is a complete-system comparison and that success measures certificate-search yield inside a controlled environment, not natural-problem generalization.

Core claim

The central claim is that a tool-using language model performs exact multi-step symbolic search far better when post-trained on the underlying algebra and optimized against an exact verifier than when the same tools are simply added to the base model. Concretely, the full configuration verifies 78.96% of held-out weighted-SOS instances, versus 44.73% for the base model with the same four native functions. Acceptance requires positive rational weights, polynomial squares, and exact coefficient-by-coefficient equality after expansion, so every counted success is a checked identity. The authors frame the object of study as tool coordination: exact operations do not eliminate errors in choosing,

What carries the argument

The load-bearing object is the exact terminal verifier: a candidate is accepted only if it parses as sum_j c_j p_j^2 with positive rational c_j, each p_j a polynomial, and expand(f - sum) is identically zero, making every accepted certificate a machine-checkable proof of nonnegativity. Around this verifier, the training recipe combines a nine-task synthetic curriculum (four local operations, four structural-algebra tasks, weighted SOS), supervised fine-tuning on direct algebra and simulated symbolic traces, and GRPO with rewards computed from exact algebraic contracts rather than string matches. At evaluation, the agent drives four native symbolic functions—expand, collect, reorder, factoriz

Load-bearing premise

The claim's load-bearing premise is that success on same-generator synthetic polynomials (1–3 variables, degrees 2/4/6, weights 1–10, m≤5) measures learned tool coordination rather than exploitation of generator regularities, especially that every input is SOS by construction and m=1 instances are perfect squares.

What would settle it

Stratify the reported 78.96% by the hidden number of squares m: if verified success is near 100% on m=1 and drops sharply for m=4–5, or if retraining on an out-of-generator sampler (more variables, degree 8, non-SOS distractors) makes the Full-minus-Base+Tools gap collapse, the coordination claim is an artifact of the generator.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • The full system's 78.96% verified SOS success, against 44.73% for the base model with the same tools, supports the claim that algebraic post-training complements interface access rather than substituting for it.
  • Full is best on all eight direct tasks (93.35% macro), so the trained checkpoint carries the algebraic skills even when native tools are disabled.
  • The gap over SFT grows from 12–18 points on local/structural tasks to 27 points on weighted SOS, consistent with the claim that the hardest part is global search and stopping, not single operations.
  • Exact verification separates failures into abstention, structural invalidity, and identity mismatch; because only the exact identity counts, the reported rate is a search-yield measure, not a recognition or syntax score.
  • Retention checks show no obvious loss on general-mathematics problems in a single 16-sample pass, though the authors explicitly label these as retention evidence, not transfer.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the result holds up, it implies tool-use evaluation should report the terminal state reached (the verified certificate) alongside call validity, since a schema-valid call can still be part of a failed search.
  • A natural stress test the paper does not run is stratifying success by hidden generator difficulty—number of squares m, degree, variable count; a concentration of failures at high m would indicate the coordination advantage is partly an easy-instance artifact.
  • The recipe may transfer to other domains with cheap exact verifiers—such as term rewriting, equality saturation, or proof-assistant checkable obligations—because the core idea is to train on subtasks whose outputs are exactly checkable before RL on the composite task.
  • Since every evaluation input is SOS by construction, the system is never asked to distinguish SOS from non-SOS; an out-of-distribution control with non-SOS polynomials would clarify whether the model learns to search or to exploit guaranteed solvability.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 3 minor

Summary. The paper proposes a controlled synthetic environment in which an LLM agent must produce verified weighted sum-of-squares (SOS) certificates for polynomials. The pipeline begins with Phi-4-reasoning-plus, applies QLoRA SFT on 1.35M synthetic examples covering eight supporting algebraic tasks plus weighted SOS, and then applies GRPO with task-specific symbolic rewards. At evaluation, two of the four configurations receive a native four-function SymPy interface for SOS search, and every terminal certificate is checked by exact expansion and coefficient comparison. On 10,000 held-out, same-generator test polynomials, the full SFT+GRPO+tools system reaches 78.96% verified success, compared with 44.73% for the base model with the same tools; the eight-task direct macro-accuracy is 93.35%. The paper explicitly scopes the evidence to same-generator synthetic problems, one backbone, and one run per training stage, and distinguishes checkpoint-level ability from complete-system certificate search.

Significance. If the empirical claims are taken at face value, this is a useful, carefully instrumented case study of tool coordination for exactly checkable algebraic outputs. The main strengths are: (i) the terminal verifier is exact, so all accepted certificates are correct; (ii) the paper cleanly separates checkpoint-level competence from complete-system search; (iii) the training–deployment mismatch (no native tool calls during training, native calls at test time) is explicitly documented; and (iv) the authors are unusually candid about the scope and about what the four-configuration design can and cannot identify. The result is not a claim of state-of-the-art inequality proving, but rather a controlled benchmark for studying sequential symbolic-tool use. The central quantitative claim is credible as a measurement on this synthetic benchmark, but the paper has not yet supplied the per-stratum analysis needed to support the qualitative claim that the learned system is specifically coordinating multi-step symbolic search rather than exploiting easy generator strata.

major comments (2)
  1. [Experiments, Table 6; Appendix Table A2] The headline weighted-SOS success is a single average over a generator with m uniform in {1,...,5}, degree in {2,4,6}, and variables in {1,2,3}. Since every test polynomial is SOS by construction and m=1 is exactly a single square f = c·q^2, the aggregate cannot distinguish learned multi-step coordination from success on easy strata. Please report verified success for Full and Base+Tools stratified by m, degree, and number of variables, and ideally the mean number of native calls per stratum. Without such a breakdown, the Introduction's 'coordination' narrative — regroup, revise, retry — is not established for the cases that motivate the environment.
  2. [Verifier-grounded GRPO and Appendix Eqs. (A20)–(A21)] Eq. (A21) defines the trajectory-shaping reward R_tool in terms of N_schema, N_exec, N_repeat, and T, which are properties of native tool-call trajectories. However, Table 3 and the deployment section state that GRPO optimizes chat-template responses with no native calls. The paper does not specify where R_tool is evaluated during training. If it is applied to simulated traces, the trace format and the exact computation of these counts must be described; if it is not part of GRPO, the reward definition should be corrected or moved. This matters because the GRPO reward is a central component of the proposed recipe and the reader must be able to reproduce the training signal.
minor comments (3)
  1. [Table 6] The nine-task macro combines checkpoint-level direct-task accuracies with a system-level SOS success rate. The text does acknowledge this heterogeneity, but the table caption should repeat the caveat to prevent misreading the number as a uniform checkpoint metric.
  2. [Experiments, 'Verification separates search from proof'] The paper reports that successful Full episodes use 3.8 native calls on average. Reporting the distribution of call counts, and the call counts of failed episodes, would strengthen the coordination narrative and help the reader judge where search difficulty lies.
  3. [Throughout] There are a few transcription/formatting artifacts in the text (e.g., 'macro- average' and 'on90,000separately generated' lack spacing). These should be cleaned up in the camera-ready version.

Circularity Check

0 steps flagged

No circularity: the central claims are empirical measurements on separately held-out, same-generator test instances, checked by an exact verifier that is independent of the trained model.

full rationale

The paper makes no derivation that reduces to its inputs. Weighted-SOS instances are generated backward from a hidden valid certificate (Eq. A4), but the evaluation accepts any certificate satisfying the exact coefficient identity, and the test set is separately generated with a different seed (the appendix states: “Training and evaluation generation use seeds 42 and 2025, respectively”). Success rates therefore measure certificate-search yield, not reconstruction of the generator’s hidden decomposition. The reward functions (Eqs. A10, A20) use the same algebraic contracts as evaluation, but this is standard training/evaluation alignment, not circular reasoning: the terminal verifier is an external, deterministic check of the mathematical state, not a fitted parameter. The same-generator scope is explicitly acknowledged by the paper (“the suite measures competence within the designed algebraic environment rather than natural-problem or out-of-distribution generalization”), which limits external validity but does not make the measurement circular. No self-citations are load-bearing; no uniqueness theorem or ansatz is smuggled in via citation. The comparison across Base, SFT, Base+Tools, and Full is a controlled empirical comparison, and the paper honestly states which causal effects are outside its design. Therefore no significant circularity is present.

Axiom & Free-Parameter Ledger

7 free parameters · 5 axioms · 0 invented entities

The central claim is an empirical measurement typical of ML benchmarks: the 'free parameters' are hand-chosen hyperparameters and generator ranges that define the benchmark distribution. No new mathematical or physical entities are introduced; the background facts about SOS certificates and exact symbolic computation are standard.

free parameters (7)
  • Reward blend weight (format vs task score) = 0.1 / 0.9
    Hand-chosen in Eq. (2)/(A10); weights the format gate against the exact task score in GRPO.
  • Trajectory shaping reward coefficients = 0.05, 0.05, -0.2, -0.01, +1.0
    Hand-chosen in Eq. (A21); reward schema-valid calls, executed calls, penalize repeats and long trajectories, and grant a large verified increment.
  • Residual-score temperature lambda = 10
    Hand-chosen in Eq. (A11); sharpens the exponential residual reward for quotient/remainder, xgcd, and SOS.
  • Per-task reward sub-weights = e.g., 0.3/0.7, 0.4/0.6, 0.5/0.5 in Eqs. (A12)-(A20)
    Hand-chosen balances between exact equality and format/structure checks across the nine tasks.
  • Generator ranges (variables, terms, coefficients, weights, m, degrees) = 1-3 vars, 1-5 terms, a in [-10,10], c in 1..10, m in 1..5, degrees per Table A2
    These define the synthetic distribution; the reported success rates are specific to them.
  • GRPO batch and sampling = batch 64, 8 generations/prompt, temp 0.9, top-p 0.95
    Hand-chosen; affect policy optimization and thus outcomes.
  • Budgets (calls, attempts, seconds) = 10 calls, 3 attempts, 5s/call, 60s/episode
    Hand-chosen; constrain the search horizon and influence success rate.
axioms (5)
  • standard math A weighted sum of polynomial squares with positive rational weights certifies global nonnegativity on R^n.
    Invoked in the acceptance contract (Eq. (1)) and throughout.
  • domain assumption SymPy's expand, collect, reorder, and factorize are exact and correct for polynomials over Q[x] within the supported ranges.
    The harness executes these tools and the verifier relies on their output (Table A4).
  • standard math The exact coefficient comparison in the terminal verifier decides polynomial equality correctly.
    All certificates are accepted/rejected based on this comparison; a bug would invalidate the metric.
  • domain assumption The synthetic generators and the train/eval seed split (42 vs 2025) produce disjoint datasets.
    Held-out evaluation is only valid if train and test instances do not overlap.
  • domain assumption Phi-4-reasoning-plus and the training stack (QLoRA, Axolotl, GRPO) behave as documented.
    The reported checkpoints are assumed to have been produced by the described procedures.

pith-pipeline@v1.3.0-alltime-deepseek · 17011 in / 14830 out tokens · 125317 ms · 2026-08-04T00:42:53.427590+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2608.00326 by Bohan Chen, Richard Hoffmann, Sam Looi, Shivam N. Patel, Tony Yue Yu.

Figure 1
Figure 1. Figure 1: Overview of the controlled study. Algebraic post-training builds a checkpoint from eight supporting tasks and [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustrative coordination example, not a model trajectory. Exact factorization verifies a proposed group, but the search [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

42 extracted references · 6 linked inside Pith

  1. [1]

    Abdin, M.; Agarwal, S.; Awadallah, A.; Balachandran, V.; Behl, H.; et al. 2025. Phi-4-reasoning Technical Report. arXiv:2504.21318

    Pith/arXiv arXiv 2025

  2. [2]

    AI-MO . 2024. AIMO Validation AIME . Hugging Face dataset. 90 problems from AIME 2022, 2023, and 2024

    2024

  3. [3]

    Chen, W.; Ma, X.; Wang, X.; and Cohen, W. W. 2023. Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks. Transactions on Machine Learning Research

    2023

  4. [4]

    Cobbe, K.; Kosaraju, V.; Bavarian, M.; Chen, M.; Jun, H.; et al. 2021. Training Verifiers to Solve Math Word Problems. arXiv:2110.14168

    Pith/arXiv arXiv 2021

  5. [5]

    Dettmers, T.; Pagnoni, A.; Holtzman, A.; and Zettlemoyer, L. 2023. QLoRA : Efficient Finetuning of Quantized LLMs . In Advances in Neural Information Processing Systems, volume 36

    2023

  6. [6]

    Fawzi, A.; Malinowski, M.; Fawzi, H.; and Fawzi, O. 2019. Learning Dynamic Polynomial Proofs. In Advances in Neural Information Processing Systems, volume 32

    2019

  7. [7]

    Feng, J.; Huang, S.; Qu, X.; Zhang, G.; Qin, Y.; Zhong, B.; Jiang, C.; Chi, J.; and Zhong, W. 2026. ReTool : Reinforcement Learning for Strategic Tool Use in LLMs . In International Conference on Learning Representations

    2026

  8. [8]

    Gao, L.; Madaan, A.; Zhou, S.; Alon, U.; Liu, P.; Yang, Y.; Callan, J.; and Neubig, G. 2023. PAL : Program-Aided Language Models. In Proceedings of the 40th International Conference on Machine Learning, 10764--10799

    2023

  9. [9]

    Gou, Z.; Shao, Z.; Gong, Y.; Shen, Y.; Yang, Y.; Duan, N.; and Chen, W. 2024 a . CRITIC : Large Language Models Can Self-Correct with Tool-Interactive Critiquing. In International Conference on Learning Representations

    2024

  10. [10]

    Gou, Z.; Shao, Z.; Gong, Y.; Shen, Y.; Yang, Y.; Huang, M.; Duan, N.; and Chen, W. 2024 b . ToRA : A Tool-Integrated Reasoning Agent for Mathematical Problem Solving. In International Conference on Learning Representations

    2024

  11. [11]

    Z.; Z u z i\'c, G.; et al

    Hubert, T.; Mehta, R.; Sartran, L.; Horv \'a th, M. Z.; Z u z i\'c, G.; et al. 2026. Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning. Nature, 651: 607--613

    2026

  12. [12]

    Laban, P.; Hayashi, H.; Zhou, Y.; and Neville, J. 2026. LLMs Get Lost in Multi-Turn Conversation. In International Conference on Learning Representations

    2026

  13. [13]

    Lasserre, J. B. 2001. Global Optimization with Polynomials and the Problem of Moments. SIAM Journal on Optimization, 11(3): 796--817

    2001

  14. [14]

    Li, M.; Zhao, Y.; Yu, B.; Song, F.; Li, H.; Yu, H.; Li, Z.; Huang, F.; and Li, Y. 2023. API -Bank: A Comprehensive Benchmark for Tool-Augmented LLMs . In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 3102--3116. Singapore: Association for Computational Linguistics

    2023

  15. [15]

    Li, Z.; Li, Z.; Tang, W.; Zhang, X.; Yao, Y.; Si, X.; Yang, F.; Yang, K.; and Ma, X. 2025. Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning. In International Conference on Learning Representations

    2025

  16. [16]

    Li, Z.; Liao, B.; and Ye, Q. 2025. IneqSearch : Hybrid Reasoning for Olympiad Inequality Proofs. In Advances in Neural Information Processing Systems, volume 38

    2025

  17. [17]

    Lightman, H.; Kosaraju, V.; Burda, Y.; Edwards, H.; Baker, B.; Lee, T.; Leike, J.; Schulman, J.; Sutskever, I.; and Cobbe, K. 2024. Let's Verify Step by Step. In International Conference on Learning Representations

    2024

  18. [18]

    Liu, B.; Qi, N.; Zeng, X.; Dehbi, L.; and Yang, Z. 2025. Automated Proof of Polynomial Inequalities via Reinforcement Learning. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, 5052--5060

    2025

  19. [19]

    Lv, K.; Dong, Y.; Han, R.; Jia, F.; Ma, F.; and Zhang, J. 2026. LLM -Guided Quantified SMT Solving over Uninterpreted Functions. Proceedings of the AAAI Conference on Artificial Intelligence, 40(17): 14304--14312

    2026

  20. [20]

    P.; Paprocki, M.; C ert \'i k, O.; Kirpichev, S

    Meurer, A.; Smith, C. P.; Paprocki, M.; C ert \'i k, O.; Kirpichev, S. B.; Rocklin, M.; Kumar, A.; Ivanov, S.; Moore, J. K.; Singh, S.; et al. 2017. SymPy : Symbolic Computing in Python. PeerJ Computer Science, 3: e103

    2017

  21. [21]

    Mirzadeh, I.; Alizadeh-Vahid, K.; Shahrokhi, H.; Tuzel, O.; Bengio, S.; and Farajtabar, M. 2025. GSM -Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models. In International Conference on Learning Representations

    2025

  22. [22]

    Parrilo, P. A. 2003. Semidefinite Programming Relaxations for Semialgebraic Problems. Mathematical Programming, 96(2): 293--320

    2003

  23. [23]

    G.; Mao, H.; Yan, F.; Ji, C

    Patil, S. G.; Mao, H.; Yan, F.; Ji, C. C.-J.; Suresh, V.; Stoica, I.; and Gonzalez, J. E. 2025. The Berkeley Function Calling Leaderboard ( BFCL ): From Tool Use to Agentic Evaluation of Large Language Models. In Proceedings of the 42nd International Conference on Machine Learning, volume 267 of Proceedings of Machine Learning Research, 48371--48392. PMLR

    2025

  24. [24]

    Pelleriti, N.; Spiegel, C.; Liu, S.; Mart \'i nez-Rubio, D.; Zimmer, M.; and Pokutta, S. 2026. Neural Sum-of-Squares: Certifying the Nonnegativity of Polynomials with Transformers. In International Conference on Learning Representations

    2026

  25. [25]

    Putinar, M. 1993. Positive Polynomials on Compact Semi-Algebraic Sets. Indiana University Mathematics Journal, 42(3): 969--984

    1993

  26. [26]

    Qin, Y.; Liang, S.; Ye, Y.; Zhu, K.; Yan, L.; et al. 2024. ToolLLM : Facilitating Large Language Models to Master 16000+ Real-World APIs . In International Conference on Learning Representations

    2024

  27. [27]

    F.; Hulak, D

    Ramos, A. F.; Hulak, D. B.; and Barretto de Queiroz, R. J. G. 2026. Formal Verification of an Explicit Counterexample to the Jacobian Conjecture. Archive of Formal Proofs

    2026

  28. [28]

    Z.; Shao, Z.; Song, J.; Xin, H.; Wang, H.; et al

    Ren, Z. Z.; Shao, Z.; Song, J.; Xin, H.; Wang, H.; et al. 2025. DeepSeek-Prover-V2 : Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv:2504.21801

    Pith/arXiv arXiv 2025

  29. [29]

    Schick, T.; Dwivedi-Yu, J.; Dess \`i , R.; Raileanu, R.; Lomeli, M.; Hambro, E.; Zettlemoyer, L.; Cancedda, N.; and Scialom, T. 2023. Toolformer: Language Models Can Teach Themselves to Use Tools. In Advances in Neural Information Processing Systems, volume 36

    2023

  30. [30]

    Schm \"u dgen, K. 1991. The K -Moment Problem for Compact Semi-Algebraic Sets. Mathematische Annalen, 289(2): 203--206

    1991

  31. [31]

    Shao, Z.; Wang, P.; Zhu, Q.; Xu, R.; Song, J.; et al. 2024. DeepSeekMath : Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv:2402.03300

    Pith/arXiv arXiv 2024

  32. [32]

    I.; Alizadeh, K.; Horton, M.; Bengio, S.; and Farajtabar, M

    Shojaee, P.; Mirzadeh, S. I.; Alizadeh, K.; Horton, M.; Bengio, S.; and Farajtabar, M. 2025. The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity. In The Thirty-ninth Annual Conference on Neural Information Processing Systems

    2025

  33. [33]

    Stengle, G. 1974. A Nullstellensatz and a Positivstellensatz in Semialgebraic Geometry. Mathematische Annalen, 207: 87--97

    1974

  34. [34]

    Tao, T. 2026. A Digestion of the Jacobian Conjecture Counterexample. What's New

    2026

  35. [35]

    Wang, X.; Wang, Z.; Liu, J.; Chen, Y.; Yuan, L.; Peng, H.; and Ji, H. 2024. MINT : Evaluating LLMs in Multi-Turn Interaction with Tools and Language Feedback. In International Conference on Learning Representations

    2024

  36. [36]

    Wei, C.; Sun, M.; and Wang, W. 2024. Proving Olympiad Algebraic Inequalities without Human Demonstrations. In Advances in Neural Information Processing Systems, volume 37, 82811--82822

    2024

  37. [37]

    Z.; Song, J.; Shao, Z.; Zhao, W.; et al

    Xin, H.; Ren, Z. Z.; Song, J.; Shao, Z.; Zhao, W.; et al. 2025. DeepSeek-Prover-V1.5 : Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. In International Conference on Learning Representations

    2025

  38. [38]

    Yang, J.; Prabhakar, A.; Narasimhan, K.; and Yao, S. 2023 a . InterCode: Standardizing and Benchmarking Interactive Coding with Execution Feedback. arXiv:2306.14898

    Pith/arXiv arXiv 2023

  39. [39]

    M.; Gu, A.; Chalamala, R.; Song, P.; Yu, S.; Godil, S.; Prenger, R

    Yang, K.; Swope, A. M.; Gu, A.; Chalamala, R.; Song, P.; Yu, S.; Godil, S.; Prenger, R. J.; and Anandkumar, A. 2023 b . LeanDojo : Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems, volume 36

    2023

  40. [40]

    Yao, S.; Shinn, N.; Razavi, P.; and Narasimhan, K. 2025. -bench: A Benchmark for Tool-Agent-User Interaction in Real-World Domains. In International Conference on Learning Representations

    2025

  41. [41]

    Yao, S.; Zhao, J.; Yu, D.; Du, N.; Shafran, I.; Narasimhan, K.; and Cao, Y. 2023. ReAct : Synergizing Reasoning and Acting in Language Models. In International Conference on Learning Representations

    2023

  42. [42]

    Zuo, R.; Zhao, H.; He, G.; Yang, Z.; and Wang, J. 2026. From LLM -Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates. Accepted to ICML 2026, arXiv:2605.15445

    Pith/arXiv arXiv 2026