Pith. sign in

REVIEW 5 major objections 9 minor 2 cited by

Neuro-Symbolic Data Generation for Math Reasoning

T0 review · 5 major / 9 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read The paper claims that mutating math problems in a solver-checked symbolic space and translating them back to natural language generates training data that substantially improves LLM mathematical reasoning.

desk verdict A genuinely new data-generation recipe—mutating formal SMT-LIB problems and informalizing them—backs its claims with same-budget comparisons, but the formalization-fidelity gap and missing release mean the empirical story is conditional, not settled. read the letter →

arxiv 2412.04857 v1 pith:DFSMVLQW submitted 2024-12-06 cs.AI

Zenan Li , Zhi Zhou , Yuan Yao , Yu-Feng Li , Chun Cao , Fan Yang , Xian Zhang , Xiaoxing Ma This is my paper · ORCID
classification cs.AI
keywords mathematicalreasoningsyntheticdatagenerationneuro-symbolicAISMTsolverssymbolicmutationLLMfine-tuningGSM8KMATH
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper asks whether large language models' visible weakness in mathematical reasoning is intrinsic or a consequence of too little high-quality training data. To test this, it builds a data-generation pipeline that takes existing math word problems, formalizes them into SMT-LIB, mutates the formal statements using simplification and complication strategies with auxiliary variables, and uses SMT solvers plus projected Markov chain Monte Carlo to guarantee the mutated problems remain solvable and diverse. GPT-4 translates the formal mutations back into natural-language word problems, and the pipeline also produces solver-verified reasoning paths. The authors use the resulting 860K-problem dataset to fine-tune LLaMA-2 and Mistral models and report clear gains on GSM8K, MATH, and two out-of-domain benchmarks, including passing GPT-3.5-Turbo on GSM8K with a 7B model. The paper's own framing is that the diversity-validity tradeoff is the obstacle, and symbolic mutation with solver verification is the claimed way out.

What carries the argument

The load-bearing mechanism is a mutation operator that works inside a formal problem in SMT-LIB: each mutation introduces fresh auxiliary variables and random interpreted functions into the goal and constraints, then uses projected Markov chain Monte Carlo to sample diverse values for a subset of those variables while an SMT solver fills in the rest, guaranteeing the mutated formula remains satisfiable. Complication and simplification tactics (expression folding, Gaussian elimination, quantifier elimination, if-then-else elimination) let the pipeline control difficulty and produce levels from simple to multi-step. Informalization by GPT-4 converts each verified formal mutation into a word problem, and the paper checks consistency by having GPT-4 solve the word problem and comparing with the solver's answer.

What would settle it

Train a model on the same 860K prompts but with the mutation and verification steps replaced by unverified GPT-4 rephrasing; if the accuracy gains on GSM8K, MATH, SVAMP, and ASDiv shrink to noise, the claim that solver-verified symbolic mutation causes the improvement would survive, and if the gains are identical, the verification mechanism would be shown to be unnecessary.

Watch

Extended reading notes

Core claim

The paper's central claim is that the apparent shortage of mathematical reasoning in LLMs can be relieved by exposing them to large quantities of automatically generated, solver-verified mathematical problems, and that the right way to generate such data is to mutate problems in formal symbolic space rather than to rephrase them in natural language. The method formalizes seed problems from GSM8K and MATH into SMT-LIB, mutates the goal and constraints using random operations plus auxiliary variables, and relies on SMT solvers to maintain satisfiability. Diversity comes from sampling many solutions to the auxiliary variables via projected MCMC, and difficulty is controlled by combining complication and simplification tactics across levels. The experimental section reports that fine-tuned LLaMA-2-7B/13B and Mistral-7B models outperform four existing open-source math models on GSM8K and MATH, and that at equal data budgets the generated data beats MetaMathQA's bootstrapped data, with accuracy gains persisting as dataset size grows. The paper also interprets these results as evidence that the deficiency is substantially data-limited rather than inherent to the models.

Load-bearing premise

The load-bearing premise is that GPT-4's autoformalization of the original word problem is faithful enough that a solver-verified mutation of the formal formula is still a meaningful math word problem, since the solver never checks the natural-language meaning and the paper reports that a substantial share of MATH formalizations are inaccurate while still being used.

Editorial extensions

