该研究论文介绍了一种从自然语言生成数学方程的方法，通过整合树结构和采用逐层并行解码策略，以及应用二分匹配算法来对齐预测结果与注释，以提高解方程的准确性和性能。

Oct, 2023

本文介绍了一种在连续向量空间中表示数学表达式的方法，使用序列到序列架构的编码器生成向量表示，并比较了这种方法与自编码器的差异。最后，为了加快未来的项目，我们发布了一组等价的超越和代数表达式对的语料库。

Oct, 2022

通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。

May, 2022

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

Mar, 2021

本论文的主要研究方向是解决神经机器翻译数学公式的问题，特别是涉及到模糊表示语言和明确内容语言之间的翻译，论文采用卷积序列到序列网络来翻译 LaTeX 和 Mathematica，达到了 95.1% 和 90.7% 的准确匹配。

May, 2023

使用变压器架构生成、评估和训练数学表达式，将其作为字符级序列转换任务进行分析，建立在关注机制上的编码器和解码器上。三个模型分别被训练在数学符号变量和表达式的理解和评估上，最终达到了测试准确率高达 76.1%、78.8% 和 84.9%。

Dec, 2018

本文介绍了潜在树语言模型（LTLM），该模型将给定句子的语法和语义编码为单词角色树。将 LTLM 与 4 元修改 Kneser-Ney 语言模型相结合，通过线性插值，在英语和捷克语语料库中的实验表明，与独立的 4 元修改 Kneser-Ney 语言模型相比，明显降低了困惑度（英语最高降低 46％，捷克语最高降低 49％）

Jul, 2016

利用大型语言模型 (LLMs) 进行特定领域的数学推导是一项新兴的研究方向，可以帮助发现模型的局限性，潜在地支持数学发现。本文利用符号引擎在大规模上生成方程的推导，并研究 LLMs 在从前提中推导目标方程时的能力。实证结果表明，fine-tuned FLAN-T5-large (MathT5) 在绝对性能方面超过了 GPT 模型在所有静态和分布外的测试集上。然而，深入分析发现，fine-tuned 模型对于涉及未知符号的扰动 (以及较小程度的方程结构更改) 更为敏感。此外，我们分析了 1.7K 个方程和 200 多个推导，突出了常见的推理错误，如包含不正确、无关或多余的方程，以及跳过推导步骤的倾向。最后，我们探讨了评估数学推导的现有指标的适用性，发现尽管它们能捕捉到对扰动的敏感性等一般属性，但无法凸显细粒度的推理错误和模型之间的重要差异。总体来说，本研究表明在合成数据上训练模型可以提高其数学能力，超越更大的架构。

Jul, 2023

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

Jul, 2017

本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。

Sep, 2020