# v0.7.0 增量验证与既有基准

v0.7.0 与不可变 v0.6.1 发布引擎在相同预算、任务、评分和机器上进行三轮交替顺序重放。表格首候选均为 179/225、至少一个候选正确均为 191/225，新增与回退均为 0；46 道首候选失败继续保留。字符串在相同协议 2（训练上限 32）两版均为 104/104，完全相同拆分去重后为 51/51。没有借本轮扩展改变分母或训练拆分。[三轮对照](evidence/comparison-v0.6.1-v0.7.0.json) · [本轮表格逐题结果](evidence/benchmark-v0.7.0.json) · [本轮字符串逐题结果](evidence/sygus-v0.7.0.json)

新覆盖的是排序程序及其结构组合：128 组 Python Decimal/稳定排序构造对照、三个新批次流程均通过。这些不是新增的独立盲测，不计入 Foofah/SyGuS 成绩。[排序对照](evidence/sorting-v0.7.0.json)

表格三轮分位数中位数：v0.6.1 P50/P95 为 133.2/207.0 ms，v0.7.0 为 131.7/212.4 ms。此结果不支持普遍加速声明；新能力的目标是扩大可表达和可学习的程序范围。本轮核心源码为 `483a8f38056008dbff1661150f7fc9da784853e2`，Windows 引擎 SHA-256 为 `d348cdc42391ad5ecdc2cdcf1c291929bb0f4c325d00ff886cd5342f85fc3edd`。复现时设置 `BASELINE_VERSION=0.6.1`，获取对应发布引擎后执行现有对照脚本。

## v0.6.0 的评测结果与口径修正

字符串在新口径下为 104/104，表格为 179/225，表格仍有 46 道未达到首候选全对。下表的两版使用相同输入、预算和评分条件。成功要求每道题的全部留出单元格、行序和输出形状一致。

| 指标 | v0.5.1 | v0.6.0 |
| --- | ---: | ---: |
| Foofah 训练一致 / 全部文件 | 214/250 | 231/250 |
| Foofah 首候选留出整表全对 | 158/225 | 179/225 |
| Foofah 至少一个候选正确 | 174/225 | 191/225 |
| Foofah 搜索 P50 / P95 | 144.4 / 236.1 ms | 148.6 / 234.9 ms |
| 字符串协议 2（训练上限 32）训练一致 | 88/104 | 104/104 |
| 字符串协议 2 首候选留出全对 | 88/104 | 104/104 |
| 字符串协议 2 相同拆分去重后全对 | 45/51 | 51/51 |
| 字符串协议 2 搜索 P50 / P95 | 55.8 / 116.7 ms | 58.0 / 97.3 ms |
| 字符串协议 1（训练上限 6）首候选全对 | 88/104 | 101/104 |

## 字符串训练信息修正

原评测按输入哈希排序后取前 `min(6,n−1,ceil(2n/3))` 条训练。univ_3-long 与 univ_4/5/6-long 得到了相同的六条训练样例，却在两个相同测试输入上要求不同的输出。一种意图保留州名 New York，另一种意图改为 NY。在只传训练样例和相同选项的接口下，这组意图无法被区分，首候选指标的保守上界为 103/104。[原口径审计](evidence/string-audit-protocol1-v0.6.0.json)

协议 2 将训练上限提高到库已支持的 32，仍按相同输入哈希排序，训练 `min(32,n−1,ceil(2n/3))` 条，其余全部留出。选择规则只用输入和样例数，测试标签及文件名均不传给学习器。更完整的训练信息消除了上述同训练、异答案的冲突。两版均在该拆分上重新运行。训练及留出内容改变，算法增幅应从同口径的两版对照计算。[新口径逐题结果](evidence/sygus-protocol2-v0.6.0.json) · [原口径重放](evidence/sygus-protocol1-v0.6.0.json)

