SDRPC-PRIME-001 Validation Phase I — Round 13

Counterexample-Guided Adaptive Policy Synthesis

日期： 2026-09-23
Domain： odd 3 ≤ n ≤ 2,000,000

作者： Neo.K
機構： EveMissLab／一言諾科技有限公司
版本： 原稿未標註（本次整理版）

1. 這次 Policy 不再人工指定

Round 12 是 exhaustive / curated policy search。

Round 13 改成 counterexample-guided synthesis：

start with empty policy
-> find lowest surviving composite witness
-> among atoms that reject this witness,
   choose the best composite-elimination / generation-cost atom
-> append only on the all-pass branch
-> repeat

Prime truth 只用於 validation / safety gate；registered atom 不允許誤拒 prime。

2. Synthesized Policy

D3 → D5 → D7 → S2 → S7 → S3

Depth = 6
Average atoms evaluated = 2.955
Average probe-generation proxy = 23.000
Composite fallback = 0

3. Synthesis Trace

這張表是真正的『policy 生長史』：每個新 atom 都有一個具體 counterexample forcing event。

4. Counterexample 在這裡不只是反駁

現在 witness 有三個角色：

1. 證明目前 policy insufficient；
2. 限定下一輪候選 atom 必須真的能分裂它；
3. 成為 policy graph 中新增 node 的 provenance。

所以：

counterexample -> repair obligation -> operator insertion

CGPR 在這裡正式變成 synthesis rule。

5. 與其他 Policy 比較

這個比較很重要：counterexample-guided greedy 不保證找到全域最低 burden policy。

它的價值是：

every added operator has a witnessed necessity at insertion time

而 exhaustive search 的優勢則是能找到更好的全域排列，但缺少同樣清楚的生成 provenance。

6. Greedy Policy 與 Global-Greedy Control

Counterexample-guided：D3 → D5 → D7 → S2 → S7 → S3。

Global elimination/cost greedy：D3 → D5 → D7 → S2 → S7 → S3。

如果兩者不同，代表『先修眼前反例』和『最大化整體淘汰效率』是兩個不同 objective。

這是 proof-policy synthesis 的第一個真正 control problem。

7. Ablation：插入過的 Atom 後來還必要嗎？

• 移除 D3 → fallback=0, first=None, avg probe=28.963
• 移除 D5 → fallback=0, first=None, avg probe=25.648
• 移除 D7 → fallback=0, first=None, avg probe=24.588
• 移除 S2 → fallback=8, first=703, avg probe=18.946
• 移除 S7 → fallback=3, first=1373653, avg probe=18.933
• 移除 S3 → fallback=1, first=314821, avg probe=18.933

這裡故意做 post-hoc ablation。

因為一個 atom 在插入當下可能是必要的，但後續加入更強 atom 後，它可能變成冗餘。

所以：

insertion-time necessity != final-policy necessity

這表示 synthesis 後還需要 compression / pruning pass。

8. 這就是一個新的 Proof Policy 生命週期

目前完整流程已經變成：

counterexample discovery
-> local repair
-> policy growth
-> new counterexample
-> further repair
-> zero-repair candidate
-> global ablation
-> policy compression
-> certificate handoff

它和傳統一次性寫出固定 proof script 很不一樣。

9. Policy Graph 已可序列化

本輪輸出 policy_graph.json，每個 node 保存：

• atom；
• fail edge；
• pass edge；
• terminal certificate handoff。

而 synthesis_trace.json 保存它為什麼長出來。

所以現在不只 proof 可 replay，proof architecture 的形成過程也可 replay。

10. 對算子本體論的再前進

前面是：

operator set
-> operator order
-> branch semantics

現在再多一層：

operator provenance

也就是每個 operator 為什麼被加入，必須由某個 unresolved state / witness 支撐。

這使 operator ontology 從靜態 ontology 變成演化 ontology。

11. Round 13 的限制

• atom grammar 是人工給定的；
• witness selection 固定為 lowest surviving composite；
• objective 是局部 elimination/cost greedy；
• 沒有證明 synthesized policy globally optimal；
• zero fallback 仍只對 finite domain 有效。

所以這是 synthesis prototype，不是新 primality theorem。

12. 下一輪

Round 14 最值得做：

Policy Pruning + Branch-Specific Atom Invention

兩部分：

1. 對 synthesized policy 做最小化，刪除被後續 operators 支配的歷史修補；
2. 不只從固定 atom grammar 選，開始允許從 counterexample fiber 自動生成 candidate relational probes。

也就是從：

choose an atom

升級成：

invent a probe that splits the unresolved fiber

那才真正會開始碰到 SDRPC 原本想要的新搜尋法。

13. Round 13 結論

counterexamples can synthesize proof policy structure;
local repair decisions carry provenance;
insertion-time necessity may disappear after later refinements;
therefore synthesis must be followed by pruning;
proof architecture can itself be a replayable evolving object.

Round 13: COMPLETE
Next: Round 14 — Policy Pruning + Branch-Specific Atom Invention