一句话：提出 SynVer，用两个 LLM 分别合成 C 程序候选并生成 Rocq/VST 正确性证明，实现高保障 C 程序合成。
本文提出 SynVer，一个面向 C 程序的通用合成器，目标是生成带机器检查正确性证明的高保障程序。SynVer 使用两个大型语言模型：第一个根据用户规约生成候选 C 程序，第二个在 Rocq 证明助手中借助 Verified Software Toolchain 自动构造其正确性证明。为便于验证，SynVer 对候选程序施加一组语法限制，使其适合自动化推理，并采用符号推理与 LLM 驱动证明生成相结合的混合验证策略，以处理符号引擎无法独立完成的证明义务。作者使用来自程序合成与验证文献的多样化基准展示了该方法的适用性。
We present SynVer — a novel, general purpose synthesizer for C programs equipped with machine-checked proofs of correctness using the Verified Software Toolchain. To do so, SynVer employs two Large Language Models (LLMs): the first generates candidate programs from user-provided specifications, and the second helps automatically construct formal proofs of their correctness in the Rocq proof assistant. To facilitate verification, SynVer places a set of syntactic restrictions on candidate programs that make them amenable to automated reasoning. SynVer uses a hybrid verification strategy that combines symbolic reasoning with LLM-powered proof generation to discharge proof obligations that the symbolic engine cannot handle on its own. We demonstrate the applicability of SynVer using a diverse set of benchmarks drawn from the program synthesis and verification literature.
DOI 原文 ·
@inproceedings{paperbot9201,
title = {LLM-Assisted Synthesis of High-Assurance C Programs},
author = {Prasita Mukherjee and Minghai Lu and Benjamin Delaware},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00255}
}