固定上游全部 108 份文件仍在清单中。四份文件各自包含同一输入要求两种不同输出的原始约束，确定性函数无法同时满足。审计记录了文件 SHA-256、约束序号和输入/输出摘要。其余 104 份进入训练与泛化评估。相同训练/留出内容合并后为 51 个拆分，题族之间仍有关联。[原题与固定版本](https://github.com/SyGuS-Org/benchmarks/tree/13c8deb68a873635879c9a69bc78caebd340f646/comp/2017/PBE_Strings_Track) · [新口径及原始约束审计](evidence/string-audit-protocol2-v0.6.0.json)

该题库参与了本轮错误定位，104/104 是固定口径下的复现结果。该评估验证输入输出转换，未强制使用原 SyGuS 题目的语法。原始语法及题目名没有作为额外意图输入。上游根目录未提供统一许可文件，原题下载到本地忽略目录，公开快照包含摘要与统计。两个协议均为全部可评估文件保留错误和超时，不能把缺答案或矛盾约束的文件记作已通过。

## 表格任务与剩余差距

Foofah 保留固定提交中的全部 250 个 exp0 文件、50 个任务族。25 份使用缺答案占位值，其中五份超过输入列数上限，全部仍列入库存与训练统计。225 份有测试答案的任务进入留出评分，TestAnswer 仅在合成后核验。[来源和 MIT 许可](../fixtures/foofah/README.md) · [逐题结果](evidence/benchmark-v0.6.0.json)

旧新各跑三轮并交替先后顺序，各题的训练和留出判定稳定。本次新增 21 道首候选通过，回退 0 道。46 道首候选未通过，其中 12 道已找到可通过的候选，当前排名没有将其放在首位。另有 34 道候选覆盖或泛化不足。候选任一个正确是使用参考答案事后计算的上界，自动运行选定程序时不能获得该信息。[完整对照和增减清单](evidence/comparison-v0.5.1-v0.6.0.json)

两版都有 245/250 道报告搜索截断。外层上限保持 4 步、128 状态、2000 次结构尝试和 8 候选。数据已用于项目迭代，50 个任务族内变体也有关联。成绩用于复现和诊断，实际应用需要验证自己的转换规则。

有些失败还需要核对预期布局。exp0_6_1 的训练目标按日期、产品、数值排列，测试参考按产品、日期、数值排列。exp0_29_1 的训练目标交替排列金额与数量，测试参考先列出全部金额，再列出全部数量。额外训练样例或明确的输出格式约束才能说明这类布局选择。这些任务继续计入失败。[日期与产品样例](../fixtures/foofah/exp0_6_1.txt) · [金额与数量样例](../fixtures/foofah/exp0_29_1.txt)

## 搜索代价与复现

字符串两版统一使用 8 候选、6 拼接段、4000 次原子求值、30000 步和 1024 前沿状态。新版完整字段小搜索与全语法共用这一步数预算。缓存统计为两阶段累计值。各题采用独立 Worker，5 秒超时覆盖启动、合成和重放，毫秒耗时只测合成调用。

表格耗时为每版三轮分位数的中位数，字符串每口径每版运行一轮，逐题轮换先后顺序。Windows / i7-14650HX / Node v24.22.1 为该轮环境，CPU 负载会影响耗时。比较没有测量 PROSE 或 Foofah 本体。

本轮引擎 SHA-256 为 `f38ace4de5feacc1ef276b406c102a3ac6fcd9fcc94ae76f1b282b63d6ff27a6`，测量源码为[固定提交](https://github.com/zhangbowen2006/ExampleLoom/tree/d271cc38d12b6c068884d2292988acea3ed8f1f6)。

```sh
node scripts/build.mjs
python scripts/fetch-baseline.py
node scripts/compare-benchmarks.mjs
python scripts/import-sygus.py
python scripts/audit-string-benchmark.py
node scripts/benchmark-strings.mjs --paired
```

PowerShell 下可用 `$env:SYGUS_TRAIN_LIMIT="6"` 后重新导入来重放协议 1，完成后移除该变量再重新导入以恢复协议 2。两种运行的 JSON 都标记协议与训练上限。旧记录见 [v0.5.1 报告](https://github.com/zhangbowen2006/ExampleLoom/blob/v0.5.1/docs/BENCHMARKS.md)。

pandas 的 36 组构造验证和 IANA/SQLite 工作流也已复测。72 次显式管道执行与参考实现一致，36 组构造任务在新输入上首候选正确。[实际运行记录](VALIDATION.md) · [pandas 语义对照](evidence/pandas-v0.6.0.json)