用大模型自动把自然语言需求转成电路，效果超过传统工具。
Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
- 大模型+模型检验器迭代修复电路代码
- 在竞赛中解决的测试用例比顶尖工具多
- 支持参数化系统设计，适合非专家使用
反应式综合是自动从逻辑规范生成硬件电路的长期挑战，主要因算法困难和人工编写形式化规格难度大。本文从算法与规格两方面突破：算法上提出神经符号方法，通过大模型与模型检验器协同，利用可靠符号反馈迭代修复生成的Verilog代码；该方法在年度合成竞赛中解决的基准测试数量超过最佳专用工具，并可扩展至参数化系统（已知不可判定问题）。规格方面，引入自动形式化步骤，将规范任务从时序逻辑转为自然语言，基于人工编写的自然语言规格数据集进行评估，性能接近直接使用形式化规格，证明自然合成可作为端到端可行工作流。
原文摘要 · Abstract (English)
Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this paper, we tackle both sides of the problem. For the algorithmic side, we present a neuro-symbolic approach to reactive synthesis that couples large reasoning models with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmarks than the best dedicated tools in the annual synthesis competition and extends to constructing parameterized systems, a problem known to be undecidable. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language by introducing a hand-authored dataset of natural-language specifications for evaluation. We demonstrate performance comparable to that of starting from formal specifications, establishing natural synthesis as a viable end-to-end workflow.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。