MathDSL: A Domain-Specific Language for Concise Mathematical Solutions Via Program Synthesis

Authors: sagnik  anupam
maddy  bowers
omar  costilla-reyes
armando  solar-lezama
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-25 07:59:25

Abstract: We present MathDSL, a Domain-Specific Language (DSL) for mathematical equation solving, which, when deployed in program synthesis models, outperforms state-of-the-art reinforcement-learning-based methods. We also introduce a quantitative metric for measuring the conciseness of a mathematical solution and demonstrate the improvement in the quality of generated solutions compared to other methods. Our system demonstrates that a program synthesis system (DreamCoder) using MathDSL can generate programs that solve linear equations with greater accuracy and conciseness than using reinforcement learning systems. Additionally, we demonstrate that if we use the action spaces of previous reinforcement learning systems as DSLs, MathDSL outperforms the action-space-DSLs. We use DreamCoder to store equation-solving strategies as learned abstractions in its program library and demonstrate that by using MathDSL, these can be converted into human-interpretable solution strategies that could have applications in mathematical education.

Main paper: 
 introduction: 
 Building machine learning models that can replicate human reasoning abilities in symbolic domains, such as algebra or arithmetic, is a challenging problem that researchers continue to face today [7] . Even large models that exhibit state-of-the-art performance on language modelling datasets, like GPT-4, exhibit much poorer performance on mathematical exams involving reasoning tasks [6] . Improving these systems to perform well on reasoning tasks often requires extensive usage of techniques such as chain-of-thought reasoning and training on large datasets of mathematical data, which is expensive in both time and cost.Improving machine learning models' mathematical reasoning ability may yield significant interpretability that can provide educational benefits, as studies have shown that automated tutor systems can yield similar or greater educational gains than human tutors [11] . Additionally, such improvements, when extended to more complex mathematical domains, can aid in developing software for researchers by helping describe the behavior of previously unknown functions [4] . Thus, an important research goal is to develop machine-learning systems that write step-by-step solutions to mathematical problems while being as efficient as possible regarding training data and compute.For simple algebraic domains like linear equations, many step-by-step solvers rely on manually written heuristics. However, those have been shown to have surprising blind spots that fail to account for solving rare equation cases [7] . In recent years, attempts to help models learn neurosymbolic reasoning in mathematical domains have led to the development of specific reinforcement learning techniques, like the Contrastive Policy Learning (ConPoLe) algorithm [7] . When presented with an equation, ConPoLe uses reinforcement-learning techniques to query the search space and find the most promising next step until it synthesizes a complete step-by-step solution.However, in the linear equations domain, the solutions generated using ConPoLe often tend to be elaborate and unwieldy [5] , and often contain unnecessary steps that may confuse program users, as demonstrated by the ConPoLe solution in Figure 1 . Recent research has demonstrated that humans find solutions simplified using skill-based, higher-level abstractions very useful [9] . One approach that uses this idea is a theorem-proving language, Peano [8] , which changes ConPoLe's action space to a finite set of valid axioms and discovers tactics by analyzing a batch of ConPoLe-generated solutions. However, solution discovery in Peano is limited to a few types of equations due to the limitations of the tactic language, and in practice, the discovered tactics are quite simple [8] . Another approach, Lemma [5] , leverages the idea of abstraction learning by examining several ConPoLe solutions generated on a training dataset (using its original action space) and building abstractions that ConPoLe can use to solve equations on a test dataset. However, Lemma requires training on a large dataset of previously generated ConPoLe solutions to build high-quality abstractions. Hence, it is not able to leverage the power of the abstractions the first time it solves tasks in a new domain.Equation ((1 + 2x) + 3x) = 4 ConPoLe Solution ((1 + 2x) + 3x) = 4 1 + (2x + 3x) = 4 ((1 + (2x + 3x)) -1) = (4 -1) (((2x + 3x) + 1) -1) = (4 -1) ((((2 + 3) * x) + 1) -1) = (4 -1) (((2 + 3) * x) + (1 -1)) = (4 -1) (5x + (1 -1)) = (4 -1) (5x + 0) = (4 -1) 5x = (4 -1) (x * 5) = (4 -1) (x * 5) = 3 ((x * 5)/5) = (3/5) (x * (5/5)) = (3/5) (x * 1) = (3/5) x = (3/5)Lemma Solution((1 + 2x) + 3x) = 4 (3x + (1 + 2x)) = 4 (3x + (2x + 1)) = 4 4 = (3x + (2x + 1)) 4 = ((3x + 2x) + 1) 4 = ((3 + 2) * x + 1) 4 = ((3 + 2) * x) + 1 4 = (5x + 1) (5x + 1) = 4 5x = 3 x = (3/5)DreamCoder + MathDSL Solution ((1 + 2x) + 3x) = 4 (5x + 1) = 4 5x = 3 (x * 5)/5 = (3/5) x = (3/5) 
