用代码生成自然语言问题,自动检测规范与代码一致性并优化。
Fidelity Probes for Specification--Code Alignment

- 从代码生成带真值答案的问题,评估规范与代码匹配度。
- 在COBOL基准上将规范一致性从0.63提升至0.94,8轮迭代收敛。
- 支持多模型、多分析路径融合,可识别不一致并指导修改。
我们提出保真度探针:从参考代码生成自然语言问题,以代码推导的真值答案为标准,由候选规范作答。探针回答一致率称为保真度,可分解为矛盾率和覆盖缺口率,用于指导针对性规范修改直至收敛。在包含15个程序、约1.2万行代码的COBOL基准(AWS CardDemo)上,经过八轮迭代,冻结测试集上的规范保真度从0.63提升至0.94;其收敛位置可通过仅四轮数据估算的两状态马尔可夫固定点 $F^$ 预测。探针来源包括大模型读取代码或基于控制流、数据流、系统依赖图的静态分析管道,支持可调混合。采用冻结保留集的探针重采样协议,提供霍夫丁界约束的过拟合判别器;实测训练/测试差距远低于该边界一个数量级以上。三种图结构驱动的混合方式使保真度提升16至30点;跨分布评估表明大模型与符号化通道具有经验互补性。对五个独立大模型家族(Anthropic、DeepSeek、Google、Alibaba、OpenAI)的生成器扫面确认,收敛行为不依赖单一模型家族:其中三个非Claude生成器轨迹符合马尔可夫固定点预测,而两个探针分布随迭代漂移的生成器被冻结测试协议主动证伪。该方法适用于任何应描述同一行为的双产物对。
原文摘要 · Abstract (English)
We introduce fidelity probes: natural-language questions generated from a reference artifact with code-derived ground-truth answers, answered from a candidate specification. The fraction of agreeing probes, which we call the fidelity, decomposes into contradiction and coverage-gap rates that drive targeted spec edits to convergence. On a 15-program, roughly 12k-line COBOL benchmark (AWS CardDemo), we raise frozen-test specification fidelity from 0.63 to 0.94 over eight iterations, with the plateau location predicted by a two-state Markov fixed point $F^\dagger$ from just four iterations of rate data. Probes come from an LLM reading the code or from a static-analysis pipeline over its control-flow, data-flow, and system-dependence graphs, with a tunable mixture. A probe-resampling protocol with a frozen held-out set gives a Hoeffding-bounded overfitting discriminant; our measured train/test gap stays more than an order of magnitude below this envelope. Three graph-grounded mixtures lift fidelity by +16 to +30 points; cross-distribution evaluation shows the LLM and symbolic channels are empirically complementary. A cross-family generator sweep on five independent LLM lineages (Anthropic, DeepSeek, Google, Alibaba, OpenAI) confirms the convergence behaviour is not tied to any single model family: three of five non-Claude generators produce trajectories consistent with the Markov fixed-point prediction, and the frozen-test protocol actively falsifies the two generators whose probe distributions drift across iterations. The method applies to any pair of artifacts that are supposed to describe the same behaviour.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。