Research map / Large language models / Agents, code and math
Neuro-Symbolic Data Generation for Math Reasoning
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes a neuro-symbolic framework that mutates formal (SMT-LIB) math problems via projected MCMC and symbolic solvers, informalizes them with GPT-4, and fine-tunes LLaMA-2 and Mistral on the resulting 860K-example dataset.
Problem
LLMs remain weak at mathematical reasoning, and existing math data generation either sacrifices validity (prompt-based rephrasing) or diversity (template-based rewriting), limiting high-quality supervised math data.
Approach
Generate math problems by mutating formalized SMT-LIB problems with simplification and complication operators, sample auxiliary variables via projected MCMC with symbolic solver inverse projection to ensure validity and diversity, then informalize back to natural language with GPT-4 and verify reasoning paths with symbolic solvers.
Key results
- Mistral 7B fine-tuned on the generated data reaches 86.8% on GSM8K and 37.3% on MATH, surpassing MetaMath by 3.6 and 4.3 points and slightly exceeding GPT-3.5-Turbo on GSM8K (80.8%).
- LLaMA-2 7B fine-tuned on the data reaches 79.0% GSM8K and 30.4% MATH, improving over the best open baseline by at least 10.6 points on both.
- Under equal 240K GSM8K budget vs MetaMathQA, LLaMA-2 7B improves GSM8K from 66.1 to 72.7 and SVAMP from 61.7 to 78.8.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Train on neuro-symbolically generated math data instead of existing baseline data | LLaMA-2 7B · GSM8K | accuracy: 68.4 -> 79.0; +10.6 | Helped |
| Train on neuro-symbolically generated math data instead of existing baseline data | LLaMA-2 7B · MATH | accuracy: 19.8 -> 30.4; +10.6 | Helped |
| Train on neuro-symbolically generated math data instead of existing baseline data | LLaMA-2 13B · GSM8K | accuracy: 72.3 -> 84.1; +10.1 | Helped |
| Train on neuro-symbolically generated math data instead of existing baseline data | LLaMA-2 13B · MATH | accuracy: 22.4 -> 33.7; +11.3 | Helped |
| Train on neuro-symbolically generated math data instead of existing baseline data | Mistral 7B · GSM8K | accuracy: 83.2 -> 86.8; +3.6 | Helped |
| Train on neuro-symbolically generated math data instead of existing baseline data | Mistral 7B · MATH | accuracy: 33.0 -> 37.3; +4.3 | Helped |
| Use neuro-symbolically generated data rather than MetaMathQA with the same 240K GSM8K training budget | LLaMA-2 7B · GSM8K | accuracy: 66.1 -> 72.7; ↑6.6 | Helped |
| Use neuro-symbolically generated data rather than MetaMathQA with the same 240K GSM8K training budget | LLaMA-2 7B · SVAMP | accuracy: 61.7 -> 78.8; ↑17.1 | Helped |
| Use neuro-symbolically generated data rather than MetaMathQA with the same 155K MATH training budget | LLaMA-2 7B · GSM8K | accuracy: 28.6 -> 42.1; ↑ 13.5 | Helped |
| Use neuro-symbolically generated data rather than MetaMathQA with the same 155K MATH training budget | LLaMA-2 7B · SVAMP | accuracy: 49.0 -> 73.4; ↑ 24.4 | Helped |
| Add the mutation operation to informalization (ablation) | GPT-4 informalization · GSM8K sample (1,000 problems) | consistency rate: 75.6 -> 41.6 | Hurt |
| Use informalization pattern P1 (operations 1–5) (ablation) | GPT-4 informalization · GSM8K sample (1,000 problems) | consistency rate: 90.5 | Helped |
Surprising findings
- Tool-based models such as MAmmoTH degrade sharply without tools (e.g., Mistral 7B MATH from 40.0 to 17.5 w/o tools), suggesting over-reliance on external tools.
- Roughly 3,600 of 7,500 MATH training formalizations were inaccurate and 822 could not be formalized, mainly in precalculus and geometry, so GPT-4 prompting without verification was used for those problems.
Limitations
- Effectiveness depends heavily on the expressiveness of symbolic solvers, which struggle with gcd/lcm, multivariate inequalities, and geometry/precalculus concepts.
- Mutation operators are limited and do not yet produce college- or olympiad-level difficulty problems.
- Relies on GPT-4 for informalization and reasoning path generation; some MATH problems bypass solution verification.
Experimental setup
Datasets: GSM8K MATH MetaMathQA SVAMP ASDiv DyVal
Benchmarks: GSM8K MATH SVAMP ASDiv DyVal Hungarian High School National Finals Exam
Metrics: accuracy (pass@1) BLEU score for contamination consistency rate diversity gain
Baselines: WizardMath MuggleMATH MAmmoTH MetaMath MetaMathQA Tora
Builds on: MetaMath projected MCMC SMT-LIB PySMT QLoRA
Closest papers by meaning
- Advancing Mathematical Reasoning in Language Models: The Impact of Problem-Solving Data, Data Synthesis Methods, and Training Stages (ICLR 2025 · similarity 0.91)
- Controlling Equational Reasoning in Large Language Models with Prompt Interventions (AAAI 2025 · similarity 0.90)
- Frugal LMs Trained to Invoke Symbolic Solvers Achieve Parameter-Efficient Arithmetic Reasoning (AAAI 2024 · similarity 0.90)
- Learning Theorem Rationale for Improving the Mathematical Reasoning Capability of Large Language Models (AAAI 2025 · similarity 0.89)
- MathCoder2: Better Math Reasoning from Continued Pretraining on Model-translated Mathematical Code (ICLR 2025 · similarity 0.89)
- Physics of Language Models: Part 2.2, How to Learn From Mistakes on Grade-School Math Problems (ICLR 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.