自然合成：优于具有大型推理模型的反应合成工具

反应式综合，即根据逻辑规范自动构建硬件电路的问题，是形式验证中长期存在的挑战。它难以捉摸有两个原因：它在算法上很难，并且手工编写正式规范是出了名的困难。在本文中，我们解决了问题的两个方面。对于算法方面，我们提出了一种反应合成的神经符号方法，它将大型推理模型与模型检查器结合起来，通过声音符号反馈迭代修复合成的 Verilog 实现。我们的方法比年度综合竞赛中最好的专用工具解决了更多的基准，并扩展到构建参数化系统，这是一个已知的不可判定的问题。在规范方面，我们引入了一个自动形式化步骤，通过引入用于评估的手工编写的自然语言规范数据集，将规范任务从时间逻辑转移到自然语言。我们展示了与从正式规范开始的性能相当的性能，将自然合成建立为可行的端到端工作流程。