来源笔记
Inferring Code Correctness from Specification
摘要
TRAILS 通过测试程序行为，再让 LLM 将得到的输入输出对与规格说明进行比对，来判断某个生成程序是否符合自然语言规格。它针对的是 LLM 生成代码的 oracle 问题，也就是用户常常没有可信测试用例可用。
问题
- LLM 生成的代码看起来可能合理，却违反规格；这很重要，因为开发者和非专业用户可能会在没有可信 oracle 的情况下接受错误代码。
- 动态一致性方法需要多个候选程序和大量执行，成本高。静态代码推理会漏掉运行时 bug，而且不同模型运行之间的结果会变化。
- 这篇论文研究的是单个候选程序的正确性推断，只使用规格和候选代码，不使用可信测试、示例或用户反馈。
方法
- TRAILS 先让 LLM 从规格中提取行为类别和前置条件。
- 对每个类别，它生成候选输入，在代码上运行，按固定预算修复无效输入，丢弃无效分区，并按代码覆盖率去掉重复输入。
- 它把剩余输入运行到候选代码上，收集具体输出。
- 它把规格和单个输入输出对交给 LLM，不展示代码，并要求给出二元正确性判断。
- 它把每个输入的判断汇总成一个分数，并与阈值比较，文中报告了 τ = 0.6、0.7 和 0.8。
结果
- 评估使用了经过筛选后的 LiveCodeBench v4 Lite，119 个任务，以及 CoCoClaNeL，161 个任务。它测试了 Qwen3Coder-30B、Devstral-Small-24B 和 Olmo3.1-32B-Instruct，并与 HoarePrompt 和 Zero-Shot COT 比较，结果取 3 次重复运行的平均值。
- 在 LiveCodeBench 上，最佳 MCC 分数分别是：Qwen 0.661，对比 Zero-Shot COT 的 0.612 和 HoarePrompt 的 0.605；Devstral 0.550，对比 0.463 和 0.357；Olmo 0.606，对比 0.464 和 0.355。相对 Zero-Shot COT 的 MCC 提升分别达到 8.01%、18.79% 和 30.60%。
- 在 CoCoClaNeL 上，最佳 MCC 分数分别是：Qwen 0.259，对比 Zero-Shot COT 的 0.186 和 HoarePrompt 的 0.223；Devstral 0.261，对比 0.212 和 0.223；Olmo 0.431，对比 0.332 和 0.269。相对 Zero-Shot COT 的 MCC 提升分别达到 39.24%、23.11% 和 29.82%。
- P4 在最强结果上也有提升：LiveCodeBench 的 Qwen 达到 0.825，对比 Zero-Shot COT 的 0.804；LiveCodeBench 的 Olmo 达到 0.803，对比 0.723；CoCoClaNeL 的 Qwen 达到 0.617，对比 0.512；CoCoClaNeL 的 Olmo 达到 0.711，对比 0.591。
- TRAILS 的 token 成本更高：表 1 中每个任务需要 18.6k 到 37.5k tokens，而 HoarePrompt 为 11.3k 到 20.6k，Zero-Shot COT 为 1.1k 到 2.5k。论文把额外成本主要归因于输入修复，尤其是在遇到会崩溃的错误代码和 CoCoClaNeL 中的标准输入格式时。
- 摘要声称它在带随机种子的重复运行中更稳定，并且能给更多独特代码样本打出正确标签。不过，给出的摘录里没有这些稳定性或独特标签数量的具体数值。