通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。
May, 2022
本研究使用由 10 million 問題 - 答案組成的大型多語言數據集，展示了對 Transformer 模型的微調可以應用於複雜數據集的自動評分，並討論了評分的信任和倫理問題。透過人工介入自動評分的過程，我們展示了如何提高自動化評分答案的準確性，並實現了相當於助教的準確性。同時，我們提出了一種有效的方法讓老師控制系統出現的錯誤類型，並且有效地驗證自動評分器在個別考試上的表現接近預期的表現。
Jan, 2022
本文提出了一种基于 “数理语言处理” 的数据驱动框架来自动评分开放性数学问题实现的方案，采用不同聚类方法组成的三层模型对多步解决方案进行追踪和错误定位，并在真实的慕课数据上进行了测试和验证，说明它可以极大地减少大规模教育平台上所需的人力投入。
Jan, 2015
NaturalProofs 是一个使用自然数学语言编写数学命题和证明的多域语料库，可用于评估系统在数学参考检索和生成任务中确定证明中出现的关键结果的能力，并提供了许多研究理解和创建自然数学语言的挑战性数学任务的新途径。
Mar, 2021
基于大语言模型的自动生成反馈在智能辅导系统和在线学习平台中具有潜力来提高许多学生的学习效果，本文针对自动生成和评估反馈的问题，提出了数学反馈评估标准和反馈生成框架，通过强化学习优化反馈的正确性和一致性，并通过案例研究定性分析了生成和评估系统。
Mar, 2024
本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。
Jan, 2023
通过评估大型语言模型在自动评分方面的可行性，并强调大型语言模型如何支持教育工作者验证评分程序，研究表明，虽然 “开箱即用” 的大型语言模型提供了宝贵的工具来提供补充视角，但它们对于独立自动评分的准备工作仍然是一个尚未完成的工作，需要人工监督。
Sep, 2023
本文研究了自动短答案评分问题，提出了一种新的基于 MathBERT 及上下文学习方法的框架，并在真实数据集上进行了评估，证明该框架对于之前未见过的数学问题的表现优于现有方法。
通过在交互证明助理中引入自然语言规范支持，可以在验证软件正确性的同时保证规范翻译的正确性和可审计性。
本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。
Sep, 2020