methods: 
 Previous research on developing machine-learning models for mathematical equation solving has shown that neural models perform poorly on arithmetic tasks unless task-specific components are used [13] . To improve the performance of neural models, recent approaches have examined if it is possible to use these models in sequence-to-sequence contexts by first converting mathematical expressions into Abstract Syntax Trees (ASTs), and then into prefix sequences derived from these trees [4] . Extending this idea, MathDSL modifies the problem domain from algebra to algebraic manipulation and uses primitives that describe operations performed on the prefix form of equations.Our approach involves searching the space of all possible programs in MathDSL to find the correct program that converts the input from the prefix form of the equation to the solution state string. Thus, the entire solution to the equation is synthesized at once, unlike previous reinforcement learning systems, which attempt to find the next step in the solution by choosing from the existing action space. For searching the space of MathDSL programs, we use DreamCoder [2] , a library-learning framework designed for use on inductive program synthesis problems [12] . We use DreamCoder with the Stitch library learning algorithm [1] (as described in [3] ). A complete description of the program synthesis system and its components has been provided in Appendix A.We provide DreamCoder with MathDSL, our DSL that encodes a set of mathematical axioms, along with some elementary equation manipulation operations, as basic programming primitives. These primitives can then be composed to form more complex operations that can fully convert a linear equation into its corresponding solution state. MathDSL performs manipulations on equations in prefix form and comprises three types of primitive operations: tree operations, arithmetic operations, and index operations. Tree operations, such as tree rotations and distributive operations, are defined as operations performed on the equation's tree structure that rearrange the equation tree to make future simplifications easier without introducing additional nodes. Arithmetic operations, like dividing or multiplying both sides of the equation by a term, introduce additional nodes in the equation tree.Index operations are helper operations used to help determine the indices for accessing the specific subtrees of an equation AST on which tree and arithmetic operations act. In MathDSL, arithmetic operations can only accept arguments that are subtrees of the current tree, and tree operations can only be performed on the current equation tree's subtrees. This constraint helps us avoid having to discretize the space of integers or real numbers in the DSL, which would make the search space much larger and make program synthesis prohibitively expensive. In our experiments, the index operations in MathDSL can generate integer constants from 0-110, a range much larger than the number of subtrees in any equation in our dataset. The complete list of MathDSL's primitive operations is provided in Appendix B, and an example program for solving an equation is provided in Figure 2 . 