If this is right

  • If the central claim holds, then mathematical reasoning ability in LLMs is substantially data-limited, so additional solver-verified data should keep producing gains as generation scales.
  • At equal data budgets the generated data beats bootstrapped-rephrasing data, suggesting the quality of the symbolic mutation, not the number of tokens, is what carries the improvement.
  • Models trained on this data transfer to out-of-domain word-problem benchmarks (SVAMP, ASDiv) and to a dynamic benchmark (DyVal), indicating the improvement is not just memorization of a training distribution.
  • Open-source 7B models trained on these data can reach or exceed the reasoning accuracy of a much larger proprietary model on GSM8K, lowering the cost of strong math reasoning.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A direct ablation separating the solver-verified subset from the 80,000 unverified MATH problems would isolate how much of the score gain comes from verification rather than from GPT-4 rephrasing.
  • Because the consistency check uses GPT-4 answers as a proxy for semantic correctness, a stricter check using human-verified samples or a second independent solver could confirm the lower-bound claim about informalization accuracy.
  • The same symbolic-mutation idea could extend to other problem domains that admit formal encodings, such as physics or logic puzzles, where solvers or verifiers can certify the mutated task.
  • The paper's upward scalability curve suggests training-data generation could become a continuous, solver-guided process that improves as the base model improves, rather than a one-time dataset build.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 9 minor

Summary. The paper proposes a neuro-symbolic data-generation framework for mathematical reasoning. Seed problems from GSM8K and MATH are autoformalized into SMT-LIB; the formal problems are mutated through simplification and complication operators, with validity maintained by symbolic solvers and diversity sampled via projected MCMC; GPT-4 then informalizes the mutated formal problems back into natural-language word problems, and GPT-4-generated reasoning paths are checked against solver answers. The generated dataset (860K examples) is used to fine-tune LLaMA-2-7B/13B and Mistral-7B. The authors report improved accuracy over WizardMath, MuggleMATH, MAmmoTH, and MetaMath on GSM8K, MATH, SVAMP, and ASDiv, and same-budget comparisons against MetaMathQA in Table 3. The central claim is that symbolic mutation with solver verification produces diverse and valid data, and that this data, rather than raw volume, drives the gains.

Significance. If the main claims hold, the paper provides a practical method for generating large, verifiable math datasets and presents evidence that data quality can improve open-source models' math reasoning. The same-budget comparison in Table 3 is a sound experimental design, and the use of machine-checked solver verification for mutated formal problems is a genuine strength. However, the formalization-fidelity assumption and the unverified 80K MATH examples mean that the validity guarantee is not established for a substantial part of the dataset. The paper would be significantly strengthened by quantifying the impact of these subsets and by adding statistical error bars.

major comments (5)
  1. [Section 3 (Informalization)] The claim that the consistency rate is a lower bound on the true consistency rate relies on the unsupported assertion of 'zero false positive' in the observation that incorrectly informalized problems are almost never confirmed by symbolic solvers. A GPT-4 solution to an informalized problem can match a solver's answer even when the natural-language problem is inconsistent with the original seed, because the formal mutant itself may be derived from an inaccurate formalization. The paper should either provide evidence (e.g., human evaluation or a calibration study) that false positives are negligible, or weaken the lower-bound claim; this is load-bearing for the soundness of the informalization step.
  2. [Section 4.1 and Appendix D (Table 4)] The paper concedes that for MATH, 822 of 7,500 seeds cannot be formalized, approximately 3,600 formalizations are 'inaccurate although usable,' and 80K problems were generated without solution verification. For these subsets, the advertised guarantee that solver verification ensures validity is either absent or operates on a formalization that may misrepresent the original problem. Please report the fraction of final training examples that come from these subsets and provide ablations (e.g., training without the 80K unverified examples, or consistency rates stratified by formalization accuracy) to show that the main results do not depend on unverified or misformalized data.
  3. [Section 4.2 (Table 3) and Checklist item 7] No error bars, multiple seeds, or significance tests are reported, and the checklist states that statistical significance is not provided. The MATH improvements in Table 3 are as small as 1.7–3.2 percentage points, which may be within fine-tuning variance. To support the claim of significant outperformance, please report at least three runs with means and standard deviations (or bootstrap confidence intervals) for the central same-budget comparisons.
  4. [Section 4.1 (RQ2) and Table 3] The 'same data generation budget' is measured only as the number of generated examples. The proposed pipeline uses GPT-4 for formalization, informalization, and reasoning-path generation plus symbolic solver time, while MetaMathQA's bootstrapping cost is not equivalent. If 'efficiency' is a claimed advantage, a constant-compute or constant-cost comparison is needed; otherwise the conclusion should be framed as 'same dataset size,' not 'same budget.'
  5. [Section 5 (Related Work) and Tables 2–3] Xwin-Math, which is cited as a peer study and also uses GPT-4 to generate math data, is not included in the experimental comparison. Given that Xwin-Math reports strong open-source results and represents a direct alternative data-generation approach, its omission weakens the claim that the fine-tuned models surpass the state of the art. Please add Xwin-Math (or another recent strong baseline) to Tables 2 or 3, or justify the exclusion.
