Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning

📄 arXiv: 2509.06239v2 📥 PDF

作者: Manvi Jha, Jiaxin Wan, Deming Chen

分类: cs.AI

发布日期: 2025-09-07 (更新: 2025-10-20)

💡 一句话要点

Proof2Silicon：基于强化学习的提示修复，实现可验证代码与硬件生成

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式验证 硬件综合 强化学习 大型语言模型 代码生成

📋 核心要点

  1. 现有LLM代码生成常无法通过形式验证，限制了其在硬件和安全关键领域的应用。
  2. Proof2Silicon利用强化学习迭代修复LLM提示，引导生成可验证的Dafny代码，无需微调。
  3. 实验表明，该方法显著提升了Dafny验证成功率，并实现了端到端的硬件综合。

📝 摘要（中文）

大型语言模型(LLMs)在自动代码生成方面表现出令人印象深刻的能力，但经常生成无法通过形式验证的代码，而形式验证是硬件和安全关键领域的基本要求。为了克服这一根本限制，我们之前提出了PREFACE，这是一个基于强化学习(RL)的、与模型无关的框架，它迭代地修复提供给冻结LLM的提示，系统地引导它们生成可形式验证的Dafny代码，而无需昂贵的微调。本工作提出了Proof2Silicon，一种新颖的端到端综合框架，它嵌入了先前提出的PREFACE流程，以实现直接从自然语言规范生成构造正确的硬件。Proof2Silicon的运作方式是：(1)利用PREFACE的验证器驱动的RL代理来迭代地优化提示生成，确保Dafny代码的正确性；(2)使用Dafny的Python后端和PyLog自动将经过验证的Dafny程序翻译成可综合的高级C代码；(3)采用Vivado HLS来生成RTL实现。在具有挑战性的100个任务的基准上进行了严格的评估，PREFACE的RL引导的提示优化始终将各种LLM的Dafny验证成功率提高了高达21%。至关重要的是，Proof2Silicon实现了高达72%的端到端硬件综合成功率，通过Vivado HLS综合流程生成RTL设计。这些结果展示了一个鲁棒、可扩展和自动化的LLM驱动的、形式验证的硬件综合流水线，弥合了自然语言规范和硅实现之间的差距。

🔬 方法详解

问题定义：论文旨在解决LLM生成的代码难以通过形式验证的问题，尤其是在硬件设计等安全攸关领域。现有方法要么依赖于代价高昂的LLM微调，要么无法保证生成代码的正确性，导致无法直接应用于硬件综合。

核心思路：论文的核心思路是利用强化学习(RL)来迭代优化LLM的输入提示(prompt)，从而引导LLM生成满足形式验证要求的代码。通过验证器驱动的奖励函数，RL代理能够学习如何修改提示，使得LLM更有可能生成正确的Dafny代码。

技术框架：Proof2Silicon框架包含三个主要阶段：(1) 使用PREFACE框架，通过RL优化LLM的提示，生成可验证的Dafny代码；(2) 将Dafny代码自动翻译成可综合的C代码，利用Dafny的Python后端和PyLog实现；(3) 使用Vivado HLS工具将C代码综合成RTL硬件描述。

关键创新：该方法最重要的创新点在于使用RL进行提示修复，这是一种模型无关的方法，可以应用于各种LLM，而无需对LLM进行微调。此外，该框架实现了从自然语言规范到硬件实现的端到端自动化流程，显著降低了硬件设计的门槛。

关键设计：PREFACE框架中的RL代理使用验证器的输出来作为奖励信号，引导提示的优化。具体的奖励函数设计和RL算法选择（例如，策略梯度方法）是影响性能的关键因素。此外，Dafny到C代码的翻译以及Vivado HLS的配置也会影响最终硬件的性能和资源利用率。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，PREFACE的RL引导提示优化将Dafny验证成功率提高了高达21%。更重要的是，Proof2Silicon实现了高达72%的端到端硬件综合成功率，证明了该方法在实际硬件设计中的有效性。这些结果优于直接使用LLM生成代码并进行综合的方法。

🎯 应用场景

该研究成果可应用于自动化硬件设计、安全关键系统开发等领域。通过将自然语言规范转化为可验证的硬件实现，可以显著提高设计效率和可靠性，降低开发成本。未来，该技术有望推动定制化硬件的快速开发和部署，加速人工智能在嵌入式系统中的应用。

📄 摘要（原文）

Large Language Models (LLMs) have demonstrated impressive capabilities in automated code generation but frequently produce code that fails formal verification, an essential requirement for hardware and safety-critical domains. To overcome this fundamental limitation, we previously proposed PREFACE, a model-agnostic framework based on reinforcement learning (RL) that iteratively repairs the prompts provided to frozen LLMs, systematically steering them toward generating formally verifiable Dafny code without costly fine-tuning. This work presents Proof2Silicon, a novel end-to-end synthesis framework that embeds the previously proposed PREFACE flow to enable the generation of correctness-by-construction hardware directly from natural language specifications. Proof2Silicon operates by: (1) leveraging PREFACE's verifier-driven RL agent to optimize prompt generation iteratively, ensuring Dafny code correctness; (2) automatically translating verified Dafny programs into synthesizable high-level C using Dafny's Python backend and PyLog; and (3) employing Vivado HLS to produce RTL implementations. Evaluated rigorously on a challenging 100-task benchmark, PREFACE's RL-guided prompt optimization consistently improved Dafny verification success rates across diverse LLMs by up to 21%. Crucially, Proof2Silicon achieved an end-to-end hardware synthesis success rate of up to 72%, generating RTL designs through Vivado HLS synthesis flows. These results demonstrate a robust, scalable, and automated pipeline for LLM-driven, formally verified hardware synthesis, bridging natural-language specification and silicon realization.