conciseness metric: 
 Here, we describe a metric to measure the conciseness of solutions generated by different equationsolving systems. We use an AST-based metric to ensure that large expressions were not added or transposed to different sides of the equations. We define the metric function as follows, for a solution s with n steps of an equation e:f (s) = n-1 i=1 max(|s i .lef t -s i+1 .lef t|, |s i .right -s i+1 .right|, 1)Here, s i refers to the equation tree of the equation at the i-th step of the solution, while x.lef t and x.right refer to the size of the left and right subtrees of x, respectively, where the size is defined as the number of subtrees of a tree (including the original tree). For a given equation, a solution with a smaller value of f (s) indicates a more concise solution.As demonstrated in Figure 1 , solutions that introduce large terms into the equation tree without prior simplification make the solution more difficult to interpret, especially in a pedagogical context. Hence, this metric function penalizes solutions that introduce complicated expressions in a solution step. Since this function assumes a cost of at least 1 occurring per step and does not normalize for length, it rewards shorter solutions over longer solutions. As a result, the function penalizes solutions that take many steps to simplify expressions without changing tree size (such as the ConPoLe solution in Figure 1 ). However, it can also reward overly-compressed solutions. A description of metric function limitations can be found in Appendix C.For a given equation e, a target model A, and a baseline model B, we use the metric function to compare two solutions to the same equation by measuring the relative improvement or decline in the metric compared to the baseline model. Let s A and s B denote the solutions generated by the target model and the baseline model, respectively. Then, the relative improvement or decline in performance is measured by the score:C(s A , s B |s A , s B both solve e) = f (s B ) -f (s A ) f (s B )We refer to this score as the C-score of A and B on e. We report the mean C-score over all equations solved by both the target and the baseline models. Positive mean C-scores indicate that the target model generates more concise solutions than the baseline model on average. In contrast, negative mean C-scores indicate that the target generates less concise solutions than the baseline on average. To measure conciseness in our experiments, we take ConPoLe as our baseline model and compute the C-scores of Lemma and DreamCoder (considering each DSL separately) with respect to ConPoLe. 
experiments and results: 
 For evaluating the performance of MathDSL in our program synthesis system and compare its performance to Lemma and ConPoLe in terms of accuracy and conciseness, the models were evaluated on a variant of the Cognitive Tutor Algebra dataset [7] . We note that it is extremely difficult to normalize the performance of DreamCoder and its reinforcement learning alternatives, since DreamCoder has previously shown the ability to learn useful abstractions from a few carefully chosen tasks [2] , while both ConPoLe and Lemma rely on generating ≈ 10 6 equations from the equation templates during training. Instead of training Lemma and ConPoLe from scratch on our training set, which may reduce their efficacy by training them on a smaller set of equations, we simply evaluated the final trained models on the infix-notation form of our train and test datasets to observe if the models can discover the equation solutions. Our evaluation also allowed Lemma to use all the abstractions it had discovered during its original training. Additional details about the experiments are in Appendix D, and some abstractions discovered by DreamCoder are described in Appendix E.Additionally, to demonstrate that the improved performance is due to using the MathDSL and not due to DreamCoder being an inherently more powerful system, we also run experiments with DreamCoder using ConPoLe and Lemma's action spaces as DSLs. In our first experiment, we treat each axiom listed by [7] in Appendix A as a separate primitive in a new DSL (titled ConPoLeDSL). In our second experiment, in addition to the aforementioned axioms, we use the 15 abstractions discovered by [5]  
