Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Sagnik Anupam, Maddy Bowers, Omar Costilla-Reyes, Armando Solar-Lezama

TL;DR

The work addresses the challenge of symbolic mathematical reasoning by neural models, proposing a domain-specific language (MathDSL) integrated with the DreamCoder program-synthesis framework to synthesize complete linear-equation solutions and learn reusable abstractions. It introduces an AST-based conciseness metric and uses C-scores to demonstrate that MathDSL yields more concise, accurate solutions with far fewer training examples than reinforcement-learning baselines. Experiments on a Cognitive Tutor–derived dataset show significant gains in both accuracy and solution simplicity, with learned abstractions offering human-interpretable strategies for education. The approach suggests practical benefits for educational tools and automated reasoning, and it opens avenues to extend to more complex mathematical domains such as calculus or discrete mathematics.

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.

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

TL;DR

The work addresses the challenge of symbolic mathematical reasoning by neural models, proposing a domain-specific language (MathDSL) integrated with the DreamCoder program-synthesis framework to synthesize complete linear-equation solutions and learn reusable abstractions. It introduces an AST-based conciseness metric and uses C-scores to demonstrate that MathDSL yields more concise, accurate solutions with far fewer training examples than reinforcement-learning baselines. Experiments on a Cognitive Tutor–derived dataset show significant gains in both accuracy and solution simplicity, with learned abstractions offering human-interpretable strategies for education. The approach suggests practical benefits for educational tools and automated reasoning, and it opens avenues to extend to more complex mathematical domains such as calculus or discrete mathematics.

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.
Paper Structure (10 sections, 5 equations, 3 figures, 7 tables)

This paper contains 10 sections, 5 equations, 3 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Methods
  3. Conciseness Metric
  4. Experiments and Results
  5. Conclusions
  6. Program Synthesis System Description
  7. Description of MathDSL
  8. Limitations of Conciseness Metric
  9. Experiments
  10. DreamCoder Abstractions for Equation Solving

Figures (3)

  • Figure 1: Comparison of ConPoLe solutions with more concise DreamCoder+Stitch+MathDSL and Lemma solutions. The ConPoLe solution contains unnatural subroutines, while DreamCoder+MathDSL and Lemma offer more human-like strategies. The italicized step in the ConPoLe solution is a step storing the final answer as a fraction and not a division operation poesia_contrastive_2021.
  • Figure 2: Example of an equation, its corresponding prefix form string, a solution program solving the equation written in MathDSL, and the solution string generated when the equation string is passed as input to the solution program. An example of a useful abstraction here would be simplify(rrotate()), which could then be composed with other abstractions to build more powerful abstractions in future training iterations.
  • Figure 3: Percentage of tasks solved across 25 iterations for DreamCoder experiments using different DSLs.