基于多项式指纹的证明验证

《Journal of Logical and Algebraic Methods in Programming》：Proof verification by polynomial fingerprinting

　　

摘要
为了满足数学证明快速验证的需求，我们描述了一种将形式句编码为整数系数的多元多项式上的 2 × 2 矩阵的方法。这种对应是同态的：通常的证明步骤，如肯定前件式（modus ponens）或项和公式中的变量替换，变成了矩阵运算。通过在适当选择的有限域的随机元素中评估多项式变量，证明被替换为一个数值序列。只有对应于公理和重言式的值需要从 scratch（从头）计算。对应于派生公式的值是通过应用同态性质从对应于其祖先的值计算得出的。对应于证明结论的多项式矩阵也在所选的随机值上进行评估。如果数值序列的最后一项等于结论的评估值，根据施瓦茨 - 齐珀引理（Schwartz-Zippel Lemma），该证明以高概率是正确的。

章节片段
动机
人们对自动证明检查器（如 Methamath, Hol Light Coq, Isabelle 等）的兴趣日益增加。此外，还有整个研究计划旨在基于自动可验证的基础重写数学。另一方面，人们对程序或程序运行（如在线银行或加密货币交易）的正确性证书的经济和社会兴趣日益增加。计算速度是两个发展方向的重要因素，但更为敏感

问题
已经有一些指纹识别方法，旨在用于证明验证，并最终通过 CIRCOM 生成简洁证书，正如 Brandon Moore 向作者传达的那样，[12]。在所有这些方法中，证明行被视为字符串。对于字符串，很容易关联数字，或者大有限域的元素，使得肯定前件式步骤同态地工作。但在字符串之间找到同态对应更为困难

原理
假设固定了一种数学证明的形式体系，它包括命题逻辑和一阶逻辑，但也可以包括其他特定的证明系统，如匹配逻辑 [2], [3]。考虑一个由有限签名和有限数量的公理及公理模式组成的子系统。对于每个良构表达式 E（可以是项或公式），关联一个矩阵 [E]∈M2×2(Z[x1,x2,?,xn,?])，使得一个矩阵最多对应一个公式。

我们系统中的证明
多元多项式矩阵
导致本节小节的最初观察是，由不同变量组成的矩阵：
M(k)=(x4k+1x4k+2x4k+3x4k+4)
是非交换的，以至于如果两个乘积相等：
M(i1)?M(in)=M(j1)?M(jm)
那么 n=m 且 i1=j1, ?, in=jn。这意味着这样的单项式（初等矩阵的乘积）包含了关于因子数量、顺序和身份的信息。这三个信息要素对于编码树内部的路径至关重要。
然而，

边和节点的非交换表示
本节的目的是展示如何使用前面的构造进一步将矩阵与由树表示的项或公式关联起来。
下文，由边变量我们理解为一个多项式变量 xi。对于树的每一条边和每一个顶点，我们将关联一个形状如下的矩阵：
A(xi)=(xi101)。
为了通过树表示公式，逻辑操作和项构建操作都表示为树的顶点。对于每个元数为 d=d(c) 的特定符号 c，数量为 d+1

同态性质
在本小节中，我们定义了公式指纹的概念，并表明该概念具有证明中使用的公式操作的同态性质：肯定前件式和替换。我们展示了如何从肯定前件式操作的参数的指纹计算由肯定前件式产生的公式的指纹。我们还展示了如何从公式的指纹计算通过替换获得的公式的指纹，该公式是其中的

形式化证明示例
在本节中，我们将指纹技术应用于一个形式数学证明。我们考虑以下命题逻辑框架。有三个公理模式如下：
K(α,β):α→(β→α),
S(α,β,γ):(α→(β→γ))→((α→β)→(α→γ)),
N(α,β):(?α→?β)→(β→α)。
我们考虑以下定理：
定理 7.1 A→A。
正如我们将看到的，这个特定的命题逻辑定理甚至不需要公理 N(α, β) 来进行证明。然而，为了完整性，提到了这个公理。
经典证明：考虑公式 B ? A → A。

一阶逻辑和其他逻辑系统
本节介绍了一些进一步的构造。其目标是表明迄今为止提出的想法——主要集中在肯定前件式和替换上——对于一大类逻辑和证明系统来说是足够的。
我们从一阶逻辑开始。这里我们列出了一些一般性考虑，用于将每个一阶公式翻译为整数系数 Z 的多元多项式矩阵，分别通过多项式评估来执行快速证明验证。一个证明系统的示例，用于

CRediT 作者贡献声明
Mihai Prunescu：写作 – 回顾与编辑，写作 – 初稿，可视化，验证，监督，资源，项目管理，方法论，调查，资金获取，形式分析，概念化。

竞争性利益声明
作者声明，他们没有已知的竞争性经济利益或个人关系，这些可能影响本文中报告的工作。

Mihai Prunescu
逻辑、优化和安全研究中心 (LOS)，布加勒斯特大学数学与计算机科学学院，Academiei 14 街，布加勒斯特，010014，罗马尼亚