conclusions: 
 In this paper, we introduced MathDSL, a domain-specific language designed for solving linear equations via program synthesis. Our results demonstrate that DreamCoder combined with MathDSL significantly outperforms existing models like ConPoLe and Lemma in terms of both accuracy and solution conciseness. Specifically, DreamCoder+MathDSL achieved a testing set accuracy of 90.70% and produced solutions that were on average 48.59% more concise than those generated by ConPoLe, as evidenced by the C-score metric. Furthermore, MathDSL proved to be highly efficient in terms of training data, requiring only 198 equation templates compared to the ∼ 10 6 equations required by ConPoLe and Lemma. The system also produced human-interpretable solution strategies, unlike ConPoLe, which lacks a structured abstraction mechanism to yield human-interpretability.Our experiments using ConPoLeDSL and LemmaDSL confirmed that MathDSL's design, rather than the underlying DreamCoder framework alone, was responsible for the improved performance. The experiments showed that neither ConPoLeDSL nor LemmaDSL enabled DreamCoder to generate concise solutions with comparable accuracy.In conclusion, MathDSL offers a novel approach for generating interpretable and concise solutions to mathematical equations, with broader applications in educational tools and automated reasoning systems. Future work can explore extending MathDSL to more complex mathematical domains, such as calculus or discrete mathematics, and its potential applications in automated tutoring systems where human-like solution strategies are valuable. 
 
 Appendix: For performing program synthesis in our domain-specific language, we use DreamCoder [2] , a wake-sleep learning algorithm, alongside Stitch [1] , a library-learning algorithm. DreamCoder comprises an initial library L 0 containing the "base primitives" defined in the domain-specific DSL, which in our case would refer to MathDSL, ConPoLeDSL, or LemmaDSL. At the end of the process, it returns a learned final library, L f , which contains the various subroutines (or abstractions) generated by composing the program primitives, which aided it in solving multiple tasks in the domain. By examining the new primitives DreamCoder assigns to L f , we can study the equationsolving procedures and algorithms it has "learned", and compare them to similar human techniques. Additionally, DreamCoder also returns a neural search model Q(ρ|t, L). When given a task t and library L, Q can generate several potential solution programs ρ which have a high probability of solving the given task [2] .In order to construct Q, DreamCoder first assigns a real-valued weight θ L to each library function l ∈ L. Then, for every l, after normalizing weights, we have a production probability P [l|L, θ L ].Then for any program ρ comprising of library functions l, we have prior probability of ρ given by:EQUATIONThen, a neural search model Q is constructed to predict the programs that can solve a given task t using functions from the current library [12] . This probability is expressed as P [ρ|t, (L, θ L )] (probability of program conditioned on task, library, and library weights), so the model can be expressed in the following manner at iteration i of training:EQUATIONHere, the probability P [t|ρ] is the likelihood the task is solved by the program under consideration. Thus, programs are sampled from the prior and executed to compute the posterior probabilities of solving tasks. Then, Q is trained to assign higher probabilities to programs with higher posterior probabilities [2] .DreamCoder divides this program into the following three stages: wake, sleep(abstraction), and sleep (dream). Firstly, in the wake stage, a random minibatch of tasks is sampled, and programs with higher posterior probability are found using beam search.Secondly, in the abstraction stage, the programs discovered via beam search are held constant, and the library is rewritten to include new primitives that compress both the programs as well as the description length of the updated library. For refactoring, we use Stitch, a corpus-guided top-down synthesis algorithm which has been shown to outperform DreamCoder's library rewriting algorithm in certain domains [1] . Stitch uses a utility function for scoring abstractions given a corpus and a rewrite strategy. This utility function is calculated in Equation 17 in [1] as follows:EQUATIONIn this equation, P is the corpus while R is the rewrite strategy, while A is the abstraction for which utility is being computed. The summation term in the equation is summed over all programs p in the corpus P.Thirdly, in the dream stage, Q is trained to assign a high probability to programs ρ with higher posterior probability. This is done by having DreamCoder generate its own examples: "replays" of tasks it has already solved successfully, and "fantasies" of tasks which it creates on its own. These fantasies are created by generating programs by combining various primitives in its own current library, executing these programs on various sample inputs to generate outputs, and passing the (input, output) data points to the neural model to train it until it learns to accurately compute the probability for programs [2] .MathDSL's primitive operations are listed in Table 2 , alongside their type annotation (which Dream-Coder utilizes for synthesis). Table 2 also describes whether an axiom comparable to our primitive is present in ConPoLe's action space, while Table 3 describes ConPoLe axioms that were omitted from MathDSL since they can be expressed using semantically equivalent programs. In the primitive name, given an equation e to solve and an integer x, we define y as a subtree of e uniquely identified by the integer x. Then, the complete list of all primitive operations in the DSL is as follows: We don't need to encode reflexive equality since our commutativity operator, swap, rearranges 2 = x =⇒ x = 2. assoc Associativity rules are considered while performing left and right rotations, so a separate operation is unnecessary. sub_comm Left and right rotations handle reordering arguments within the same operation for all four arithmetic operations (e.g. a+b+c = (a+c)+b)). sub_subThe model can insert 0 via swap and addzero or subzero and simplify the constants to convert from positive to negative constants and vice versa. Hence the equivalence between +(-x) and (-x) does not need to be explicitly encoded. zero_div While zero divided by a non-zero constant will always be 0 arithmetically, for an expression x, our system can instead multiply 0/x by x and rotate to obtain 0 * (x/x) and then simplify to get 0 * 1 = 0. There are two main drawbacks of the conciseness metric function f described in Section 3. The first drawback is that since it tends to generally reward shorter solutions, it may provide solutions with large jumps, like Ax + B = C =⇒ x = (C -B)/A, with similar scores as solutions like Ax + B = C =⇒ Ax = C -B =⇒ x = (C -B)/A, even though the latter is arguably a clearer and more explanatory solution.We argue that our methods allow for the latter to be easily recoverable from the former since our abstractions are comprised of functions composed together. Hence we can decompose the functions in the abstraction as we wish, to adjust for the mathematical maturity of the student, and thus we can obtain the latter solution from the former. On the other hand, we cannot assign equal metric function values to a solution like 2x + 5 = 7 =⇒ 2x + 5 -5 = 7 -5 =⇒ 2x + 0 = 7 -5 =⇒ 2x = 7 -5 =⇒ x = 1 and a solution like 2x + 5 = 7 =⇒ 2x = 7 -5 =⇒ x = 1 and say that the abstractions required to generate the latter solution are easily recoverable from the former. The statement does not hold because if the abstractions are not already present in the learned library of the model, it may lead to the former solution never being discovered by the program synthesis model in the first place. The equation could very well not be solved within the time specified since the syntax tree of the program required to generate the former solution is too deep, and thus never be found by the program synthesis model.The second drawback is that the metric function is not as helpful for comparing solutions to two different equations, since equations have different types and different original equation tree sizes. Complex equations with larger tree sizes will require more steps to solve than simpler equations, and as a result, we observe that the scores are not directly comparable. However, we have developed the notion of C-Scores in Section 3 to compensate for this drawback, as we simply take the mean of the percentage difference in the metric function value on solved problems across the entire dataset. This approach helps measure the performance improvement of a model across a wide variety of problems, thus accounting for the difficulty in directly comparing two different solutions.Future work could explore refining the metric to better account for pedagogical clarity and solution complexity while maintaining the efficiency of program synthesis. Approaches for overcoming these limitations may involve adding additional terms to the C-Score ensure that the length of the target solution is at least some constant k, where k is proportional to the complexity of the equation being solved. Additionally, researchers can conduct a user study that evaluates when students start to consider an equation's solution to be too short. Then, the different terms in the C-Score can be weighted in a manner consistent with the results of the study.Cognitive Tutor is a mathematical education software developed by Carnegie Learning based on the ACT-R theory of cognition [10] . For the evaluation of the ConPoLe model on the equations domain, the authors constructed a dataset of 290 equations (each of a different equation type) that was built from Cognitive Tutor templates. For our evaluation, a modified dataset using 284 of the Cognitive Tutor equation types was used, as 6 of the equations are unsolvable. We split the dataset into a training dataset with 198 randomly selected equation templates and a test dataset with 86 held-out problems. Our synthesis system was run for 25 iterations with 10 5 recognition model training steps and an enumeration timeout of 1000s on 95 CPUs. Evaluation on the held-out test dataset was conducted once every 3 iterations.As described in their respective papers, ConPoLe and Lemma were originally trained with (infixformat) equations sampled from these Cognitive Tutor equation templates that had their constants chosen at random. Both ConPoLe and Lemma were trained for 10 7 environment steps, which are defined as queries where the environment indicates whether a problem has been solved or lists all allowed actions in the next step [7] . This training procedure results in ≈ 10 For each model, the solutions used for the C-scores were generated as follows: for ConPoLe and Lemma, each step discovered by the model was selected as a solution step, and its C-score was computed accordingly. DreamCoder's solutions were programs in the MathDSL, ConPoLeDSL, and LemmaDSL that comprised many subprograms utilizing its learned abstractions (equationsolving strategies). These abstractions often solve equation templates from beginning to end in a single program. We make the first step in our solution the initial equation passed to the program. The abstractions are composed of several lambda functions generated by Stitch via lambda-aware unification, comprising a chain of function calls to primitive functions in the DSL. While generating solutions from programs for measuring conciseness, if the result of the lambda function is not passed as an argument to a DSL primitive function (which further simplifies the expression), we save the result of a lambda function call as a step in our final solution. By doing this, we ensure that only the highest-level lambda functions are considered while generating solution steps, and not intermediate results later simplified by other primitives. Hence, our solutions utilizing these abstractions have multiple steps, even when the abstractions by themselves can directly solve the equation template. Examples of discovered abstractions are listed in Appendix E. However, when parsing DreamCoder solutions by evaluating the outputs of intermediate lambda functions in the solution program, we observe that occasionally, an abstraction may be applied to the equation that does not modify the equation state at all. In such cases, DreamCoder produces duplicate steps in the solution since the program "halts" at a certain equation state before modifying it with other abstractions later in the program. If we perform a post-processing step that de-duplicates the steps in the equation solution, the conciseness metric is observed to be as follows in Table 4 .Training This section describes some of the useful abstractions or equation-solving strategies that are generated by Stitch and learned by DreamCoder in different domain-specific languages at the end of 25 iterations. The first argument passed to the primitive is a string containing an equation in prefix form, and the second argument is an integer containing the index of the subtree on which the function acts.Note that whenever the term is enclosed by square brackets (for example, [x = A + B]), this means that the term has had the simplify operation applied to it in its result (for example, if A = 3 and B = 5 in the original equation, executing the abstraction generates x = 8). The Conversion Formula Examples columns in Tables 5, 6 , and 7 show an example transformation that can occur when the program is applied to a specific equation template. The output may differ if the same program is applied to a different equation template. A more detailed description of the ConPoLe [7] and Lemma [5] primitives can be found in the original works.Description #(lambda (#(lambda (simplify (dist (#(lambda (swap (simplify $0 0) 0)) (rrotate (swap (div (#(lambda (simplify (dist (rrotate $0 1) 1) 0)) (mult (swap (#(lambda (simplify (dist (rrotate $0 1) 1) 0)) $0) 4) 3)) 3) 5) 4)) 1) 0)) (sub $0 5)))(A/x) + B = C → x = [A/(C -B)]Subtract B from both sides, simplifies the equation, then multiplies both sides by x, and then simplifying to calculate x's value.#(lambda (#(lambda (lrotate (swap (#(lambda (swap (simplify $0 0) 0)) $0) 1) 1)) (#(lambda (simplify (dist (rrotate $0 1) 1) 0)) (add $0 5))))Ax -B = C → Ax = [C + B]Add B to both sides, eliminate B from lefthand side and simplify right-hand side. #(lambda (#(lambda (swap (simplify (rrotate (swap (div (swap (simplify (rrotate $0 4) 0) 0) 3) 5) 4) 0) 0)) (#(lambda (simplify (dist (rrotate $0 1) 1) 0)) (sub $0 5))))Ax + B = C → x = [(C -B)/A]Subtract B from both sides, simplify both left-hand and righthand sides, and then divide by A.  



