Constraint-Based Synthetic Data Generation for LLM Mathematical Reasoning

Authors: timofey  fedoseev
i  dimitrov
timon  gehr
martin  vechev
école  polytechnique
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-26 13:51:41

Abstract: Mathematical reasoning with large language models (LLMs) is an emerging research area. A recent breakthrough is the use of off-the-shelf tools LLMs are trained to utilize to offload complex tasks they cannot perform independently. Unfortunately, this approach is limited to popular tools, as many specialized tools lack the data to train these models on. Motivated by our observation that the current tools used with LLMs are insufficient for solving counting problems, in this work, we explore the problem of using Satisfiability Modulo Theories (SMT) solvers with LLMs. Namely, we leverage the SMT grammar to generate synthetic data consisting of problem statements and their solutions represented as Python code interacting with the Z3 API. Our experiments show that fine-tuning LLMs on this dataset substantially enhances their ability to generate accurate Z3 constraint encodings and improves their overall mathematical problem-solving capabilities.

Main paper: 
 introduction: 
 Mathematical reasoning is a key emerging area of competence for LLMs. Instead of asking for the solution of a mathematical problem directly, a common technique is to instead ask for program code that in turn solves the problem, offloading already easily automatable parts of the mathematical reasoning to off-the-shelf libraries [1, 2, 3, 4] . This works particularly well for popular libraries (such as SymPy [3] ), because large amounts of high-quality training data can be found online. Common approaches are to train LLMs on solutions obtained from stronger LLMs [5] , and/or to bootstrap from a large number of samples, discarding any incorrect solutions [6] . However, not for every reasoning tool, training data is initially similarly abundant. Therefore, more elaborate data generation approaches may be helpful in order to more readily tap into the potential of less popular tools.Motivated by the observation that existing methods based on SymPy often struggle to solve counting problems, we investigate an approach based on Z3Py [7] , which excels at counting problems with a small enough answer. As expected due to the relatively lower popularity of Z3Py, even state-of-the-art LLMs such as are not yet proficient users of Z3Py.In this work, we make the following contributions:• A method for generating large-scale, high-quality synthetic data for Z3Py that can be used to enhance the mathematical problem-solving capabilities of current LLMs. • An additional Z3Py synthetic dataset obtained through filtering of problems from existing datasets with traditional rejection sampling of solutions from LLMs. • A quantitative evaluation on GPT-4o and GPT-4o-mini against their fine-tuned variants using the two approaches for data generation, showing that our new training data generation method improves the model performance on the Z3Py formalization task more than rejection sampling solutions of existing problems alone. • A qualitative evaluation, showing the models fine-tuned on our Z3Py data can solve problems that they were unable to solve without fine-tuning, even if allowed to use arbitrary libraries.2 Background: Enumerating Solutions with Z3PySatisfiability modulo theories (SMT) generalizes the Boolean satisfiability problem. Constraints can involve various different types of mathematical objects. An SMT solver takes in a set of constraints and determines whether the constraints can be satisfied, producing a solution ("model") if possible.The Z3 theorem prover is a state-of-the-art open-source SMT solver. Z3Py is the Z3 API for Python. We solve counting problems with Z3Py using the technique of blocking: We iteratively solve constraints, adding constraints that the solution should not be one of the ones found previously. This way, the solver steps through all solutions. Once all solutions have been found, the solver returns that the constraints are unsatisfiable. This way we in particular obtain the number of possible solutions.In some cases, state-of-the-art LLMs are able to generate Z3Py code that solves a problem specified in natural language. E.g., we prompted GPT-4o with "Please give me code using Z3Py that counts the number of ways to cover a 4x4 chessboard with 2x1 and 1x2 dominos.", and shortened the result:1 from z3 import * 2 solver = Solver() The code first generates pairs of Z3Py Boolean variables and pairs of squares covered, for each way to place a domino. Then, it adds constraints that say that every square of the board should be covered by exactly one domino. Finally, the solutions are enumerated using the blocking technique.3 4 n = 4 5 board = [(x, y) for x in range(n) for y in range(n)] 6 dom = [(Bool(f"h _ {x} _ {y}"), [(x, y), (x+1, y)]) for x in range(n-1) for y in range(n)] \ 7 + [(Bool(f"v _ {x} _ {y}"), [(x,Unfortunately, despite succeeding in simple cases like this one, LLMs often fail to give a correct encoding, particularly for more involved problem statements. In this work, we show how to fine-tune LLMs on the task of producing correct code to solve combinatorics problems using Z3Py. 
adjacency constraints:: 
 • For each edge (u, v), ensure that the colors of u and v are different.• Specific Vertex Color Constraint:• Vertex 1 must be colored with color A (0).• Cardinality Constraint:• The number of vertices colored with color B (1) must be exactly 2.Step 3: Model Counting:• Use Z3 to find all possible assignments that satisfy the constraints.• Step 2: Define Variables • We need variables to represent who is sitting in each seat (excluding the fixed seat 0). • Create integer variables for each seat (from seats 1 to 4).• Each variable will represent the guest sitting in that seat.Step 3: Encode the Guests • Since the twins are identical, we'll represent them with the same identifier. Find the number of functions $f(x)$ from $\{1, 2, 3, 4, 5\}$ to $\{1, 2, 3, 4, 5\}$ that satisfy $f(f(x)) = f(f(f(x)))$ for all $x$ in $\{1, 2, 3, 4, 5\}$. 
datasets used for fine-tuning: 
 We now present our methodology for generating datasets of problems with correct Z3Py solutions.To address the lack of training data for Z3py, we generate fully synthetic pairs of counting problems with corresponding Z3py solutions. We focus on four classes of ground sets: Sequences, permutations of the set {1, 2, . . . , n}, numbers in base k, and subsets of the set {1, 2, . . . , n}. For each object, we define a set of supported constraints, where each constraint includes a natural language description and corresponding Z3py code. Constraints can be applied to the object itself or to an integer parameter derived from the object, such as the sum of the sequence or the number of inversions in a permutation.When generating a problem, we sample a ground set and a set of constraints, where each constraint has a probability of 1/2 of being negated. These constraints are then combined to form a problem and a Z3Py solution. We run the solution and retain only the problems that finish within the time limit, returning a non-zero answer. Below is an example of a generated synthetic problem:A subset of the set {1, 2, . . . , 6} (no two elements in the subset are consecutive integers) and (no three elements in the subset form an arithmetic progression) and (the subset sum is not divisible by 10). Count the number of valid objects.Here is the relevant part of the corresponding Z3py solution generated by our dataset generator:1 from z3 import * 2 subset = [Bool(f'subset _ {i}') for i in range(6)] 3 subset _ sum = Sum([If(subset[i], i + 1, 0) for i in range(6)]) 4 constraint _ 1 = And([Not(And(subset[i], subset[i + 1])) for i in range(6 -1)]) 5 constraint _ 2 = And([Not(And([subset[i], subset[j], subset[k]])) \ 6 for i in range(6) for j in range(i + 1, 6) \ 7 for k in range(j + 1, 6) if j -i == k -j]) 8 constraint _ 3 = subset _ sum % 10 == 0 9 constraint _ 4 = Not(constraint _ 3) 10 constraint _ 5 = And(constraint _ 2, constraint _ 4) 11 constraint _ 6 = And(constraint _ 1, constraint _ 5)12 solver = Solver() 13 solver.add(constraint _ 6)We found that fine-tuning on raw synthetic problems leads to severe overfitting to the specific format of those problems (almost perfect scores on our validation synthetic problems), while degrading the performance on real problems from the NuminaMath dataset [8] . To address this issue and make the problem statements sound more natural, we rephrase the problems using a language model.To minimize the number of incorrect rephrasings, we use a technique similar to rejection sampling. For each problem, we prompt the language model to generate a naturally sounding problem statement. We then prompt it again to generate a new Z3py solution from the rephrased statement. We verify that the original and generated solutions produce the same integer answer. If they do, we count both the rephrasing and the new solution as correct.In our experiments, we rephrased each problem twice and sampled three solutions for each rephrasing at temperature 0.5. For example, for the problem above, we generated the following rephrasing.Consider the set {1, 2, 3, 4, 5, 6}. How many subsets can be formed such that no two elements in the subset are consecutive integers, no three elements form an arithmetic progression, and the sum of the elements is not divisible by 10?We constructed training sets containing 2624 and 2883 rephrased synthetic problems, for GPT-4omini and GPT-4o, respectively. We generated rephrasings and solutions for GPT-4o-mini and GPT-4o independently to avoid confounding our results with knowledge transfer between the models.We applied our approach to problems from the NuminaMath dataset [8] . We excluded the syntheticmath portion, as it contains rephrasings (which may be incorrect) of other problems. We retained only problems with integer answers and used the GPT-4o-mini model to filter for counting problems (which are potentially solvable using our Z3py approach). For validation, we selected the amc-aime portion of the dataset, resulting in 145 problems after filtering. The remaining 8935 filtered problems were used to construct a baseline training set.For each problem in the training set, we generated 3 Z3py solutions for rejection sampling, using GPT-4o-mini and GPT-4o, respectively. This process left us with 2624 training problems for GPT-4o-mini and 2883 training problems for GPT-4o.to count the number of elements in the subset defined by the constraints. All problems mentioning minimization or maximization must be discarded. 4. A natural solution must involve going through all the elements of the ground set and checking if they meet the constraints. 5. The problem must be challenging to solve analytically; i.e., it should not be possible to solve it by a simple formula or direct calculation. 6. The problem statement must not contain any URLs or diagrams.Do not try to solve the problem. Carefully review each of the listed conditions. All words in the conditions are important.Please provide a clear answer by putting "Yes" (without quotes) in \boxed{} if the problem satisfies the criteria, and "No" in \boxed{} otherwise. If you are not sure, answer "No."Example Problem 1 ** Problem ** : Consider the following undirected graph G with 5 vertices:EQUATIONWe need to assign colors to the vertices using colors A, B, and C, such that: 1. Adjacent vertices must have different colors.2. Vertex 1 must be colored with color A.3. The number of vertices colored with color B must be exactly 2.How many valid colorings of the graph satisfy these constraints? ** Solution ** :Step 1: Define Variables:• For each vertex, define an integer variable representing its color.• Colors are encoded as integers: A = 0, B = 1, C = 2.Step 2: Specify Constraints:1. Color Assignment Constraints:• Each vertex's color variable can take on values 0, 1, or 2. 
evaluation: 
 We fine-tuned both GPT-4o and GPT-4o-mini for one epoch using a standard learning rate on three datasets: (i) Problems filtered from the NuminaMath dataset, (ii) synthetic problems, and (iii) a mix of NuminaMath and synthetic problems.Z3 solutions We evaluated a total of ten models: four before fine-tuning and six after fine-tuning. To assess their performance, we generated 32 samples with a temperature of 0.7 for each of the 145 problems in the validation set. We ran the default and fine-tuned versions of GPT4o-mini and GPT4o with a few-shot prompt specifically asking for solutions written in Z3py. We include two example problems with solutions in all prompts. We additionally ran the default models with a Z3py reference prepended to the prompt. A solution was considered correct if it executed properly using Z3py and returned the correct answer. We first compare the models in the pass@k metric [9] . For each k, ranging from 1 to 32, we calculated the expected number of problems solved at least once given that we subsample the results on each problem using k samples. For each problem solved x times out of 32 trials, the probability of at least one success in k attempts is given by:P (solved) = 1 - 32-x k 32 kSumming the probabilities across problems provides the expected number of solved problems per k.We note that for GPT-4o, fine-tuning on synthetic data outperforms fine-tuning on the NuminaMath dataset, and fine-tuning on a mix of the two outperforms both. For GPT-4o-mini, the results are less clear, as fine-tuning on synthetic data seems to produce the best performance. We also observe that GPT-4o-mini fine-tuned on synthetic data performs better than GPT-4o.Model Score (maj@32) To enable a fair comparison in a setting where the answers are unavailable, we also calculate the number of correctly solved problems for each model using the majority vote across the 32 samples.The relative performance of the models aligns with the pass@k metric, supporting the intuition that a model which solves a problem correctly more frequently is more likely to have a majority of correct samples.General problem solving Additionally, we prompted the models to generate any Python code, potentially using SymPy, Z3Py, or any other library. On our validation data set, all fine-tuned models managed to solve additional tasks that were not solved without our fine-tuning: The strongest difference is on GPT-4o, where fine-tuning with NuminaMath yielded 7 additional solutions on our validation set. Of those solutions, 5 used Z3Py. For GPT-4o-mini, NuminaMath and Numina-Math+Synthetic both yielded 4 extra problems solved, where all of the solutions used Z3Py. 
conclusion and future work: 
 We presented an algorithm for synthesizing training data for fine-tuning LLMs to solve mathematical problem statements using SMT solvers. Our experimental results demonstrate that fully synthetic random problem statements can be helpful for tasks with less readily available training data. Furthermore, we showed that fine-tuning on SMT-based solutions improves the general problem solving capabilities of LLMs. Future work includes more advanced synthetic problem statements, using fine-tuned models to bootstrap harder datasets from existing problem statements, as well as applying the approach to other less well-known libraries for mathematical reasoning in addition to Z3Py. 
 
 Appendix: Rephrasing for Synthetic ProblemsRewrite the following problem as if it were a question in a middle school math competition. Ensure that the rewritten question is equivalent to the original while sounding natural.First, analyze the constraints in the initial problem. Be very careful, some constraints can contain double negatives. Provide the final statement formatted as follows: '''statement'''.Z3 Solver (Fine-Tuning & Evaluation)You will be provided with a combinatorial problem related to enumeration. Your task is to write Python code using the Z3 library to solve the problem and print the correct answer.Requirements You are given the following problem: \n\n{problem} \n\n Determine if it is an enumeration problem. By "enumeration," we mean a complete, ordered listing of all the items in a collection. More precisely, the problem must satisfy each of the following conditions:1. The problem deals with a clearly and explicitly defined, finite set of objects (like permutations, combinations, bounded sequences, graphs, etc.). Problems involving real numbers, functions, infinite sets, etc., are not considered enumeration problems. 2. There must be clear and explicit constraints on individual objects, expressible in first-order logic, that define a subset of the ground set. All problems mentioning constraints on subsets of the ground set must be discarded.To solve this problem using the Z3 library, we need to model the constraints on the function \( f \) such that \( f(f(x)) = f(f(f(x))) \) for all \( x \) in \(\{1, 2, 3, 4, 5\}\).Here's how you can implement this: 38th Conference on Neural Information Processing Systems (NeurIPS 2024). 


Decision: All reviewers are in support of this paper, and it will make a great contribution to our workshop.

Reviews: review: title: title: Review
main_review: main_review: This paper proposes an algorithm for synthesizing counting problems that require Z3py to solve.
With the synthesized data, they fine-tune GPT-4o and GPT-4o-mini to use Z3py.
The fine-tuned models are both better at solving problems using only Z3py and using a series of tools like sympy, Z3py and others.

**Weakness:** Novelty is limited. While People haven't done that for Z3py, this kind of data synthesis is common and used for many other tools/libraries.

**Strength:** The performance is good, and SMT seems to provide a better guarantee for the data synthesis quality. I'm curious how this can be extended beyond counting problems.
title: title: Practical method for equipping LLMs with counting abilities
main_review: main_review: **Summary** 

This paper explores the use of an SMT solver, Z3Py, in order to address the shortcomings of LLMs on counting problems (e.g., "how many ways can a chessboard be tiled with dominoes?"). Models are asked for python code which utilizes Z3Py in order to output the answer to a particular counting problem. The authors introduce a method of synthetic data generation -- problems with Z3Py-based solutions -- over a reasonably broad collection of counting problems (based on sequences, sets, etc.) They evaluate three copies of gpt4o and gpt4o-mini on the aime-amc subset of the NuminaMath dataset: One finetuned on just (a curated subset of) NuminaMath, one just with synthetic data generated from NuminaMath, and one with a mix of both. Fine-tuning on synthetic (or a mix) produces the best performance. When prompts are relaxed to not mandate Z3Py solutions, the fine-tuned models still outperform the base models and even provide new solutions not using Z3Py.

**Pros**
* Writing is easy to follow
* Straightforward and natural idea
* Presents an interesting and practical method of equipping LLMs with computational abilities
* Demonstrates that this method is successful (with these models on this data)
* The rephrasing idea is interesting

**Cons**
* 102: "We found that..." Worth including the details of this experiment.
* 116: "We generated..." More specifics on this should be included.
* Missing related work -- What else has been done in this area? 
* Limited to one dataset and gpt.
* NeurIPS Checklist?
title: title: Reviewer of "LLM Training Data Synthesis for More Effective Problem Solving using Satisfiability Modulo Theories"
main_review: main_review: This paper investigates the intersection of mathematical reasoning with Large Language Models (LLMs), particularly focusing on the use of Z3Py, to solve counting problems. The authors chose Z3Py which excels at counting problems with a 25 small enough answer. This eliminates possible concerns and answer extraction issues that exist for math reasoning datasets such as MATH, Algebra.  A novel and interesting approach for generating synthetic training data designed to fine-tune LLMs is presented, improving their mathematical problem-solving capabilities.
title: title: Clear and relevant paper, perhaps in need of some additional experiments or metrics
main_review: main_review: This paper seeks to improve pre-trained LLMs' abilities to use a SMT solver (Z3) to solve simple combinatorics problems.
The primary contribution is a synthetically generated dataset of combinatorics problems paired with Z3 solutions.
Importantly, the authors correctly evaluate on a held-out set of real problem instances; the synthetic problems are only used to train on.

Pros:
- The main part of the paper is well written. The description of the domain and the proposed solution is clear.
- The results are somewhat interesting: they do suggest that even simple ways of generating synthetic Z3 instances can help the models a fair bit.
- The paper is relevant to the topic of the workshop, as SMT solvers are used throughout formal mathematics and automated theorem proving, and recent work has shown that interfacing with them is crucial when using LLMs to automate math.

Cons:
- I'm missing a related work section; I understand this is a short paper and that there is not a lot of space to work with but I would appreciate an appendix being added to compare this work to other prior and contemporary research.
- I'm not convinced pass@k is a meaningful metric here; it's used in code generation because you can tell when you get a correct program (because it passes the unit tests). Thus obtaining 1 correct program in 20 samples is still meaningful. In this domain, you can't tell which of your 20 samples is the correct one (without cheating), so it's not necessarily a meaningful metric.
- I would have liked to see more interpretation of the results. For example, looking at the figure it appears to me that the primary benefit is improved (semantic) diversity in the outputs, particularly when comparing the different finetuning methods (e.g., gpt4o syntheticdata with vs. without numinamath is identical at pass@1 but several % different at pass@20). Maybe quantifying/measuring this in some way would reveal more interesting insights.
- I personally find the use of the words "novel algorithm" a bit too strong to describe a simple way to synthetically generate data from a language for which you have a grammar.
- I would have liked to see some analysis of what parts of your synthetic data it was that actually helps the models - e.g. is there some part of the Z3 grammar that has poor coverage in real data, but your synthetic data covers well?

Overall, I think this paper is a good candidate for the workshop. I look forward to reading the paper again once it has been fleshed out a bit more.