一般来说，您的想法可能是可行的，但神经网络可能是用于探索此问题的错误高级工具。

神经网络的优势在于在将输入映射到输出时找到允许高度非线性解决方案的内部表示。当我们训练一个神经网络时，这些映射是通过重复示例以统计方式学习的。当给定与训练集相似的数据时，这往往会产生可以很好地插值的模型，但推断很糟糕。

神经网络模型也缺乏上下文，因此如果您使用生成模型（例如，在创建有效或有趣证明的序列上训练的 RNN），那么它很容易产生统计上令人愉悦但毫无意义的垃圾。

您将需要一些组织原则，允许您以组合方式探索和确认证明。事实上，像你的想法这样的事情已经做过不止一次了，但我目前无法找到参考。

这一切都不会阻止你在人工智能中使用神经网络来搜索证据。例如，在数学 AI 中，您可能需要一个很好的启发式方法来指导搜索——例如，在上下文中 X 是子证明 Y 可能是有趣或相关的。评估可能性分数是神经网络可以作为更广泛的 AI 方案的一部分来做的事情。这类似于神经网络如何与强化学习相结合。

原则上，有可能完全用神经网络构建你的想法。毕竟，有充分的理由怀疑人类推理使用生物神经元的工作方式类似（尚未证明人工推理可以以任何方式匹配）。然而，这种系统的架构超出了任何现代 NN 设计或训练设置。这绝对不是仅仅添加足够的层然后输入数据的问题。

不像描述的那样直截了当，但神经网络成功地应用于指导证据的搜索。有自动定理证明器。他们所做的大致是这样的：

1. 获取数学语句

2. 应用一种已知的数学等价变换（定理、公理等）

3. 检查结果语句是否为真。然后我们的转换序列就是证明（因为它们都是等价转换）。否则，转到 2。

这里棘手的部分是选择在第 2 步应用哪种变换。可以训练神经网络来预测函数，例如

语句，转换->该转换对该语句的有用性

然后，在搜索过程中，我们可以应用这种神经网络认为最有用的变换。此外，证明一个定理可以被视为游戏，其中公理是规则，当你达到证明时你就赢了。在这种形式下，可以应用强化学习代理来证明定理（这也是成功完成的）。

以下是做类似事情的论文：

• 使用神经网络生成正确性证明( Proverbot9001 )

• 定理证明的学习环境（游戏手柄）

• 学习用战术证明(TacticToe)

• 通过与证明助手（CoqGym）互动学习证明定理

• HOList：高阶定理证明的机器学习环境

• 定理证明的强化学习(rlCoP)

这是可能的，但可能不是一个好主意。

逻辑证明是人工智能最古老的领域之一，有一些不需要训练的专用技术，而且比神经网络方法更可靠，因为它们不依赖于统计推理，而是使用数学家的朋友：演绎推理。

主要领域被称为“自动定理证明”，它已经足够老了，以至于它作为一个研究领域被钙化了一点。创新不多，但还是有人在努力。

基本思想是定理证明只是经典或启发式引导搜索：您从由一组公认前提组成的状态开始。然后，您应用任何有效的推理逻辑规则来生成也必须为真的新前提，从而扩展您拥有的知识集。最终，您可以通过诸如广度优先搜索或迭代深化之类的枚举搜索，或通过具有特定领域启发式的A*之类的方法来证明所需的前提。许多求解器也只使用一个逻辑规则（统一），因为它是完整的，并且减少了搜索的分支因子。

我已经发表了一篇文章，使用了相应的基于一阶理论的生成语法的新方法：

关于生成语法的思考及其在基于神经网络的自动定理证明中的应用

这种方法允许不使用以前的数据，而是根据机器学习的需要生成它。在这篇文章中，您可能会找到有关逻辑、语法和神经网络的必要理论。您还可以从字面上找到生成证明的 python 函数的示例。我为命题逻辑添加了一个语法，它可以自然地扩展到一阶理论（例如群论或数论）的“真实”案例。