minor comments (9)
  1. [Introduction vs. Section 4.1] The Introduction states that the framework generates 'a mathematical dataset of 620K examples,' but Section 4.1 reports 860K and Table 2 lists 860K. Please reconcile the numbers.
  2. [Abstract] The abstract states that the Mistral-7B model outperforms GPT-3.5-Turbo 'by 2.4%' on GSM8K, but Section 4.2 reports a 6.0-point margin (86.8 vs. 80.8). Correct the abstract.
  3. [Algorithm 1] Algorithm 1 has two loops with unspecified bounds ('for i = 1, . . . ,do') and a typo ('Initalize'). Please specify termination conditions (e.g., maximum iterations or acceptance thresholds).
  4. [Figure 3] Figure 3 and the RQ3 text refer to 'BLUE score'; this should be 'BLEU score.'
  5. [Section 4.1] The dataset name is typeset inconsistently ('SV AMP' vs. 'SVAMP'); please use a consistent spelling.
  6. [Appendix D] The training details mention fine-tuning a LLaMA-2-70B model with QLoRA, but no results for a 70B model appear in Tables 2 or 3; clarify whether this experiment was run and where its results are reported.
  7. [Section 2.3] The projected MCMC sampler is described only by reference; the paper should give the proposal distribution, acceptance criterion, and number of iterations so that the diversity-sampling step is reproducible.
  8. [Table 1] The rows of Table 1 do not clearly associate each consistency rate with the operation it tests; please add explicit row labels.
  9. [Section 4.2 (RQ3)] The memorization analysis selects '150 problems with the highest majority vote score' but does not define the majority-vote score; please add a definition or reference.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the reported gains are external benchmark measurements, and the self-citations are non-load-bearing technique references.

full rationale

The paper's central claims are empirical: fine-tuned model accuracies on GSM8K, MATH, SVAMP, ASDiv, and DyVal are measured against external benchmarks that are not used to fit any parameter of the generation framework. The data-generation pipeline does not define its target metric in terms of its own outputs; the same-budget comparison with MetaMathQA (Table 3) is a controlled empirical contrast, not a derivation. The solver-verification step checks the mutated SMT-LIB formula, and the informalization consistency check compares GPT-4's solution of the natural-language problem against the symbolic answer; both checks are genuine and can fail, and the paper reports failure rates (Table 1, Appendix D). The self-citations, e.g., [15] for projected MCMC and [72] for the fuzzy-logic encoding, are technique citations and are not load-bearing; projected MCMC is also attributed to independent work [14]. Appendix D's admissions — 822 of 7,500 MATH problems unformalizable, about 3,600 formalizations inaccurate but 'usable,' and 80K MATH problems generated without solver verification — weaken the coverage of the validity guarantee, but they are limitations of the method's reach, not a circular reduction of the central claim to its inputs. The checklist's broken cross-references ('Appendix ??') are presentation defects and do not affect circularity.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new mathematical or physical entities. Its contribution is a procedural pipeline; the free parameters are the hand-chosen mutation schedule, operator set, and informalization patterns, while the axioms listed are the unverified or partially verified assumptions about formalization fidelity, the consistency surrogate, MCMC mixing, and reasoning-path correctness.

free parameters (3)
  • Mutation operator set and selection distribution
    The simplification and complication strategies (simplify, qe, gaussian_elim, expression complications with random operators and interpreted functions) are hand-chosen in Section 2.3, and the probabilities or relative frequencies of each operation are not reported. This determines the character of the generated data.
  • Difficulty level schedule and per-level dataset sizes = GSM8K: 30K/100K/100K/100K/100K; MATH: 70K/120K/120K/120K
    Section 4.1 sets the number of complication steps per difficulty level and the data volume per level by hand. The paper's Figure 2 shows the choice of levels affects reasoning-step counts and downstream accuracy, so the exact schedule is part of the method.
  • Informalization pattern selection (P1 vs P2)
    Section 3 recommends two patterns based on a 1,000-problem consistency evaluation (Table 1). Which pattern is applied to which problems at scale is a choice that affects the style and potentially the difficulty of the final natural language problems.
assumptions (4)
  • domain assumption SMT-LIB formalization of a seed problem faithfully represents the problem's intended mathematical meaning.
    The entire mutation pipeline assumes the symbolic form is a correct target for mutation. Appendix D concedes this fails for 822/7,500 MATH problems and is inaccurate for roughly 3,600 others, making this assumption false in a large fraction of cases.
  • domain assumption A GPT-4 solution matching the symbolic solver answer implies the informalized natural language problem is consistent with the formal problem.
    Section 3 uses this surrogate consistency rate as a lower bound on true consistency, asserting 'zero false positive' without quantitative evidence.
  • domain assumption Projected MCMC, as sketched in Algorithm 1, explores the solution space diversely enough to avoid mode collapse.
    No convergence or mixing analysis is given for the mutation chain; the paper relies on the cited works [14,15] for the general technique, but the adaptation to SMT-LIB mutation syntax is not specified in enough detail to check.
  • ad hoc to paper A GPT-4-generated reasoning path that ends at the correct final answer is a valid step-by-step derivation suitable as supervision.
    Section 4.1 states reasoning paths are generated by GPT-4 and verified only by comparing the final answer with the solver's answer; intermediate steps are not checked for correctness.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neuro-Symbolic Data Generation for Math Reasoning." pith.science (2026). https://pith.science/paper/DFSMVLQW

