首个神经推测数据集和实验
该研究采用深度神经网络进行数学形式化的自动化,使用机器翻译模型将非正式的 LaTeX 写的 Mizar 文本转化成正式的 Mizar 语言,并进行了多次实验以测试其可行性。结果表明,通过人工神经网络进行数学形式化是一种有前途的方法。
May, 2018
本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用,提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f,使用 Metamath 形式语言,并分析了其性能。 GPT-f 发现了新的简短证明,并被采纳为正式数学社区所接受,这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。
Sep, 2020
本文旨在通过实验探讨利用神经网络自动将 LaTeX 格式的非正式数学语句翻译成 Mizar 语言中的正式数学陈述。研究通过监督和非监督方法训练了三个基于神经网络的机器翻译模型,并开发了自定义的类型详细说明机制来优化结果。
Dec, 2019
本文提出了一种利用机器智能在数学数据中找到抽象模式生成数学不等式的猜想的系统方法,以 < f<g 类型的严格不等式为重点研究对象,并将它们与一个向量空间相关联,并在这个称为猜想空间的空间中执行几何渐进式下降算法,生成了有关素数计数函数和非阿贝尔简单群的 Cayley 图直径的新猜想,并突显了该空间中数学发现的重要性和领域专业知识的必要性。
Jun, 2023
本文研究了基于 transformer 的神经网络在自然语言理解方面的多项选择问题,主要针对先验偏差和选择麻烦等问题做了四项混淆测试,并表明该模型在应对这些问题时表现出明显的偏差和选择麻烦,建议需要进一步增强测试协议和基准测试以确保语言模型在面向实际决策的系统中得到合理的应用。
Oct, 2022
本文提出了一种新的架构 —— 神经单元器,并提出了相应的训练过程,实现了最先进的推理结果,通过模拟一种众所周知的推理过程 —— 向后链接,即使模型只在浅层次的数据上进行训练,也能回答深度问题,并通过使用各种基准数据集进行实验。
Sep, 2021
本文研究了构建有效和高效神经序列标记系统的设计挑战,通过复现 12 个模型,在三个基准测试中进行系统模型比较,消除现有文献中的误解和不一致的结论,并得出了一些对从业者有用的实用结论。
Jun, 2018
本研究引入了三种不同类型的解释数据集,发现基于 BERT 分类器的方法能够显著提高解释质量,同时通过使用广义推理链,使得对某些扰动更具鲁棒性。
Oct, 2020
通过将机器翻译应用于英语数据集,本研究聚焦于生成波斯语命名实体数据集。通过实验评估,最高的 F1 分数是 CoNLL 2003 数据集的 85.11%。本研究的结果强调了机器翻译在为低资源语言(如波斯语)创建高质量的命名实体识别数据集方面的潜力,并提供了有关机器翻译在此任务中有效性的见解。此外,此方法可用于增强低资源语言中的数据或创建嘈杂数据以使命名实体系统更加稳健并改进它们。
Feb, 2023