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，一种用于数学方程求解的领域特定语言（DSL）。该语言在程序合成模型中的部署效果优于当前最先进的基于强化学习的方法。我们同时提出了一种用于量化评估数学解简洁性的度量指标，并证明了相比其他方法，所生成解的质量得到了提升。我们的系统表明，使用MathDSL的程序合成系统（DreamCoder）能够生成比强化学习系统更精确、更简洁的线性方程求解程序。此外，我们证明若将先前强化学习系统的动作空间作为DSL使用，MathDSL的性能优于这些动作空间DSL。我们利用DreamCoder将方程求解策略作为习得的抽象概念存储于其程序库中，并证明通过MathDSL可将这些策略转化为人类可理解的求解方案，该成果在数学教育领域具有潜在应用价值。