Reviews: review: title: title: Review for MathDSL
main_review: main_review: The paper presents MathDSL, a domain-specific language designed to solve linear equations through program synthesis. By integrating MathDSL with the DreamCoder system, the approach outperforms existing methods like ConPoLe and Lemma in terms of both accuracy and solution conciseness. MathDSL generates human-interpretable, reusable abstractions that can be applied to educational tools and automated reasoning systems. It also introduces a metric to measure the conciseness of solutions. 

One advantage of MathDSL is its ability to generate concise solutions compared to other systems like ConPoLe and Lemma. By reducing unnecessary steps, it produces solutions that are clearer and easier to interpret. Another benefit is its higher accuracy in solving linear equations, achieving a testing accuracy of 90.7%, which is an improvement over previous methods. Also, MathDSL allows for the creation of human-interpretable abstractions, which might be useful for other downstream applications such as education.

However, MathDSL has some drawbacks: First, it is currently limited to solving linear equations, meaning that its use is restricted unless extended to other mathematical domains. The conciseness metric, while useful, can reward solutions that are overly compressed, potentially skipping important steps that aid understanding, especially in an educational setting. Also, developing a domain-specific language like MathDSL involves significant work, such as defining primitives and abstractions, which may be difficult for more complex math problems.
title: title: Well written paper for a narrow domain of limited usefulness
main_review: main_review: This paper does two things to solve problems in the ConPoLe equations benchmark on equational reasoning:
* Apply the DreamCoder learning algorithm (with the faster Stitch component)
* Change the DSL to a new MathDSL to better support reasoning

