Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

该论文提出了一种基于多项式推理的混合代数验证技术，通过并行多模运算避免大整数计算，显著提升了算术电路字级验证的效率。

要点

这篇论文介绍了一种验证数字电路（特别是乘法器）是否“诚实”的新方法。

想象一下，你是一位超级审计师，你的任务是检查一个巨大的、复杂的自动售货机（这就是算术电路）是否真的按照说明书工作。说明书说：“如果你投进 5 块钱，应该吐出价值 5 块钱的饮料。”

1. 以前的难题：算数太慢，数字太大

在以前，审计师们（验证工具）在检查时，喜欢用**“大数算术”**。

• 比喻：就像你要计算 $64 \times 64$，结果是一个巨大的数字。以前的工具在处理这些数字时，就像是用算盘去算天文数字。数字越来越大，算盘珠子都不够用了，必须请专门的“大数计算器”（任意精度算术库）来帮忙。
• 后果：这非常慢，而且容易卡死。当电路变得很复杂（比如 64 位或 128 位）时，数字大到连超级计算机都算不过来，验证过程就崩溃了。

2. 新方法的核心理念：化整为零，并行作战

这篇论文提出的新方法叫**“并行多模算术验证”。它的核心思想是：“别算大数，我们把它拆成很多个小问题，大家一起算！”**

比喻：分头检查的审计团队

想象你不再派一个审计师去算那个巨大的天文数字，而是派了5 个审计师（对应 5 个不同的质数模数）。

• 审计师 A 负责算“除以 7 余几”。
• 审计师 B 负责算“除以 11 余几”。
• 审计师 C 负责算“除以 13 余几”。
• ...以此类推。

为什么这样好？

1. 数字变小了：每个审计师只需要处理很小的数字（比如 0 到 12），就像用手指算数一样快，完全不需要那个笨重的“大数计算器”。
2. 并行加速：这 5 个审计师可以同时工作（并行计算）。在现代多核电脑上，这就像 5 个人一起干活，速度直接翻了 5 倍。
3. 结果可靠：根据数学上的**“中国剩余定理”**（就像拼图），只要这 5 个审计师算出来的“余数”拼起来是对的，那么那个巨大的原始数字肯定也是对的。

3. 混合策略：既用“直线思维”，也用“曲线救国”

光把数字变小还不够，验证电路还需要一种聪明的策略。作者把两种策略结合在了一起，就像**“先走直线，走不通再绕路”**。

策略 A：线性重写（走直线）

• 比喻：审计师先尝试找简单的规律。比如，他们发现“只要输入是 1，输出就是 2"。这种简单的线性关系很容易验证。
• 技巧：他们使用一种叫“猜与证”（Guess and Prove）的方法。先猜一个规律，然后用逻辑推理去证明它是对的。如果猜对了，就快速通过。
• 创新：以前的方法在猜的时候，容易漏掉一些罕见的情况（就像只检查了白天，没检查晚上）。这篇论文改进了采样方法，确保能抓到所有“鬼鬼祟祟”的异常情况。

策略 B：非线性重写（绕路）

• 比喻：如果电路太复杂，简单的直线规律行不通（比如输入和输出之间是弯曲的、纠缠的关系），审计师就切换到**“非线性模式”**。
• 作用：这时候他们不再找简单的规律，而是直接一步步地拆解电路，像剥洋葱一样，直到把问题彻底解决。虽然这步比较慢，但非常** robust（稳健）**，能保证在复杂情况下也能算出结果。

混合的威力：
新工具（TalisMan2.0）会先尝试快速的“直线模式”。如果卡住了，就自动切换到稳健的“绕路模式”。这种**“双保险”**策略，既保证了速度，又保证了能解决难题。

4. 实验结果：快且稳

作者把这个新工具（TalisMan2.0）拿去测试了 200 多个复杂的乘法器电路。

• 结果：它是唯一一个全部通过所有测试的工具。
• 对比：以前的工具要么算得太慢超时，要么在复杂的电路面前直接放弃。而这个新工具，因为用了“分头算小数字” + “混合策略”，不仅速度快，而且非常可靠。