@misc{pith2026241204857,
  author       = {Pith},
  title        = {Pith review of: Neuro-Symbolic Data Generation for Math Reasoning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DFSMVLQW}},
  note         = {Machine review of arXiv:2412.04857}
}
read the original abstract

A critical question about Large Language Models (LLMs) is whether their apparent deficiency in mathematical reasoning is inherent, or merely a result of insufficient exposure to high-quality mathematical data. To explore this, we developed an automated method for generating high-quality, supervised mathematical datasets. The method carefully mutates existing math problems, ensuring both diversity and validity of the newly generated problems. This is achieved by a neuro-symbolic data generation framework combining the intuitive informalization strengths of LLMs, and the precise symbolic reasoning of math solvers along with projected Markov chain Monte Carlo sampling in the highly-irregular symbolic space. Empirical experiments demonstrate the high quality of data generated by the proposed method, and that the LLMs, specifically LLaMA-2 and Mistral, when realigned with the generated data, surpass their state-of-the-art counterparts.

Figures

Figures reproduced from arXiv: 2412.04857 by the authors.

Figure 1
Figure 1. The overview of our neuro-symbolic data generation framework. The framework comprises [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The performance of our proposed mutation mechanism. The first figure illustrates that [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. BLUE scores between the output of our fine-tuned model, versus the ground￾truth solution and GPT-4 output. The model is fine-tuned on the Mistral 7B base model, and MetaMath Mistral 7B model is also included as a reference. The results show that our method does not induce data contamination. 0.0 0.2 0.4 0.6 0.8 BLUE 0.4 0.6 0.5 0.6 0.6 0.8 0.5 0.5 Training Set MMQA Ours GSM8K Ground-Truth GSM8K GPT-4 MATH Ground-Tru… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Performance curves of the LLaMA-2-7B models fine-tuned on various scales of datasets. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: The diversity gain across all difficulty levels. The results indicate that the diversity gain of [PITH_FULL_IMAGE:figures/full_fig_p022_5.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. RE-IMAGINE: Symbolic Benchmark Synthesis for Reasoning Evaluation

    cs.CL 2025-06 conditional novelty 6.0 of 10

    Language models score substantially lower on automatically generated variations of standard math, logic, and code benchmarks, indicating partial reliance on memorization.

  2. LLM-Powered Benchmark Factory: Reliable, Generic, and Efficient

    cs.CL 2025-02 conditional novelty 6.0 of 10

    BenchMaker automatically builds multiple-choice benchmarks from assessment demands and matches human benchmarks' ranking power (0.967 Pearson correlation with MMLU-Pro across 12 LLMs) at $0.005 per item.

Reference graph

Works this paper leans on

88 extracted references · 48 canonical work pages · cited by 2 Pith papers

  1. [1]

    Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra

    Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V . Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Advances in Neural Information Processing Systems 35, 2022

    2022

  2. [2]

    Artur d’Avila Garcez and Luís C. Lamb. Neurosymbolic AI: the 3rd wave.Artificial Intelligence Review, 56(11):12387–12406, 2023

    2023

  3. [3]

    A survey of large language models

    Wayne Xin Zhao, Kun Zhou, Junyi Li, Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, et al. A survey of large language models. arXiv preprint arXiv:2303.18223, 2023

    arXiv 2023

  4. [4]

    A survey on large language model based autonomous agents

    Lei Wang, Chen Ma, Xueyang Feng, Zeyu Zhang, Hao Yang, Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Xu Chen, Yankai Lin, et al. A survey on large language model based autonomous agents. arXiv preprint arXiv:2308.11432, 2023

    arXiv 2023

  5. [5]

    Chatgpt for good? on opportunities and challenges of large language models for education

    Enkelejda Kasneci, Kathrin Seßler, Stefan Küchemann, Maria Bannert, Daryna Dementieva, Frank Fischer, Urs Gasser, Georg Groh, Stephan Günnemann, Eyke Hüllermeier, et al. Chatgpt for good? on opportunities and challenges of large language models for education. Learning and individual differences, 103:102274, 2023

    2023

  6. [6]

    A survey on evaluation of large language models

    Yupeng Chang, Xu Wang, Jindong Wang, Yuan Wu, Linyi Yang, Kaijie Zhu, Hao Chen, Xiaoyuan Yi, Cunxiang Wang, Yidong Wang, et al. A survey on evaluation of large language models. ACM Transactions on Intelligent Systems and Technology, 2023

    2023

  7. [7]

    Scibench: Evaluating college-level scientific problem-solving abilities of large language models

    Xiaoxuan Wang, Ziniu Hu, Pan Lu, Yanqiao Zhu, Jieyu Zhang, Satyen Subramaniam, Arjun R Loomba, Shichang Zhang, Yizhou Sun, and Wei Wang. Scibench: Evaluating college-level scientific problem-solving abilities of large language models. arXiv preprint arXiv:2307.10635, 2023

    arXiv 2023

  8. [8]

    An Independent Evaluation of ChatGPT on Mathematical Word Problems (MWP)

    Paulo Shakarian, Abhinav Koyyalamudi, Noel Ngu, and Lakshmivihari Mareedu. An in- dependent evaluation of chatgpt on mathematical word problems (mwp). arXiv preprint arXiv:2302.13814, 2023

    work page Pith review arXiv 2023

Show all 88 references
  1. [9]

    Dyval: Graph-informed dynamic evaluation of large language models

    Kaijie Zhu, Jiaao Chen, Jindong Wang, Neil Zhenqiang Gong, Diyi Yang, and Xing Xie. Dyval: Graph-informed dynamic evaluation of large language models. CoRR, abs/2309.17167, 2023

    2023 arXiv

  2. [10]

    Training verifiers to solve math word problems

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021

    arXiv

  3. [11]

    Measuring mathematical problem solving with the math dataset

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. In Advances in Neural Information Processing Systems Track on Datasets and Benchmarks, 2021

    2021

  4. [12]

    Are nlp models really able to solve simple math word problems? arXiv preprint arXiv:2103.07191, 2021

    Arkil Patel, Satwik Bhattamishra, and Navin Goyal. Are nlp models really able to solve simple math word problems? arXiv preprint arXiv:2103.07191, 2021

    2021 arXiv

  5. [13]

    Llemma: An open language model for mathematics

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023. 11

    arXiv

  6. [14]

    Sampling constraint satisfaction solutions in the local lemma regime

    Weiming Feng, Kun He, and Yitong Yin. Sampling constraint satisfaction solutions in the local lemma regime. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing, pages 1565–1578, 2021

    2021

  7. [15]

    Softened symbol grounding for neuro-symbolic systems

    Zenan Li, Yuan Yao, Taolue Chen, Jingwei Xu, Chun Cao, Xiaoxing Ma, L Jian, et al. Softened symbol grounding for neuro-symbolic systems. In The Eleventh International Conference on Learning Representations, 2023

    2023

  8. [16]

    Llama 2: Open foundation and fine-tuned chat models

    Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, W...

    2023 arXiv

  9. [17]

    Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chap- lot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thoma...

    arXiv

  10. [18]

    A diverse corpus for evaluating and developing english math word problem solvers

    Shen-Yun Miao, Chao-Chun Liang, and Keh-Yih Su. A diverse corpus for evaluating and developing english math word problem solvers. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 975–984, 2020

    2020

  11. [19]

    The SMT-LIB Standard: Version 2.6

    Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org

    2017

  12. [20]

    Z3: An efficient smt solver

    Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 337–340. Springer, 2008

    2008

  13. [21]

    cvc5: A versatile and industrial-strength smt solver

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength smt solver. InInternational Conference on Tools and Algorithms for the Co...

    2022

  14. [22]

    The mathsat 4 smt solver: Tool paper

    Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, and Roberto Sebastiani. The mathsat 4 smt solver: Tool paper. In Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings 20 , pages 299–303. S...

    2008

  15. [23]

    Sympy: symbolic computing in python

    Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ond ˇrej ˇCertík, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. Sympy: symbolic computing in python. PeerJ Computer Science, 3:e103, 2017

    2017

  16. [24]

    Scipy 1.0: fundamental algorithms for scientific computing in python

    Pauli Virtanen, Ralf Gommers, Travis E Oliphant, Matt Haberland, Tyler Reddy, David Courna- peau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, et al. Scipy 1.0: fundamental algorithms for scientific computing in python. Nature methods, 17(3):261–272, 2020

    2020

  17. [25]

    The strategy challenge in smt solving

    Leonardo De Moura and Grant Olney Passmore. The strategy challenge in smt solving. In Automated Reasoning and Mathematics: Essays in Memory of William W. McCune , pages 15–44. Springer, 2013. 12

    2013

  18. [26]

    The complexity of enumeration and reliability problems

    Leslie G Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3):410–421, 1979

    1979

  19. [27]

    The markov chain monte carlo method: an approach to approximate counting and integration

    Mark Jerrum and Alistair Sinclair. The markov chain monte carlo method: an approach to approximate counting and integration. Approximation Algorithms for NP-hard problems, PWS Publishing, 1996

    1996

  20. [28]

    Uniform solution sampling using a constraint solver as an oracle

    Stefano Ermon, Carla Gomes, and Bart Selman. Uniform solution sampling using a constraint solver as an oracle. In Proceedings of the Twenty-Eighth Conference on Uncertainty in Artificial Intelligence, pages 255–264, 2012

    2012

  21. [29]

    Autoformalization with large language models

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022

    2022

  22. [30]

    Wizardmath: Empowering mathematical rea- soning for large language models via reinforced evol-instruct

    Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. Wizardmath: Empowering mathematical rea- soning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.09583, 2023

    2023 arXiv

  23. [31]

    Query and response augmentation cannot help out-of- domain math reasoning generalization

    Chengpeng Li, Zheng Yuan, Hongyi Yuan, Guanting Dong, Keming Lu, Jiancan Wu, Chuanqi Tan, Xiang Wang, and Chang Zhou. Query and response augmentation cannot help out-of- domain math reasoning generalization. CoRR, abs/2310.05506, 2023

    arXiv

  24. [32]

    Mammoth: Building math generalist models through hybrid instruction tuning

    Xiang Yue, Xingwei Qu, Ge Zhang, Yao Fu, Wenhao Huang, Huan Sun, Yu Su, and Wenhu Chen. Mammoth: Building math generalist models through hybrid instruction tuning. CoRR, abs/2309.05653, 2023

    2023 arXiv

  25. [33]

    Metamath: Bootstrap your own mathematical questions for large language models

    Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint arXiv:2309.12284, 2023

    2023 arXiv

  26. [34]

    Solving quantitative reasoning problems with language models

    Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. Solving quantitative reasoning problems with language models. Advances in Neural Information Processing Systems, 35...

    2022

  27. [35]

    Bleu: a method for automatic evaluation of machine translation

    Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311–318, 2002

    2002

  28. [36]

    Testing language models on a held-out high school national finals exam

    Keiran Paster. Testing language models on a held-out high school national finals exam. https: //huggingface.co/datasets/keirp/hungarian_national_hs_finals_exam, 2023

    2023

  29. [37]

    Large language models for mathematical reasoning: Progresses and challenges

    Janice Ahn, Rishu Verma, Renze Lou, Di Liu, Rui Zhang, and Wenpeng Yin. Large language models for mathematical reasoning: Progresses and challenges. In Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics, pages 225–237, 2024

    2024

  30. [38]

    A survey of deep learning for mathematical reasoning

    Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. A survey of deep learning for mathematical reasoning. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics, pages 14605–14631, 2023

    2023

  31. [39]

    Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts

    Pan Lu, Hritik Bansal, Tony Xia, Jiacheng Liu, Chunyuan Li, Hannaneh Hajishirzi, Hao Cheng, Kai-Wei Chang, Michel Galley, and Jianfeng Gao. Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts. In Proceedings of the 12th International Conference...

    2024

  32. [40]

    Large language models are zero-shot reasoners

    Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems, pages 22199–222...

    2022

  33. [41]

    Le, Ed H

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V . Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In Proceedings of the 11th International Conference on Learning Representations , 2023

    2023

  34. [42]

    Le, and Ed H

    Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc V . Le, and Ed H. Chi. Least-to-most prompting enables complex reasoning in large language models. In Proceedings of the 11th International Confere...

    2023

  35. [43]

    Decomposed prompting: A modular approach for solving complex tasks

    Tushar Khot, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. Decomposed prompting: A modular approach for solving complex tasks. In Proceedings of the 11th International Conference on Learning Representations, 2023

    2023

  36. [44]

    Chain-of-thought prompting elicits reasoning in large language models

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in N...

    2022

  37. [45]

    Complexity-based prompting for multi-step reasoning

    Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. Complexity-based prompting for multi-step reasoning. In Proceedings of the 11th International Conference on Learning Representations, 2023

    2023

  38. [46]

    Automatic chain of thought prompting in large language models

    Zhuosheng Zhang, Aston Zhang, Mu Li, and Alex Smola. Automatic chain of thought prompting in large language models. In Proceedings of the 11th International Conference on Learning Representations, 2023

    2023

  39. [47]

    Dynamic prompt learning via policy gradient for semi-structured mathematical reasoning

    Pan Lu, Liang Qiu, Kai-Wei Chang, Ying Nian Wu, Song-Chun Zhu, Tanmay Rajpurohit, Peter Clark, and Ashwin Kalyan. Dynamic prompt learning via policy gradient for semi-structured mathematical reasoning. In Proceedings of the 11th International Conference on Learning Representat...

    2023

  40. [48]

    Boosting llm reason- ing: Push the limits of few-shot learning with reinforced in-context pruning

    Xijie Huang, Li Lyna Zhang, Kwang-Ting Cheng, and Mao Yang. Boosting llm reason- ing: Push the limits of few-shot learning with reinforced in-context pruning. arXiv preprint arXiv:2312.08901, 2023

    2023 arXiv

  41. [49]

    Teaching small language models to reason

    Lucie Charlotte Magister, Jonathan Mallinson, Jakub Adámek, Eric Malmi, and Aliaksei Severyn. Teaching small language models to reason. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics, pages 1773–1781, 2023

    2023

  42. [50]

    Scaling relationship on learning mathematical reasoning with large language models, 2023

    Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Keming Lu, Chuanqi Tan, Chang Zhou, and Jingren Zhou. Scaling relationship on learning mathematical reasoning with large language models, 2023

    2023

  43. [51]

    Making large language models better reasoners with alignment

    Peiyi Wang, Lei Li, Liang Chen, Feifan Song, Binghuai Lin, Yunbo Cao, Tianyu Liu, and Zhifang Sui. Making large language models better reasoners with alignment. CoRR, abs/2309.02144, 2023

    2023 arXiv

  44. [52]

    Large language models are better reasoners with self-verification

    Yixuan Weng, Minjun Zhu, Fei Xia, Bin Li, Shizhu He, Shengping Liu, Bin Sun, Kang Liu, and Jun Zhao. Large language models are better reasoners with self-verification. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 2550–2575, 2023

    2023

  45. [53]

    Forward-backward reasoning in large language models for mathematical verification

    Weisen Jiang, Han Shi, Longhui Yu, Zhengying Liu, Yu Zhang, Zhenguo Li, and James T Kwok. Forward-backward reasoning in large language models for mathematical verification. arXiv preprint arXiv:2308.07758, 3, 2023

    2023 arXiv

  46. [54]

    Common 7b language models already possess strong math capabilities

    Chen Li, Weiqi Wang, Jingcheng Hu, Yixuan Wei, Nanning Zheng, Han Hu, Zheng Zhang, and Houwen Peng. Common 7b language models already possess strong math capabilities. CoRR, abs/2403.04706, 2024

    2024 arXiv

  47. [55]

    Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W. Cohen. Program of thoughts prompt- ing: Disentangling computation from reasoning for numerical reasoning tasks. Transactions on Machine Learning Research, 2023. 14

    2023

  48. [56]

    PAL: program-aided language models

    Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. PAL: program-aided language models. In Proceedings of the 40th International Conference on Machine Learning, pages 10764–10799, 2023

    2023

  49. [57]

    Mathcoder: Seamless code integration in llms for enhanced mathematical reasoning

    Ke Wang, Houxing Ren, Aojun Zhou, Zimu Lu, Sichun Luo, Weikang Shi, Renrui Zhang, Linqi Song, Mingjie Zhan, and Hongsheng Li. Mathcoder: Seamless code integration in llms for enhanced mathematical reasoning. arXiv preprint arXiv:2310.03731, 2023

    arXiv

  50. [58]

    Don’t trust: Verify – grounding LLM quantitative reasoning with autoformalization

    Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify – grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, 2024

    2024

  51. [59]

    Tora: A tool-integrated reasoning agent for mathematical problem solving

    Zhibin Gou, Zhihong Shao, Yeyun Gong, Yujiu Yang, Minlie Huang, Nan Duan, Weizhu Chen, et al. Tora: A tool-integrated reasoning agent for mathematical problem solving. arXiv preprint arXiv:2309.17452, 2023

    2023 arXiv

  52. [60]

    Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli. Cvc4. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23, pages 171–17...

    2011

  53. [61]

    Validating smt solvers via semantic fusion

    Dominik Winterer, Chengyu Zhang, and Zhendong Su. Validating smt solvers via semantic fusion. In Proceedings of the 41st ACM SIGPLAN Conference on programming language design and implementation, pages 718–730, 2020

    2020

  54. [62]

    Curriculum learning

    Yoshua Bengio, Jérôme Louradour, Ronan Collobert, and Jason Weston. Curriculum learning. In Proceedings of the 26th annual international conference on machine learning, pages 41–48, 2009

    2009

  55. [63]

    Curriculum learning: A survey

    Petru Soviany, Radu Tudor Ionescu, Paolo Rota, and Nicu Sebe. Curriculum learning: A survey. International Journal of Computer Vision, 130(6):1526–1565, 2022

    2022

  56. [64]

    Alphamath almost zero: process supervision without process

    Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. Alphamath almost zero: process supervision without process. arXiv preprint arXiv:2405.03553, 2024

    2024 arXiv

  57. [65]

    Qlora: Efficient finetuning of quantized llms

    Tim Dettmers, Artidoro Pagnoni, Ari Holtzman, and Luke Zettlemoyer. Qlora: Efficient finetuning of quantized llms. In Advances in Neural Information Processing Systems, 2023

    2023

  58. [66]

    Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen

    Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models. In Proceedings of the 1th International Conference on Learning Representations, 2022

    2022

  59. [67]

    Stanford alpaca: An instruction-following llama model

    Rohan Taori, Ishaan Gulrajani, Tianyi Zhang, Yann Dubois, Xuechen Li, Carlos Guestrin, Percy Liang, and Tatsunori B Hashimoto. Stanford alpaca: An instruction-following llama model. Technical report, 2023

    2023

  60. [68]

    Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms

    Marco Gario and Andrea Micheli. Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In SMT Workshop 2015, 2015

    2015

  61. [69]

    Array programming with numpy

    Charles R Harris, K Jarrod Millman, Stéfan J Van Der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J Smith, et al. Array programming with numpy. Nature, 585(7825):357–362, 2020

    2020

  62. [70]

    Xsat: a fast floating-point satisfiability solver

    Zhoulai Fu and Zhendong Su. Xsat: a fast floating-point satisfiability solver. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 28, pages 187–209. Springer, 2016

    2016

  63. [71]

    Dl2: training and querying neural networks with logic

    Marc Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang, and Martin Vechev. Dl2: training and querying neural networks with logic. In International Conference on Machine Learning, pages 1931–1941. PMLR, 2019

    1931

  64. [72]

    Learn- ing with logical constraints but without shortcut satisfaction

    Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, L Jian, et al. Learn- ing with logical constraints but without shortcut satisfaction. In The Eleventh International Conference on Learning Representations, 2022. 15

    2022

  65. [73]

    Sara bought a pair of shoes for $50.00 and a dress for $200.00. If Rachel has twice the amount that Sara spent in total, how much is Rachel’s budget?

    Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.04805, 2018. 16 A Broader Impacts The paper aims to advance the field of math data generation. There ar...

    2018 arXiv

  66. [74]

    Guidelines: • The answer NA means that the abstract and introduction do not include the claims made in the paper

    Claims Question: Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope? Answer: [Yes] Justification: The abstract and introduction clearly state our claims. Guidelines: • The answer NA means that the abstract and introd...

  67. [75]

    Limitations

    Limitations Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [Yes] Justification: The limitation is thoroughly discussed in Appendix ??. Guidelines: • The answer NA means that the paper has no limitation while the answer No means t...

  68. [76]

    Guidelines: • The answer NA means that the paper does not include theoretical results

    Theory Assumptions and Proofs Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? Answer: [NA] 23 Justification: N/A. Guidelines: • The answer NA means that the paper does not include theoretical results...

  69. [77]

    We will public the code, as well as the fine-tuned models, for the reproducibility

    Experimental Result Reproducibility Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and da...

  70. [78]

    Guidelines: • The answer NA means that paper does not include experiments requiring code

    Open access to data and code Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material? 24 Answer: [Yes] Justification: We provide the code for ...

  71. [79]

    Guidelines: • The answer NA means that the paper does not include experiments

    Experimental Setting/Details Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results? Answer: [Yes] Justification: Training and test settings ar...

  72. [80]

    Guidelines: • The answer NA means that the paper does not include experiments

    Experiment Statistical Significance Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments? Answer: [No] Justification: We cannot provide statistical significance of the e...

  73. [81]

    Guidelines: • The answer NA means that the paper does not include experiments

    Experiments Compute Resources Question: For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments? Answer: [Yes] Justification: Details of the computer...

  74. [82]

    Guidelines: • The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics

    Code Of Ethics Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? Answer: [Yes] Justification: We have carefully reviewed the NeurIPS Code of Ethics. Guidelines: • The answer...

  75. [83]

    Guidelines: • The answer NA means that there is no societal impact of the work performed

    Broader Impacts Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed? Answer: [Yes] Justification: Social impacts are discussed in ??. Guidelines: • The answer NA means that there is no societal impact of...

  76. [84]

    Guidelines: • The answer NA means that the paper poses no such risks

    Safeguards Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)? Answer: [NA] Justification: The paper does ...

  77. [85]

    Guidelines: • The answer NA means that the paper does not use existing assets

    Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected? Answer: [Yes] Justification: Code packages an...

  78. [86]

    Guidelines: • The answer NA means that the paper does not release new assets

    New Assets Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets? Answer: [NA] Justification: The paper does not release new assets up to now. Guidelines: • The answer NA means that the paper does not release ne...

  79. [87]

    Guidelines: • The answer NA means that the paper does not involve crowdsourcing nor research with human subjects

    Crowdsourcing and Research with Human Subjects Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)? A...

  80. [88]

    Guidelines: • The answer NA means that the paper does not involve crowdsourcing nor research with human subjects

    Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals...

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.