They show that the two combined perform better than the two previous methods, Lemma and ConPoLe.  They also have an ablation showing that the new MathDSL is very important, in that DreamCoder + Stitch does worse with the old DSL.

The paper is clear and tidy.  It is well written and they get their point across.

I have to admit, I'm a bit disappointed by the results of this paper.  DreamCoder has always seemed like an interesting approach to problems like this, but the fact that it is so sensitive to the initial DSL is very disappointing, especially since the point of DreamCoder (and Stitch) is that it can learn new DSLs.

So it seems that the main contribution of this paper was the new MathDSL for reinforcement learning on a toy problem that frankly is not interesting by itself.  One can easily use existing software, or even write a custom Python program, to solve problems in this toy benchmark.  Unfortunately, I don't see what we have learned from this experiment that is useful outside of this toy domain.  Does this paper hold clues for how to design DSLs for other mathematical domains?  Does this paper present ideas for how to make DSLs that jumpstart DreamCoder's performance on other problems?  It is not even clear to me that the ideas from this paper would directly help in the very similar toy benchmark INT (https://github.com/albertqjiang/INT) which already has strong solutions (https://arxiv.org/abs/2206.00702).

Another thing I've noticed is that the authors show that DreamCoder + Stitch + MathDSL does better than Lemma and CanPoLe, and they additionally ablate DreamCoder + Stitch + the DSLs for Lemma and CanPoLe.  However, what about Lemma + MathDSL or CanPoLe + MathDSL?  I wonder if getting rid of DreamCoder here, but keeping the new MathDSL would do even better.  I can't tell if DreamCoder + Stitch is any benefit here, or if the only benefit is just the new MathDSL.

So in summary, this is a well-written paper that presents a good experiment.  Unfortunately, the results are mediocre and are unlikely to impact this field at all.
title: title: The authors introduce MathDSL, a novel domain-specific language for expressing solutions to linear equations, and demonstrates that program synthesis using MathDSL with the DreamCoder framework substantially outperforms reinforcement learning approaches in terms of accuracy, solution conciseness, and data efficiency. The paper also proposes a metric for quantifying solution conciseness.
main_review: main_review: This paper introduces MathDSL, a domain-specific language (DSL) designed to express linear equation solutions concisely. When used within the DreamCoder program synthesis framework, MathDSL generates more accurate and concise equation solutions than state-of-the-art reinforcement learning-based approaches like ConPoLe and Lemma. The paper also introduces a quantitative metric for measuring the conciseness of equation solutions. Experiments show that combining MathDSL with DreamCoder outperforms ConPoLe and Lemma in terms of solution accuracy and conciseness while requiring substantially less training data. The interpretable abstractions generated by DreamCoder using MathDSL could also have applications in mathematical education.

Pros
- MathDSL enables concise expression of equation solutions and strong empirical performance when used with DreamCoder.
DreamCoder + MathDSL substantially outperforms RL methods in accuracy, conciseness, and data efficiency ($\sim$200 templates vs $\sim 10^6$ equations).
- The conciseness metric enables quantitative comparisons of solution quality between methods.
- Interpretable abstractions are generated, which could be used to provide solution hints to students.

Cons
- Experiments are limited to linear equations; evaluating more complex domains would test generality.
- A user study with math students could help evaluate the interpretability and educational value of the learned abstractions.
- The conciseness metric has some limitations (e.g. favoring short solutions over more gradual ones); further refinements could be explored.
title: title: A novel DSL that makes math equation-solving more concise while using way fewer equation templates
main_review: main_review: **Summary:**

This paper presents a new domain-specific language, MathDSL, that when used with DreamCoder, results in highly-accurate and concise solutions to equations. The authors include an analysis of various set ups comparing the efficacy of DreamCoder with three different DSLs. The paper also presents a new AST-based metric measuring the conciseness of solutions, enabling us to measure the efficacy of DSLs beyond their plain accuracies.

**Strengths**
* The paper presents a new DSL that can be used with various systems to improve equation-solving accuracy, conciseness, and interpretability.
* The authors present a new AST-based metric that lets us measure the efficacy of an equation-solving system by measuring conciseness, i.e. how short a solution is with respect to the size of the equation trees.
* The Appendix presents an in-depth discussion of the weaknesses of the proposed evaluation metric, enabling future researchers to know of gaps they can focus on addressing.
* The Appendix includes a lot of detail about MathDSL, the program synthesis system, their experiments, and their conciseness metric. This makes the results from the paper reproducible, and makes it easier for other researchers to build upon the work of MathDSL.

**Weaknesses**
* While the authors discussing the weaknesses of the conciseness metric is notable, the issues they highlight are important, and possibly affect the scores that the different systems they compare receive.
* Linear equation-solving is a relatively narrow area, and while MathDSL presents an interesting new language for its purpose, the system would have to be generalized a lot before being broadly impactful.
title: title: A good research idea but need more information to prove the novelty
main_review: main_review: Pro:

1. The paper presents an innovative and practical methodology for solving mathematical equations using a domain-specific language. The use of program synthesis and abstractions allows for the generation of concise and human-interpretable solutions.
2. The paper provides insightful empirical findings, demonstrating the superiority of MathDSL over other methods in terms of accuracy and conciseness of generated solutions. The comparison with ConPoLe and Lemma provides a strong basis for the claims made by the authors.
3. The paper is well-structured and provides a clear review of relevant literature. The introduction and background sections provide sufficient context for understanding the motivation and significance of the research.

Cons:

1. Can you provide more details on the training process of the models? How were ConPoLe and Lemma trained on the equation templates? How were the models evaluated on the test dataset?
2. Could you provide more information on the dataset used in the experiments? How were the equation templates selected? What were the characteristics of the equations in the dataset?
3. Can you discuss the potential solutions to address the limitations of the conciseness metric? How could the metric be refined to better account for pedagogical clarity and solution complexity?
4. Lack of novelty: While MathDSL is a novel approach, the paper does not clearly highlight its novelty compared to existing DSLs and program synthesis systems
5. The evaluation of MathDSL is limited to linear equations, and it would be valuable to see its performance in more complex mathematical domains.
6. The paper only compares MathDSL with ConPoLeDSL and LemmaDSL, and it would be beneficial to compare its performance with other existing DSLs as well.