Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models¶
会议: NeurIPS 2026
arXiv: 2605.15131
OpenReview: https://openreview.net/forum?id=V35878j7OK
领域: Reasoning
关键词: 反应式合成, 大推理模型, 神经符号系统, 模型检测, 反例引导修复
一句话总结¶
本文提出神经符号化反应式合成框架 Natural Synthesis，将大推理模型与符号模型检测器紧密耦合，利用反例反馈迭代修复高层 Verilog 硬件电路，在 SYNTCOMP 基准上实现 92% 的求解率并超越专用符号工具，同时将能力扩展至不可判定的参数化合成与自然语言端到端规范合成。
研究背景与动机¶
在硬件设计流程中，功能正确性验证占据了绝大部分开发成本，因为硬件电路一旦流片量产，逻辑缺陷便无法通过后期补丁修复。传统工业界主要依赖测试与形式化验证，然而这两种手段均需工程师手工编写 RTL 设计；当验证失败时，仍然必须耗费大量人力进行人工定位与漏洞修复。相比之下，反应式合成（Reactive Synthesis）致力于从时序逻辑规范（如 LTL / TLSF）直接自动生成由构造即正确的硬件电路实现，真正解放工程师由“实现怎么做”转向“规范做什么”。然而，经典反应式合成面临理论与实践的双重困境：一方面，线性时序逻辑（LTL）合成在算法复杂度上属于 2-EXPTIME 完全问题，传统基于自动机转换与奇偶博弈求解的专用符号工具在工业级复杂系统上面临严重的状态爆炸；另一方面，要求工程师直接使用精确严苛的时序逻辑编写形式化规范具有极高的专业壁垒，严重限制了合成技术的工业落地。
近期基于神经网络的神经符号反应式合成探索了“猜测-检验”（Guess-and-Check）范式，但早期方法多局限于门级网表生成、仅支持可实现规范，或受限于预训练模型的简单单轮生成能力，面对包含复杂时序关联与参数化约束的实际基准仍然力不从心。更为严峻的是，实际工程中广泛需要的“参数化合成”（即生成不依赖具体进程/客户端数量 \(n\) 的通用电路模板）在理论上已被证明是不可判定问题（Undecidable），传统符号求解器与博弈论算法在此类任务上几乎完全失效。
本文的切入视角是充分释放大推理模型（LRMs，如 Gemini 3.1 Pro、GPT-5.5）在高层语义理解与长程逻辑演绎上的涌现能力，并与严格可靠的形式化验证工具形成闭环。核心 idea：将大推理模型置于寄存器传输级（Verilog）的抽象层面，构建结合符号模型检测反例驱动修复的神经符号闭环，不仅在标准形式化合成中击败顶尖专用符号工具，更一举攻克不可判定的参数化系统合成与面向自然语言需求的自动形式化端到端合成。
方法详解¶
整体框架¶
Natural Synthesis 彻底摒弃了传统反应式合成将时序规范强行展开为底层自动机或展开至门级网表的做法，全程保持在高层语义与硬件描述语言的抽象层级。整体工作流包含三个递进阶段：首先，对于给定的系统需求（形式化 TLSF 规范或非形式化自然语言描述），系统提供自动形式化与直接生成两条路径；其次，大推理模型直接生成 RTL 级的 Verilog 模块（或在规范不可实现时生成环境反例博弈策略）；最后，利用基于工业级工具链 Yosys 与 nuXmv 的符号模型检测流水线进行形式化属性验证。一旦检测到时序违例，反例执行轨迹将被结构化回传给大推理模型，驱动其在上下文窗口中展开长思维链反思与局部逻辑修复，直至生成数学证明正确的硬件电路。
%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
A["系统需求输入<br/>自然语言描述 / TLSF 时序规范"] --> B["高层抽象建模与双极性生成<br/>生成系统解或环境反例策略"]
B --> C["符号模型检测与规约分解<br/>Yosys 综合 + nuXmv IC3 验证"]
C -->|发现反例违例反例轨迹| D["符号反例引导的闭环修复<br/>CEX-LRM 思维链诊断与代码重构"]
D --> C
C -->|形式化验证通过 Q.E.D.| E["参数化外推与自适应输出<br/>输出数学证明正确的 Verilog 硬件电路"]关键设计¶
1. 高层抽象建模与双极性生成：保持 RTL 表现力与可实现性对称判定
传统合成工具通常先将 TLSF 规范编译为纯 LTL 公式，再构造确定性奇偶自动机进入无限博弈求解，这一极低层的表示不仅摧毁了规范原始的代码结构与参数范围语义，更会导致状态空间指数级膨胀。Natural Synthesis 坚持在规范与实现两端均保持高抽象层级：输入端直接保留 TLSF 的结构化语法（包含输入输出声明、INITIALLY 初始化条件、ASSERT 系统不变量、REQUIRE/ASSUME 环境假设等分段）；输出端直接靶向寄存器传输级（RTL）的高级硬件描述语言 Verilog，使其能够直接映射至工业标准的电路综合流程。针对现实规范中普遍存在的不可实现（Unrealizable）问题，设计了优雅的双极性生成机制：若规范可实现，模型生成命名为 solution 的满足系统规范的 Verilog 模块；若规范不可实现，模型则颠倒输入输出角色，生成名为 environment 的环境对抗策略模块，向模型检测器证明在任何系统响应下均存在环境使其违例，从而对称地解决了不可实现性证明问题。
2. 符号反例引导的闭环修复：以严格形式化反馈强化非可靠推理 大推理模型虽然具备强大的代码与逻辑生成能力，但其固有生成过程并非“由构造即正确”（Sound-by-construction），单次生成的 Verilog 电路极易在边角时序（Corner Cases）或隐含状态转移上出现逻辑偏差。为此，系统接入了严格的符号验证工具链：利用开源硬件综合工具 Yosys 将生成的 Verilog 降阶转换为 AIGER 与非图格式并去除无关时钟端口，随后通过 aigtosmv 输入至符号模型检测器 nuXmv，调用基于布尔可满足性（SAT）的增量约束求解算法 IC3/IMC 进行全状态空间时序穷举验证。当电路无法满足规范时，模型检测器自动抽取出最小长度的反例执行序列 \(\sigma\)。反例轨迹精确记录了从初始周期到失效周期的输入赋值与内部状态变迁，系统将其连同当前错误代码重新注入模型的推理上下文中。大推理模型借助高预算思维链反思时序冲突诱因，对寄存器转移条件、赋值延迟及触发逻辑进行靶向修正，将非完备的神经直觉与完备的符号验证融为一体。
3. 规约目标时序分解：细粒度并发验证与精准故障定位 当系统面临大型复杂时序系统时，直接对整条巨型蕴含公式进行模型检测会导致 IC3 算法求解时间急剧上升甚至超时。基于反应式合成中多假设与多保证的经典结构，系统针对典型具有 \(n\) 个环境假设与 \(m\) 个系统保证的规范设计了时序分解算法。对于可实现情况，将原蕴含验证任务拆分为 \(m\) 个独立的子性质： $\(\bigwedge_{i=1}^n a_i \longrightarrow g_j \quad (j \in \{1, \ldots, m\})\)$ 对于不可实现情况，则拆分为 \(n\) 个独立的环境反例对抗子目标： $\(\neg \Big(a_k \longrightarrow \bigwedge_{j=1}^m g_j\Big) \quad (k \in \{1, \ldots, n\})\)$ 这种分解带来了双重收益：一方面将庞大的模型检测任务解耦为可并发执行的低维度验证；另一方面，当某条具体子性质被违背时，模型能够获知究竟是哪一条特定的业务保证（\(g_j\)）或环境假设（\(a_k\)）发生了破坏，为后续大推理模型的反例修复提供了高语义密度的精准故障定位。
4. 参数化外推与自适应输出：参数化模板归纳与自然语言双轨落地
面对参数化合成这一经典不可判定难题（要求生成的电路模板能够适用于任意客户端/总线规模 \(n\)），传统方法由于无法对无界状态空间构建穷举博弈而停滞不前。Natural Synthesis 利用 Verilog 原生支持的参数化模块接口（如 parameter n = 27），引导大推理模型归纳出结构不变的参数化逻辑模板，并通过多实例具象化检测（实例化至 SYNTCOMP 历史最大参数值进行 IC3 验证）获得伪反例反馈，实现了向任意规模泛化的强大归纳推理能力。在需求规范层面，针对手写 LTL 极难维护的痛点，提出了两条从自然语言需求到硬件的落地路线：第一条是“自动形式化路线”，利用包含完整 TLSF 语法规范的结构化 Prompt 将自然语言转化为形式化规范，并通过语法反馈循环修复格式；第二条是“端到端直接合成路线”，跳过中间形式化直接生成 Verilog，再分别利用标准形式化基准进行互校。两条路线在消除形式化使用门槛的同时，确保了最终硬件输出的严格可验证性。
损失函数 / 训练策略¶
本文基于冻结参数的前沿大推理模型（Gemini 3.1 Pro、GPT-5.5）以零样本/少样本上下文提示驱动，不涉及微调权重更新。核心推理能力完全依赖推理时算力扩展（Test-Time Compute Scaling）以及测试时反例引导的反馈循环。在模型检测后端，nuXmv 运行于 Intel Emerald Rapids 硬件架构，设置 32 GB 内存上限与 600 秒严格验证超时；Yosys 采用优化的 AIGER 转换流水线（经历 proc, flatten, opt, memory, techmap, dffunmap, abc -g AND），确保生成网表与模型检测器严格对齐。
实验关键数据¶
主实验¶
在涵盖 1586 个基准规范的年度国际反应式合成竞赛权威评测集 SYNTCOMP 2025 上的评测结果如下表所示。基线包括 2025 年竞赛冠军工具 ltlsynt、亚军工具 SemML，以及近期同类模型基线。
| 类型 | 方法 / 模型 | 反例迭代轮数 (CEX) | 求解数量 (Solved) | 求解率 (Gain / 占比) |
|---|---|---|---|---|
| 符号算法 | SemML (Kretínský et al., 2025) | - | 1295 / 1586 | 81.65% |
| 符号算法 | ltlsynt (Renkin et al., 2022) | - | 1297 / 1586 | 81.78% (前SOTA) |
| LRM 基准 | GPT-5 (Egolf et al., 2026) | 0 | 229 / 1586 | 14.44% |
| 本文方法 | Gemini 3.1 Pro (Reasoning HIGH) | 0 | 1193 / 1586 | 75.22% |
| 本文方法 | Gemini 3.1 Pro (Reasoning HIGH) | 1 | 1311 / 1586 | 82.66% (+118) |
| 本文方法 | Gemini 3.1 Pro (Reasoning HIGH) | 2 | 1355 / 1586 | 85.43% (+162) |
| 本文方法 | GPT-5.5 (Reasoning XHIGH) | 0 | 1392 / 1586 | 87.77% |
| 本文方法 | GPT-5.5 (Reasoning XHIGH) | 1 | 1449 / 1586 | 91.36% (+57) |
| 本文方法 | GPT-5.5 (Reasoning XHIGH) | 2 | 1467 / 1586 | 92.50% (+170 相对前SOTA) |
消融实验¶
消融实验分为两部分：其一为推理时计算量（思考 Token 预算）对求解成功率的影响；其二为不可判定参数化基准与自然语言数据集（NATURAL，57 个难度顶格的代表性规范）上的消融分析。
| 模型与配置 | 思考预算 / 验证模式 | 求解数量 (Solved) | 平均思考 Token 数 / 说明 |
|---|---|---|---|
| GPT-5.5 (SYNTCOMP) | NONE (无推理思考) | 123 / 1586 | 0 ± 0 (性能断崖下跌) |
| GPT-5.5 (SYNTCOMP) | LOW | 911 / 1586 | 1025 ± 534 |
| GPT-5.5 (SYNTCOMP) | MEDIUM | 1287 / 1586 | 3450 ± 2751 |
| GPT-5.5 (SYNTCOMP) | HIGH | 1378 / 1586 | 5343 ± 4088 |
| GPT-5.5 (SYNTCOMP) | XHIGH | 1392 / 1586 (0轮CEX) | 6892 ± 5342 |
| Gemini 3.1 Pro (参数化合成 57例) | 直接生成 (Zero-CEX) | 35.0 ± 1.0 / 57 | 不可判定参数化通用模板 |
| Gemini 3.1 Pro (参数化合成 57例) | + 反例引导修复 (CE-Guidance) | 38.3 ± 1.1 / 57 | 达到与固定大参数相同上限 |
| Gemini 3.1 Pro (NATURAL 自然语言) | 经由自动形式化 (验真值) | 30.0 ± 0.0 / 57 | 符号工具在此类仅解 19/57 |
| Gemini 3.1 Pro (NATURAL 自然语言) | 端到端直接生成 (验真值) | 31.7 ± 1.2 / 57 | 避开 TLSF 语法损耗，效果更佳 |
关键发现¶
- 符号反例反馈的杠杆效应：模型检测器给出的反例带来了巨大的性能跃升。在 Gemini 3.1 Pro 上，引入两轮反例反馈使得求解数量从 1193 飙升至 1355（净增 162 篇，增幅达 13.6%）；在 GPT-5.5 上，反例引导将求解率从 87.77% 进一步推高至创纪录的 92.50%，净超越传统国际竞赛冠军 170 个基准。
- 思考 Token 与求解率呈严格对数线性关系：当完全关闭推理思考预算（NONE）时，GPT-5.5 的求解数发生雪崩，从 1392 锐减至仅 123 篇；随着思考 Token 数量从 1k 扩展至近 7k，求解能力呈现典型的对数线性收益（Log-linear scaling），充分证实大推理模型的内部演绎是解决高难时序综合的本质引擎。
- 对称解决可实现与不可实现问题：与以往工作仅能处理可实现性规范不同，GPT-5.5 在 0 轮反例下解决的 1392 篇规范中，均衡地包含了 640 个可实现规范与 752 个不可实现规范，证明其完全具备合成环境博弈反例策略的能力。
- 跨越不可判定鸿沟：在 57 个参数化系统综合测试中，Gemini 3.1 Pro 在带反例指导下成功合成了 38.3 个通用参数化模板，与直接针对固定最大参数求解的 38.3/57 表现完全一致，展现出令人惊叹的符号归纳与模板抽象能力。
亮点与洞察¶
- 神经直觉与符号确定性的完美共生：将大推理模型作为高层语义与启发式搜索的“发电机”，将经过数十年形式化验证积淀的模型检测器作为“真理裁判所”。利用反例轨迹构建闭环，既发挥了神经网络绕开 2-EXPTIME 指数级状态枚举的直觉速度，又守住了硬件流片零缺陷的数学确定性底线。
- 寄存器传输级（Verilog）的抽象降维：跳出门级网表与自动机状态图的低层桎梏，直接生成高级硬件描述语言。Verilog 原生支持的数据流赋值与时序过程块使得推理模型能充分利用上下文窗口的语义承载力，避免无意义的门级网表符号堆砌。
- 自然语言直接合成硬件的端到端突破：传统形式化合成必须强依赖工程师书写高难度时序逻辑，而本文证实端到端自然语言合成不仅行之有效（求解率达 31.7/57，远超传统工具基于形式化规范的 19/57），且能反向促进自动形式化的检验与解释，为下一代无缝人机协同芯片设计铺平了道路。
局限与展望¶
- 作者承认的局限：在自然语言自动形式化阶段，现存的自动机时序等价性判定工具（如 Spot 的 ltlfilt）在面对大规模复杂规范时极易发生超时（57 例中有 26.3 例在 30 分钟内无法判定等价性），制约了中间形式化产物的自动化评测效率。
- 外部观察的局限：参数化合成的验证本质上仍退化为对有限离散参数实例的抽样检验（Testing-based Verification），在理论层面无法像经典模型检测一样对任意 \(n \in \mathbb{N}\) 给出完备的数学证明（尽管生成的 Verilog 结构上具备通用性）。
- 未来改进方向：可进一步将神经排序函数（Neural Ranking Functions）或归纳不变量生成器引入参数化验证流程，实现全自动的参数化归纳证明闭环；同时构建更大规模的面向工业总线协议（如 AXI、APB、PCIe）的自然语言硬件需求基准库。
相关工作与启发¶
- vs ltlsynt (Renkin et al., 2022) / Strix (Meyer et al., 2018)：传统符号合成工具依赖极其昂贵的全称自动机确定化（Safra 构建）与奇偶博弈求解，算法复杂度死死受困于 2-EXPTIME 完全性，在 SYNTCOMP 上止步于 1297 例。Natural Synthesis 利用大模型的高层结构归纳与反例修复绕过了博弈显式构建，直接解出 1467 例。
- vs SemML (Kretínský et al., 2025)：SemML 仅将机器学习作为底层自动机博弈求解中的局部启发式剪枝函数；Natural Synthesis 则直接用大推理模型进行端到端 RTL 代码生成，推理粒度与抽象层次截然不同。
- vs Egolf et al. (2026)：Egolf 等人使用标准 LLM 且受限于门级电路生成与非反例引导，在 SYNTCOMP 上仅解出 229 例且得出 LLM 不擅长反应式合成的悲观结论；本文通过引入 Verilog RTL 抽象、反例引导闭环以及大推理模型（LRMs），反转了这一结论，实现了对符号求解器的全面超越。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐（首次将大推理模型与时序模型检测器紧密耦合形成反例闭环，并在经典反应式合成、不可判定参数化合成及自然语言规范合成上取得里程碑式突破）
- 实验充分度: ⭐⭐⭐⭐⭐（基于 1586 个权威竞赛基准全面对比符号 SOTA 工具，包含细致的思考预算消融、参数化合成以及新建的 NATURAL 基准）
- 写作质量: ⭐⭐⭐⭐⭐（逻辑严密、动机深刻、架构图与案例翔实，理论与工程细节交代极其完备）
- 价值: ⭐⭐⭐⭐⭐（对形式化验证、EDA 自动化芯片设计以及大模型神经符号推理均具有极高的学术与工业应用价值）