{"id":"64aab1f4-1d4d-478b-9354-1ad03d5513ac","arxiv_id":"2412.04857","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A neuro-symbolic generator that mutates math problems in SMT-LIB form with solver validation and LLM informalization produces training data that improves LLM math reasoning over MetaMath and similar baselines.","lead":"The paper builds a pipeline that converts math word problems into solver-checkable logic, mutates those formal versions to create new problems, and translates them back into words with GPT-4. Fine-tuning LLaMA and Mistral models on this generated data improves GSM8K and MATH accuracy beyond existing open-source data-generation baselines at matched data budgets.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Formalization fidelity is the load-bearing assumption: solver verification and consistency checks certify only the formal problem, while Appendix D concedes thousands of inaccurate formalizations and 80K unverified MATH examples.","rationale":"The reader's weakest assumption pinpoints exactly the same issue: autoformalization fidelity is load-bearing, and the appendix admits substantial inaccuracies and unverified data. This is the single most consequential soft spot because the paper's headline contribution is the symbolic diversity-validity guarantee; if that guarantee only holds for a subset of data, the causal story behind the empirical gains is not proven. However, the paper provides same-budget comparisons against MetaMathQA that show large improvements, and the weakness is addressable by releasing the dataset and performing human evaluation on generated problems. Therefore the appropriate verdict remains CONDITIONAL rather than REJECT: the claims are plausible but need the specified checks to be accepted as stated. The reader already reached this conclusion, so my read does not change the verdict.","tokens_in":127,"tokens_out":3100,"duration_ms":45673,"concrete_test":"Independently verify formalization fidelity on a random sample of 200 MATH seeds: for each seed, solve the autoformalized SMT-LIB problem and compare its answer to the gold answer, and have a human judge whether the formal constraints match the original wording. If more than 5% disagree, solver-verified mutations of those seeds do not guarantee valid novel problems, weakening the diversity-validity claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central mechanism claims that symbolic mutation plus solver verification guarantees both diversity and validity. But the solver verifies only the mutated SMT-LIB formula, not the natural-language problem. If GPT-4's autoformalization misrepresents a seed problem (Appendix D: 822 of 7,500 cannot be formalized, ~3,600 are inaccurate but 'usable'), then every mutation of that inaccurate formalization is likewise disconnected from the original math problem. The informalization consistency check in Section 3 is a partial safeguard, but it only tests whether GPT-4's solution to the new NL problem matches the solver's answer to the mutated formal problem; a nonsense NL problem can still be internally consistent with a misformalized mutant. The paper even admits 80K MATH problems were generated without solution verification (Table 4), so for those examples the full validity guarantee is absent. Thus the claimed advantage over plain rephrasing—that symbolic mutation with solver verification yields valid, diverse problems—is not established for a substantial fraction of the dataset.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":24516,"tokens_out":9157,"duration_ms":83189,"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":[{"comment":"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.","section":"Section 3 (Informalization)"},{"comment":"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.","section":"Section 4.1 and Appendix D (Table 4)"},{"comment":"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.","section":"Section 4.2 (Table 3) and Checklist item 7"},{"comment":"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.'","section":"Section 4.1 (RQ2) and Table 3"},{"comment":"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.","section":"Section 5 (Related Work) and Tables 2–3"}],"minor_comments":[{"comment":"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.","section":"Introduction vs. Section 4.1"},{"comment":"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.","section":"Abstract"},{"comment":"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).","section":"Algorithm 1"},{"comment":"Figure 3 and the RQ3 text refer to 'BLUE score'; this should be 'BLEU score.'","section":"Figure 3"},{"comment":"The dataset name is typeset inconsistently ('SV AMP' vs. 'SVAMP'); please use a consistent spelling.","section":"Section 4.1"},{"comment":"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.","section":"Appendix D"},{"comment":"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.","section":"Section 2.3"},{"comment":"The rows of Table 1 do not clearly associate each consistency rate with the operation it tests; please add explicit row labels.","section":"Table 1"},{"comment":"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.","section":"Section 4.2 (RQ3)"}],"recommendation":"major_revision","confidential_remarks":"The paper would benefit from engaging with MathGenie (arXiv:2405.16337), which also uses solver verification to generate math training data and reports strong results on GSM8K/MATH. The omission of this closely related work from the related-work section is a novelty/completeness concern. Also, the reported dataset size inconsistency (620K vs. 860K) should be fixed before publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick read: this is the first data-generation paper I know of that mutates problems in a formal SMT-LIB space and then informalizes them with an LLM. That is a real conceptual step beyond MetaMath/WizardMath-style rephrasing, and the same-budget comparison in Table 3 is the right experiment. The result—your generated 240K GSM8K beats their 240K MetaMathQA by 6.6 points, and the gap widens on out-of-domain sets—supports the claim that symbolic mutation plus solver verification is adding quality, not just quantity.\n\nThe paper is also better than the field average on evaluation hygiene: out-of-domain checks on SVAMP, ASDiv, and DyVal, a BLEU-based contamination probe, and a scaling study. The limitation section is candid about solver expressiveness and GPT-4 dependence.\n\nThe soft spots are real but proportionate. The formalization-fidelity issue is the load-bearing one. Appendix D says 822 of 7,500 MATH problems cannot be formalized and roughly 3,600 are inaccurate but 'usable.' If the formal seed misrepresents the natural-language problem, every mutation of that seed is semantically disconnected, and the solver verifies only the formal formula, not the word problem. The GPT-4 consistency check is a partial safeguard—if GPT-4's solution to the informalized problem matches the solver's answer, that is decent evidence of alignment—but the paper's claim of 'zero false positive' is unquantified and too strong. The 80K MATH problems generated without solution verification are a minority of the 860K total but a nontrivial slice of the MATH portion.\n\nTwo other concerns are smaller. No error bars: the checklist says they could not compute statistical significance, and some gains are thin (1.7-3.2 points on MATH in Table 3). No code or data is actually released yet, despite the checklist saying it will be; that limits how strongly anyone can read the numbers. Neither flaw sinks the paper, but both should be addressed in revision.\n\nBottom line: the central mechanism is plausible and the same-budget evidence is the most convincing part. The paper deserves a serious referee; with error bars, a released dataset, and a more honest treatment of formalization accuracy, claims like 'zero false positive' should be testable. I'd send it to review, and I'd expect a revise-and-resubmit rather than a straight accept.","headline":"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.","tokens_in":25138,"tokens_out":2566,"would_cite":true,"duration_ms":26995,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["mathematical reasoning","synthetic data generation","neuro-symbolic AI","SMT solvers","symbolic mutation","LLM fine-tuning","GSM8K","MATH"],"falsifier":"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.","tokens_in":24099,"feed_emoji":"🧮","tokens_out":6670,"duration_ms":61735,"temperature":0.7,"pith_summary":"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.","feed_headline":"Solver-verified math mutations lift LLM reasoning scores","feed_subtitle":"An 860K-problem dataset from symbolic-space mutation beats MetaMathQA at equal budgets and scales with more data.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies seed problems and the evaluation benchmark for grade-school math word problems; the GSM8K training set is the source of one half of the generated data.","marker":"[10]"},{"why":"Supplies seed problems and the harder evaluation benchmark; the MATH training set provides the competition-level half of the generated data.","marker":"[11]"},{"why":"Provides MetaMathQA, the bootstrapped-data baseline that the same-budget comparisons in Table 3 are designed to beat.","marker":"[33]"},{"why":"WizardMath is a rephrasing-based baseline whose answer-extraction and evaluation protocol the paper follows.","marker":"[30]"},{"why":"MuggleMATH is a baseline that augments both questions and answers without symbolic verification.","marker":"[31]"},{"why":"MAmmoTH is a hybrid chain-of-thought and program-of-thought baseline used in the main comparison.","marker":"[32]"},{"why":"Supplies the projected MCMC technique used to sample diverse auxiliary-variable solutions while preserving satisfiability.","marker":"[14, 15]"},{"why":"Z3 is the primary SMT solver used to check satisfiability and compute answers for mutated formal problems.","marker":"[20]"},{"why":"Minerva's memorization-detection method is used to argue that the generated data does not contaminate the test set.","marker":"[34]"}],"fun_headline_variants":["Solver-verified math mutations lift LLM reasoning","Neuro-symbolic data generation yields 860K-problem math set","LLMs and solvers team up to write new math problems","Automated symbolic mutation improves LLM math scores","Math LLMs improve when trained on solver-verified data"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Solver-verified math mutations lift LLM reasoning","Neuro-symbolic data generation yields 860K-problem math set","LLMs and solvers team up to write new math problems","Automated symbolic mutation improves LLM math scores","Math LLMs improve when trained on solver-verified data"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00039,"raw_usage":{"total_tokens":2031,"prompt_tokens":898,"completion_tokens":1133,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":514,"completion_tokens_details":{"reasoning_tokens":1051}},"tokens_in":514,"tokens_out":1133,"duration_ms":10823,"temperature":1.0,"reasoning_tokens":1051,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T21:12:36.415457+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Z3: An efficient smt solver","cited_arxiv_id":null,"evidence_quote":"Z3 is the primary SMT solver used to check satisfiability and compute answers for mutated formal problems."}],"review_version":1}