总结

这篇论文就像发明了一种**“分而治之”的超级审计法**：

1. 拒绝大数：把巨大的计算任务拆成很多小任务，避免使用慢吞吞的大数计算。
2. 团队作战：利用多核电脑并行处理这些小任务。
3. 灵活应变：先用简单的方法快速解决，搞不定再上复杂的方法，确保万无一失。

这种方法让计算机在验证复杂的硬件电路时，变得更快、更聪明、更可靠。

技术摘要

这是一份关于论文《Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits》（避免大整数：算术电路的并行多模代数验证）的详细技术总结。

1. 研究背景与问题 (Problem)

核心痛点：大整数算术带来的计算开销
在算术电路（如乘法器、除法器）的单词级（Word-level）形式化验证中，基于计算机代数的方法已被证明非常有效，因为它避免了位级（Bit-level）验证带来的组合爆炸问题。然而，现有的代数推理方法面临一个严重的可扩展性瓶颈：

• 系数膨胀：对于 64 位或更大位宽的算术电路，生成的多项式系统中的系数极其巨大（例如，64 位乘法器的规范系数可达 $2^{127}$）。
• 依赖任意精度算术：为了处理这些大系数，现有工具（如 AMulet, TeluMA 等）必须依赖任意精度算术库（如 GMP）。这导致了巨大的计算开销，严重限制了验证工具在处理大规模电路时的可扩展性。
• 线性推理的局限性：现有的“猜测与证明”（Guess-and-Prove）线性重写策略在处理大型子电路时性能下降，且由于系数过大，基于 SAT 的证明步骤往往变得不可行。

2. 方法论 (Methodology)

本文提出了一种混合多模代数验证框架，核心思想是利用同态图像（Homomorphic Images）和并行计算来完全避免大整数运算。

2.1 并行多模推理 (Parallel Multimodular Reasoning)

• 基本原理：不再在整数环 $\mathbb{Z}$ 或有理数域 $\mathbb{Q}$ 上进行计算，而是将多项式系统映射到多个机器字长大小的素数域 $\mathbb{Z}_{p_i}$ 上进行计算。
• 中国剩余定理 (CRT)：通过在多个互素的模数 $m_1, \dots, m_k$ 下并行验证，利用中国剩余定理保证在整数域上的正确性。只要模数乘积大于规范多项式在所有布尔赋值下的最大绝对值，验证结果就是正确的。
• 优势：所有系数都被限制在机器字长内（如 32 位或 64 位），从而可以使用原生硬件算术，彻底消除了任意精度算术的开销。
• 并行化：不同模数下的验证任务是相互独立的，因此可以在多核 CPU 上并行执行，获得近线性的加速比。

2.2 混合重写策略 (Hybrid Rewriting Framework)

该框架结合了线性重写和非线性重写的优势，并在多模环境下执行：

1. 线性重写 (Linear Rewriting)：

   • 预处理：语义识别电路中的半加器 (HA) 和全加器 (FA) 结构，提取线性约束。
   • 子电路提取与采样：针对当前规范多项式的最高项，提取子电路。
   • 改进的采样策略：摒弃了传统的均匀输入采样，采用 CMSGen 加权采样器。该采样器能生成覆盖罕见行为（如长 AND 链输出为 1 的情况）的赋值，提高了猜测线性关系的成功率。
   • 猜测与证明 (Guess-and-Prove)：
     • 猜测：利用线性代数在有限域 $\mathbb{Z}_p$ 上求解线性方程组 $Ax=0$ 来猜测线性关系。
     • 加速技巧：利用矩阵结构（0/1 元素，行数远大于列数），通过随机矩阵 $B$ 将系统转化为 $(BA)x=0$，利用位运算加速求解。
     • 证明：使用 SAT 求解器（CaDiCaL）验证猜测的线性关系。在多模设置下，SAT 证明仅需处理小系数，效率极高。
     • 修复：如果证明失败（找到反例），将反例加入样本集重新猜测。

