Mathematical language in scientific communications and educational scenarios
is important yet relatively understudied compared to natural languages. Recent
works on mathematical language focus either on representing stand-alone
mathematical expressions, especially in their natural tree format, or
mathematical reasoning in pre-trained natural language models. Existing works
on jointly modeling and generating natural and mathematical languages simply
treat mathematical expressions as text, without accounting for the rigid
structural properties of mathematical expressions. In this paper, we propose a
series of modifications to existing language models to jointly represent and
generate text and math: representing mathematical expressions as sequences of
node tokens in their operator tree format, using math symbol and tree position
embeddings to preserve the semantic and structural properties of mathematical
expressions, and using a constrained decoding method to generate mathematically
valid expressions. We ground our modifications in GPT-2, resulting in a model
MathGPT, and demonstrate that it outperforms baselines on mathematical
expression generation tasks.

本文提出一种将数学语言与自然语言一起表示和生成的语言模型，MathGPT，在数学表达式生成任务上表现出超越基准模型的性能。

基于树形表示与生成的自然语言与数学语言

Tree-Based Representation and Generation of Natural and Mathematical Language

Understanding and creating mathematics using natural mathematical language -
the mixture of symbolic and natural language used by humans - is a challenging
and important problem for driving progress in machine learning. As a step in
this direction, we develop NaturalProofs, a multi-domain corpus of mathematical
statements and their proofs, written in natural mathematical language.
NaturalProofs unifies broad coverage, deep coverage, and low-resource
mathematical sources, allowing for evaluating both in-distribution and
zero-shot generalization. Using NaturalProofs, we benchmark strong neural
methods on mathematical reference retrieval and generation tasks which test a
system's ability to determine key results that appear in a proof. Large-scale
sequence models show promise compared to classical information retrieval
methods, yet their performance and out-of-domain generalization leave
substantial room for improvement. NaturalProofs opens many avenues for research
on challenging mathematical tasks.

NaturalProofs 是一个使用自然数学语言编写数学命题和证明的多域语料库，可用于评估系统在数学参考检索和生成任务中确定证明中出现的关键结果的能力，并提供了许多研究理解和创建自然数学语言的挑战性数学任务的新途径。

自然证明：自然语言数学定理证明

NaturalProofs: Mathematical Theorem Proving in Natural Language

While neural network approaches are achieving breakthrough performance in the
natural language related fields, there have been few similar attempts at
mathematical language related tasks. In this study, we explore the potential of
applying neural representation techniques to Mathematical Information Retrieval
(MIR) tasks. In more detail, we first briefly analyze the characteristic
differences between natural language and mathematical language. Then we design
a "symbol2vec" method to learn the vector representations of formula symbols
(numbers, variables, operators, functions, etc.) Finally, we propose a
"formula2vec" based MIR approach and evaluate its performance. Preliminary
experiment results show that there is a promising potential for applying
formula embedding models to mathematical language representation and MIR tasks.

该研究探索了将神经网络应用于数学信息检索任务的潜力，并设计了两种学习向量表示公式符号的方法，最终提出了一个基于公式嵌入模型的信息检索方法，初步实验结果表明在数学语言表达和信息检索任务中应用公式嵌入模型具有很好的潜力。