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

• URL: http://arxiv.org/abs/2509.06239v2
• Date: Mon, 20 Oct 2025 22:10:34 GMT
• Title: Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning
• Authors: Manvi Jha, Jiaxin Wan, Deming Chen,
• Abstract summary: This work presents Proof2Silicon, a novel end-to-end synthesis framework.<n>It embeds the previously proposed PREFACE flow to enable the generation of correctness-by-construction hardware directly from natural language specifications.
• Score: 7.574481956683386
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• ShortCoder: Knowledge-Augmented Syntax Optimization for Token-Efficient Code Generation [27.9837392531619]
  We propose a knowledge-infused framework named ShortCoder to optimize code generation efficiency.<n>ShortCoder consistently outperforms state-of-the-art methods on HumanEval.
  arXiv  Detail & Related papers  (2026-01-14T18:57:31Z)
• Compiling Prompts, Not Crafting Them: A Reproducible Workflow for AI-Assisted Evidence Synthesis [1.624454100511275]
  Large language models (LLMs) offer significant potential to accelerate systematic literature reviews.<n>Current approaches often rely on brittle, manually crafted prompts that compromise reliability and rigour.<n>This research proposes a structured, domain-specific framework that embeds task declarations, test suites, and automated prompt tuning into a reproducible SLR.
  arXiv  Detail & Related papers  (2025-08-22T21:37:49Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• ChipSeek-R1: Generating Human-Surpassing RTL with LLM via Hierarchical Reward-Driven Reinforcement Learning [32.11086992218369]
  ChipSeek-R1 is a hierarchical reward-driven reinforcement learning framework for large language models.<n>It generates RTL code that is both functional correctness and PPA-optimized.<n>On the RTLLM benchmark, ChipSeek-R1 generated 27 RTL designs surpassing the PPA metrics of the original human-written code.
  arXiv  Detail & Related papers  (2025-07-07T08:08:20Z)
• QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation [51.393569044134445]
  Large language models (LLMs) trained via reinforcement learning with verifiable reward (RLVR) have achieved breakthroughs on tasks with explicit, automatable verification.<n> Extending RLVR to automatically generating hardware description languages (HDLs) like Verilog from natural-language (NL) specifications, however, poses three key challenges.<n>We introduce CodeV-R1, an RLVR framework for training Verilog generation LLMs.
  arXiv  Detail & Related papers  (2025-05-30T03:51:06Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• TuRTLe: A Unified Evaluation of LLMs for RTL Generation [0.6010802600885173]
  We propose TuRTLe, a unified evaluation framework designed to assess LLMs across key RTL generation tasks.<n>We benchmark a diverse set of open LLMs and analyze their strengths and weaknesses in EDA-specific tasks.<n>Our results show that reasoning-based models, such as DeepSeek R1, consistently outperform others across multiple evaluation criteria.
  arXiv  Detail & Related papers  (2025-03-31T07:43:12Z)
• HDLCoRe: A Training-Free Framework for Mitigating Hallucinations in LLM-Generated HDL [8.078194378107936]
  HDLCoRe is a training-free framework that enhances large language models' HDL generation capabilities.<n>Our framework achieves superior performance on the RTLLM2.0 benchmark.
  arXiv  Detail & Related papers  (2025-03-18T07:09:39Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  Iterative refinement has emerged as an effective paradigm for enhancing the capabilities of large language models (LLMs) on complex tasks. We propose Context-Wise Order-Agnostic Language Modeling (COrAL) to overcome these challenges. Our approach models multiple token dependencies within manageable context windows, enabling the model to perform iterative refinement internally.
  arXiv  Detail & Related papers  (2024-10-12T23:56:19Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  Large language models (LLMs) have rapidly advanced and demonstrated impressive capabilities. In-Context Learning (ICL) and. Efficient Fine-Tuning (PEFT) are currently two mainstream methods for augmenting. LLMs to downstream tasks. We propose Reference Trustable Decoding (RTD), a paradigm that allows models to quickly adapt to new tasks without fine-tuning.
  arXiv  Detail & Related papers  (2024-09-30T10:48:20Z)
• AIvril: AI-Driven RTL Generation With Verification In-The-Loop [0.7831852829409273]
  Large Language Models (LLMs) are computational models capable of performing complex natural language processing tasks. This paper introduces AIvril, a framework designed to enhance the accuracy and reliability of RTL-aware LLMs.
  arXiv  Detail & Related papers  (2024-09-03T15:07:11Z)
• StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback [58.20547418182074]
  We introduce StepCoder, a novel framework for code generation, consisting of two main components. CCCS addresses the exploration challenge by breaking the long sequences code generation task into a Curriculum of Code Completion Subtasks. FGO only optimize the model by masking the unexecuted code segments to provide Fine-Grained Optimization. Our method improves the ability to explore the output space and outperforms state-of-the-art approaches in corresponding benchmarks.
  arXiv  Detail & Related papers  (2024-02-02T13:14:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.