2. 非线性重写 (Nonlinear Rewriting)：

   • 当线性提取因子电路过大而变得不可行时，框架自动切换到非线性重写。
   • 采用字典序（Lexicographic order），利用电路的拓扑逆序，确保门电路多项式构成 Gröbner 基。
   • 通过多项式除法计算规范形式（Normal Form）。如果结果为 0，则电路正确；否则提取反例。
   • 同样在多模域上并行执行系数运算。

2.3 工具实现：TalisMan2.0

作者将上述方法实现于新工具 TalisMan2.0 中。该工具支持：

• 多模并行计算（不同素数由不同线程处理）。
• 细粒度并行化（预处理和子电路提取串行共享，猜测、证明、修复并行）。
• 向量化的系数运算（使用 SIMD 指令处理多模系数向量）。

3. 主要贡献 (Key Contributions)

1. 完全避免大整数算术：首次将同态图像技术应用于单词级电路验证，通过多模并行计算彻底消除了对任意精度算术库的依赖，显著降低了计算开销。
2. 混合验证框架：提出了一种结合线性重写（高效）和非线性重写（鲁棒）的混合策略。线性部分处理大部分简化工作，非线性部分作为兜底机制，确保了对复杂电路（如包含长进位链的乘法器）的验证能力。
3. 算法优化：
   • 改进了“猜测与证明”策略，引入 CMSGen 加权采样，解决了长逻辑链采样覆盖率低的问题。
   • 优化了线性代数求解过程，利用矩阵稀疏性和位运算加速。
   • 设计了细粒度的并行执行策略，最大化多核 CPU 的利用率。
4. 反例生成：即使在纯线性方法无法完成验证的情况下，混合框架也能通过非线性重写生成具体的反例（Counterexamples），这是纯线性方法难以做到的。

4. 实验结果 (Results)

作者在 TalisMan2.0 上对 207 个整数乘法器基准（包括结构化的 Aoki 乘法器和经过综合优化的 ABC 乘法器）进行了评估，并与现有工具（TalisMan1, MultiLinG, AMulet2, TeluMA, DynPhaseOrderOpt）进行了对比：

• 求解能力：TalisMan2.0 是唯一成功解决所有 207 个基准测试的工具。其他工具在合成电路或特定结构（如前向进位加法器）上均存在失败案例。
• 性能提升：
  • 相比 TalisMan1（旧版），新工具在求解数量和速度上均有显著提升。
  • 消融实验表明：
    • 使用 CMSGen 采样 比均匀采样多解决了 24 个基准，且运行时间更短。
    • 仅使用线性重写仅能解决 98 个基准，仅使用非线性重写仅能解决 79 个基准，证明了混合策略的必要性。
• 资源效率：验证 64 位乘法器仅需 8 个 16 位素数，128 位仅需 16 个。内存占用极低（最大仅需 5GB），而限制设为 32GB。
• 并行加速：在多核机器上，多模并行计算带来了显著的速度提升。

5. 意义与影响 (Significance)

• 可扩展性突破：该方法解决了算术电路验证中因系数过大导致的“表达式膨胀”问题，使得验证 64 位甚至更大位宽的复杂算术电路变得可行且高效。
• 工业应用潜力：通过避免昂贵的任意精度运算，该方法更适合集成到工业级的硬件验证流程中，能够处理经过逻辑综合优化后的复杂电路（这些电路通常破坏了原有的结构特征，使得基于启发式的方法失效）。
• 理论贡献：证明了在有限域上并行验证并组合结果的正确性，为计算机代数在硬件验证领域的应用开辟了新路径。
• 未来方向：论文指出未来将集成证明日志（Proof Logging）技术，以生成可验证的简短证明，并计划将该方法扩展至等价性检查等其他问题。

总结：这篇论文通过引入并行多模代数推理和混合重写策略，成功克服了传统代数验证方法在处理大位宽算术电路时的性能瓶颈，提供了一种既高效又鲁棒的验证方案，显著提升了硬件形式化验证的边界。