本研究使用神经序列模型探讨在自动定理证明的命题选择方面的有效性，提出了一个两级方法，能够在避免现有最先进模型的手工设计功能的同时在 Mizar 语料库上为 premise selection 任务提供良好结果。据我们所知，这是首次在大规模的定理证明中应用深度学习。

Jun, 2016

该研究使用基于深度学习的方法，提出了一个新的思路来选择与证明相应的数学陈述。应用了一种新的嵌入方法，将高阶逻辑公式表示为一个不变于变量重命名的图，并在保留语法和语义信息的同时，全面地将图形嵌入到一个向量中，从而在 HolStep 数据集上实现了优异的分类表现，将分类准确度从 83％ 提高到了 90.3％。

Sep, 2017

我们设计了一个基于机器学习的工具，用于 Lean 证明助手，可以为用户正在证明的定理提供建议，它是通过在线训练自定义版本的随机森林模型，并利用 Lean 4 的元编程特性直接实现，可以通过 suggest_premises 策略在编辑器中与用户进行交互式证明

Mar, 2023

通过使用一种被称为状态规范化的机制来处理以前递归神经网络（RNNs）的不足，从而提高 RNNs 的状态转移动态分析和解释性，并将其应用于自动机抽取，自然语言处理和计算机视觉中。

Jan, 2019

本论文提出了基于机器学习的前提选择方法，通过构建依赖关系知识库并提出核方法的前提选择算法，在大型数学理论证明中实现了 50％的性能提升。

Aug, 2011

本文提出了自然前提选择 (Natural Premise Selection) 这一新型自然语言处理 (NLP) 任务，以便找到能为生成某个语句非正式数学证明提供支持定义和支持命题的前提；此外，我们还提供了一个数据集 NL-PS，用于评估不同方法在此任务上的表现，并使用不同的基线模型来展示了该任务所涉及的基本解释挑战。

Apr, 2020

该研究介绍了一种新模型，经过研究表明这种模型可以解决语言理解任务和推理任务，能够保持和更新世界状态的表示，并且具备类似于神经图灵机或可微分神经计算机的能力，该模型称为 Recurrent Entity Network。

Dec, 2016

本研究介绍了神经状态机（NSM），旨在构建神经和符号人工智能之间的桥梁，并整合它们的互补优势以执行视觉推理任务。该模型通过将视觉和语言模态转换为基于语义概念的表示，实现了显著的透明度和模块化，我们在 VQA-CP 和 GQA 两个最新的 VQA 数据集上进行了评估，取得了最新的成果。 所有情况的最好结果。

Jul, 2019

本文介绍了一种名为 “状态再构建” 的方法，旨在解决有限标记数据下现有神经网络方法的脆弱性问题，通过建模隐藏状态的分布并投影测试期间观察到的隐藏状态，从而帮助神经网络更好地泛化，特别是在标记数据稀缺的情况下，并且有助于克服采用对抗训练实现稳健泛化的挑战。

May, 2019

本文介绍了一种新的神经网络模型 —— 随机循环神经网络，该模型能高效地传播潜在状态的不确定性来构建序列神经生成模型，并在语音和音乐建模方面取得了比同类方法更好的结果。

May, 2016