exp: 轮次32——均匀细分认证一次调用可证段内碰撞,界经720项检验未证伪,但P50≤20ms的档只能证出54~63%
- certify_uniform:固定 n 个子段一次 gaps 调用,判据与二分同源(子段界=整段界/n),证不出即拒 - 确定界反证:48段×121点×15组对=720项检验 0 违例;有信息量仅 61 项,最紧仍高出 0.035 mm (是"未能在真实运动上证伪",不是证明;浮点误差仍未形式化) - 第180题 1.08-1.10s 漏检段在每个 n>=8 均判碰撞;二次加密(2n+1)反证 0 误放行 - 更正轮次31的"自适应cap无收益":旧公式 bound/2+eps 会把本可通过的子段钳成不可证; 改为 bound+2eps 后交错实测决策不变、快 1.36~1.65x(n=8 13.13→9.68,n=128 98.46→59.76 ms) - 负结论:只有 n<=16 能把认证压进 20 ms,但该档仅证出 26-30/48 根,其余必须刹停; 成本=log(bound/间隙) 决定,故下一步要在反馈后限幅并让安全层要求正余量(现 cap=0.5 会截掉余量) - 测试 23→26 项:n=5拒/n=6受的解析对照、cap_required 公式、n 张量类型门
This commit is contained in:
@@ -0,0 +1,22 @@
|
|||||||
|
{
|
||||||
|
"scope": "全部 48 段 × 15 组对 = 720 项检验;观察值按 cap=2.0 mm 钳制,故可检验命题取 min(预测下限, cap)。违例=实测最小间隙低于该下限。",
|
||||||
|
"checks": 720,
|
||||||
|
"violations": [],
|
||||||
|
"worst_margin_mm": 0.0,
|
||||||
|
"min_slack_mm": 1e-06,
|
||||||
|
"dense_cap_mm": 2.0,
|
||||||
|
"grid_points_per_segment": 121,
|
||||||
|
"supersedes": "docs/experiment_round32_uniform_validation.json 里 bound_checks=61 的部分覆盖版本",
|
||||||
|
"kin_fp": "2ebcbf17",
|
||||||
|
"wall_s": 1.66,
|
||||||
|
"nontrivial": {
|
||||||
|
"definition": "只有预测下限 < 观察 cap 才是有信息量的检验;其余组对被钳制恒等式自动满足",
|
||||||
|
"checks": 61,
|
||||||
|
"min_slack_mm": 0.035347,
|
||||||
|
"p10_slack_mm": 0.544274,
|
||||||
|
"violations": 0,
|
||||||
|
"pred_mm_median_all": 15.8639,
|
||||||
|
"pred_mm_max_all": 19.9582
|
||||||
|
},
|
||||||
|
"note": "720 项总检验 0 违例,其中有信息量的是 61 项;预测下限的中位数 15.9 mm 远大于观察 cap 2 mm,所以大部分组对无法在本网格上证伪"
|
||||||
|
}
|
||||||
@@ -0,0 +1,190 @@
|
|||||||
|
{
|
||||||
|
"device": "cuda float64",
|
||||||
|
"torch": "2.10.0+cu130",
|
||||||
|
"kin_fp": "2ebcbf17",
|
||||||
|
"roots_per_call": 2,
|
||||||
|
"pairs": 24,
|
||||||
|
"warm": 3,
|
||||||
|
"reps": 7,
|
||||||
|
"segment_sample": "docs/experiment_round31_certificates.json 的 48 段两两成对",
|
||||||
|
"design": "每对根轮流按正序/逆序测完全部配置(3次预热+7次计时);uniform_auto 的宽相位=最大子段界+2eps,uniform_cap20 固定 20 mm,bisect 为第31轮逐层二分口径",
|
||||||
|
"results": [
|
||||||
|
{
|
||||||
|
"kind": "uniform_auto",
|
||||||
|
"n_or_budget": 8,
|
||||||
|
"points": 18,
|
||||||
|
"cap_used_mm": 5.9191,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 9.684,
|
||||||
|
"p90_ms": 13.027,
|
||||||
|
"p99_ms": 15.157,
|
||||||
|
"max_ms": 17.537,
|
||||||
|
"over_20ms": 0,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 26,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 21
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_auto",
|
||||||
|
"n_or_budget": 16,
|
||||||
|
"points": 34,
|
||||||
|
"cap_used_mm": 2.9597,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 14.137,
|
||||||
|
"p90_ms": 18.454,
|
||||||
|
"p99_ms": 20.866,
|
||||||
|
"max_ms": 21.632,
|
||||||
|
"over_20ms": 5,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 30,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 17
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_auto",
|
||||||
|
"n_or_budget": 32,
|
||||||
|
"points": 66,
|
||||||
|
"cap_used_mm": 1.4799,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 20.209,
|
||||||
|
"p90_ms": 27.88,
|
||||||
|
"p99_ms": 32.268,
|
||||||
|
"max_ms": 35.563,
|
||||||
|
"over_20ms": 87,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 34,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 13
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_auto",
|
||||||
|
"n_or_budget": 64,
|
||||||
|
"points": 130,
|
||||||
|
"cap_used_mm": 0.7401,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 31.429,
|
||||||
|
"p90_ms": 48.751,
|
||||||
|
"p99_ms": 57.697,
|
||||||
|
"max_ms": 62.084,
|
||||||
|
"over_20ms": 165,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 36,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 11
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_auto",
|
||||||
|
"n_or_budget": 128,
|
||||||
|
"points": 258,
|
||||||
|
"cap_used_mm": 0.3701,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 59.761,
|
||||||
|
"p90_ms": 89.063,
|
||||||
|
"p99_ms": 109.086,
|
||||||
|
"max_ms": 117.345,
|
||||||
|
"over_20ms": 168,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 38,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 9
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_cap20",
|
||||||
|
"n_or_budget": 8,
|
||||||
|
"points": 18,
|
||||||
|
"cap_used_mm": 20.0,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 13.129,
|
||||||
|
"p90_ms": 16.44,
|
||||||
|
"p99_ms": 20.963,
|
||||||
|
"max_ms": 24.67,
|
||||||
|
"over_20ms": 3,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 26,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 21
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_cap20",
|
||||||
|
"n_or_budget": 32,
|
||||||
|
"points": 66,
|
||||||
|
"cap_used_mm": 20.0,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 28.415,
|
||||||
|
"p90_ms": 39.579,
|
||||||
|
"p99_ms": 53.023,
|
||||||
|
"max_ms": 59.983,
|
||||||
|
"over_20ms": 153,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 34,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 13
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_cap20",
|
||||||
|
"n_or_budget": 64,
|
||||||
|
"points": 130,
|
||||||
|
"cap_used_mm": 20.0,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 50.85,
|
||||||
|
"p90_ms": 75.512,
|
||||||
|
"p99_ms": 88.355,
|
||||||
|
"max_ms": 91.492,
|
||||||
|
"over_20ms": 168,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 36,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 11
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "uniform_cap20",
|
||||||
|
"n_or_budget": 128,
|
||||||
|
"points": 258,
|
||||||
|
"cap_used_mm": 20.0,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 98.46,
|
||||||
|
"p90_ms": 139.982,
|
||||||
|
"p99_ms": 167.042,
|
||||||
|
"max_ms": 177.743,
|
||||||
|
"over_20ms": 168,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 38,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 9
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "bisect",
|
||||||
|
"n_or_budget": 32,
|
||||||
|
"points": null,
|
||||||
|
"cap_used_mm": 20.0,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 54.885,
|
||||||
|
"p90_ms": 82.151,
|
||||||
|
"p99_ms": 117.205,
|
||||||
|
"max_ms": 118.716,
|
||||||
|
"over_20ms": 133,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 37,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 10
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"kind": "bisect",
|
||||||
|
"n_or_budget": 65,
|
||||||
|
"points": null,
|
||||||
|
"cap_used_mm": 20.0,
|
||||||
|
"calls": 168,
|
||||||
|
"p50_ms": 71.825,
|
||||||
|
"p90_ms": 108.559,
|
||||||
|
"p99_ms": 122.533,
|
||||||
|
"max_ms": 127.319,
|
||||||
|
"over_20ms": 133,
|
||||||
|
"roots": 48,
|
||||||
|
"safe": 41,
|
||||||
|
"collision": 1,
|
||||||
|
"rejected": 6
|
||||||
|
}
|
||||||
|
],
|
||||||
|
"wall_s": 108.63
|
||||||
|
}
|
||||||
@@ -0,0 +1,62 @@
|
|||||||
|
{
|
||||||
|
"segments": 48,
|
||||||
|
"kin_fp": "2ebcbf17",
|
||||||
|
"dense_cap_mm": 2.0,
|
||||||
|
"eps_mm": 0.0001,
|
||||||
|
"bound_falsification": "每条组对:预测下限 (ga+gb-bound)/2 应 ≤ 网格上该组对的最小实测间隙",
|
||||||
|
"per_segment": [
|
||||||
|
{
|
||||||
|
"n": 8,
|
||||||
|
"safe": 26,
|
||||||
|
"collision": 1,
|
||||||
|
"unproven": 21,
|
||||||
|
"outside_box": 0,
|
||||||
|
"false_accept_vs_dense": 0,
|
||||||
|
"cap_required_mm": 5.919107314806348,
|
||||||
|
"known_missed_segment_collision": true
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"n": 16,
|
||||||
|
"safe": 30,
|
||||||
|
"collision": 1,
|
||||||
|
"unproven": 17,
|
||||||
|
"outside_box": 0,
|
||||||
|
"false_accept_vs_dense": 0,
|
||||||
|
"cap_required_mm": 2.959653657403174,
|
||||||
|
"known_missed_segment_collision": true
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"n": 32,
|
||||||
|
"safe": 34,
|
||||||
|
"collision": 1,
|
||||||
|
"unproven": 13,
|
||||||
|
"outside_box": 0,
|
||||||
|
"false_accept_vs_dense": 0,
|
||||||
|
"cap_required_mm": 1.479926828701587,
|
||||||
|
"known_missed_segment_collision": true
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"n": 64,
|
||||||
|
"safe": 36,
|
||||||
|
"collision": 1,
|
||||||
|
"unproven": 11,
|
||||||
|
"outside_box": 0,
|
||||||
|
"false_accept_vs_dense": 0,
|
||||||
|
"cap_required_mm": 0.7400634143507935,
|
||||||
|
"known_missed_segment_collision": true
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"n": 128,
|
||||||
|
"safe": 38,
|
||||||
|
"collision": 1,
|
||||||
|
"unproven": 9,
|
||||||
|
"outside_box": 0,
|
||||||
|
"false_accept_vs_dense": 0,
|
||||||
|
"cap_required_mm": 0.37013170717539673,
|
||||||
|
"known_missed_segment_collision": true
|
||||||
|
}
|
||||||
|
],
|
||||||
|
"bound_checks": 61,
|
||||||
|
"bound_violations": [],
|
||||||
|
"worst_margin_mm": 0.0
|
||||||
|
}
|
||||||
@@ -603,6 +603,45 @@
|
|||||||
- **口径与边界**:认证只在 float64 下进行,浮点求距误差没有形式上界(`seg_seg_dist` 距离下限约 1e−9 mm),eps=1e−4 mm 是工程容差不是证明;48 段取自轮次 30 修复后的执行轨迹,是固定样本不是新策略闭环;连续认证未接入 rollout,实际执行仍走端点/中点离散检查;速度/加速度超限(轮次 30 实测最大 1.66×VMAX)本轮未处理。
|
- **口径与边界**:认证只在 float64 下进行,浮点求距误差没有形式上界(`seg_seg_dist` 距离下限约 1e−9 mm),eps=1e−4 mm 是工程容差不是证明;48 段取自轮次 30 修复后的执行轨迹,是固定样本不是新策略闭环;连续认证未接入 rollout,实际执行仍走端点/中点离散检查;速度/加速度超限(轮次 30 实测最大 1.66×VMAX)本轮未处理。
|
||||||
- **结论与下一步**:判据确实变强(抓到离散检查漏掉的段内碰撞、未知只拒不放),但成本与 `bound/间隙` 的对数绑定,**当前实现不能部署,也不得把“认证通过”说成零碰撞**。下一步两条:(1) 把逐层依赖的二分改成**一次均匀细分**(固定层数、单个 gaps 调用覆盖全部子段),其实时可行性取决于几何查询成本随批大小是否近似平坦;(2) 把余量要求移到规划/速度侧——实际轨迹贴着 0.001–0.02 mm 间隙走,任何认证方案都会退化成几十次查询,而反馈叠加后的速度约束本来就是未完成项。
|
- **结论与下一步**:判据确实变强(抓到离散检查漏掉的段内碰撞、未知只拒不放),但成本与 `bound/间隙` 的对数绑定,**当前实现不能部署,也不得把“认证通过”说成零碰撞**。下一步两条:(1) 把逐层依赖的二分改成**一次均匀细分**(固定层数、单个 gaps 调用覆盖全部子段),其实时可行性取决于几何查询成本随批大小是否近似平坦;(2) 把余量要求移到规划/速度侧——实际轨迹贴着 0.001–0.02 mm 间隙走,任何认证方案都会退化成几十次查询,而反馈叠加后的速度约束本来就是未完成项。
|
||||||
|
|
||||||
|
## 轮次 32:均匀细分认证与确定界的反证(exp: `exp/dagger-deploy`,认证仍进不了 20 ms,但定位到真正的成本杠杆)
|
||||||
|
|
||||||
|
- **本轮假设**:第31轮的二分认证把成本花在**多次依赖的 gaps 调用**上(B=1 时每次约 7 ms 起步)。若改成固定层数的一次均匀细分,同样的判据应只付一次调用;同时需要单独证明"这个确定界本身没被低估",否则判据再快也没意义。
|
||||||
|
- **实现**:`Kin.certify_uniform(a, b, n, eps, cap=None)`——每根段取 n 个子段、一次 gaps 调用查 n+1 个点,对**每个子段**用与二分版完全相同的判据(子段两端间隙之和 > 子段位移界 + 2eps;界对 Δq 线性,故子段界 = 整段界/n)。没有"未决"状态:证不出就是 `unproven`(拒绝),不存在把未知当安全。未接入 rollout,未改查看器默认。
|
||||||
|
- **确定界的反证**(`docs/experiment_round32_bound_falsification.json`):对 48 段每段取 121 个网格点,逐组对比"实测最小间隙"与"预测下限 (ga+gb−bound)/2"。720 项检验**0 违例**;但只有 **61 项有信息量**(预测下限 < 观察 cap 2 mm 才可能被证伪;其余组对的预测下限中位数 15.9 mm、最大 19.96 mm,都被钳制恒等式自动满足)。61 项里最紧的一项仍比预测下限高 **0.035 mm**,p10 高 0.544 mm。因此这是"未能在真实运动上证伪该界",不是"证明了该界";浮点求距误差仍未做形式化上界。
|
||||||
|
- **接受率曲线**(48 段单根,`docs/experiment_round32_uniform_validation.json`):
|
||||||
|
|
||||||
|
| 子段数 n | 判安全 | 判碰撞 | 证不出 | 二次加密(2n+1点)反证的误放行 |
|
||||||
|
|---|---|---|---|---|
|
||||||
|
| 8 | 26 | 1 | 21 | 0 |
|
||||||
|
| 16 | 30 | 1 | 17 | 0 |
|
||||||
|
| 32 | 34 | 1 | 13 | 0 |
|
||||||
|
| 64 | 36 | 1 | 11 | 0 |
|
||||||
|
| 128 | 38 | 1 | 9 | 0 |
|
||||||
|
|
||||||
|
第180题 1.08–1.10 s 那段(第30轮加密回放检出 −0.14927 mm、原离散证书 `certified=true`)在**每个 n≥8 都判碰撞**。
|
||||||
|
- **宽相位 cap 的正确公式**(对第31轮一条负结论的更正):第31轮用 `bound/2 + eps`,那个值恰好**会把本可通过的子段钳成不可证**,所以既没提速也可能少接受;本轮改成"最小不挡住判定的宽相位"= `最大子段界 + 2eps`,n=4 时是 5.92 mm、n=128 时 0.37 mm。第31轮那句"自适应 cap 无收益"只在旧公式下成立,新公式的实测收益见下表(原记录保留,不回改)。
|
||||||
|
- **计时 A/B**(`docs/experiment_round32_uniform_latency.json`;B=2 根=部署 commit2 口径,24 对根逐对按正序/逆序**交替**测全部配置,每配置 3 次预热 + 7 次计时 = 168 次;CUDA float64):
|
||||||
|
|
||||||
|
| 配置 | 宽相位 mm | P50 | P90 | P99 | >20 ms 次数 | 安全/碰撞/拒(48根) |
|
||||||
|
|---|---|---|---|---|---|---|
|
||||||
|
| 均匀 n=8 auto | 5.92 | **9.68** | 13.03 | 15.16 | 0/168 | 26/1/21 |
|
||||||
|
| 均匀 n=16 auto | 2.96 | **14.14** | 18.45 | 20.87 | 5/168 | 30/1/17 |
|
||||||
|
| 均匀 n=32 auto | 1.48 | 20.21 | 27.88 | 32.27 | 87/168 | 34/1/13 |
|
||||||
|
| 均匀 n=64 auto | 0.74 | 31.43 | 48.75 | 57.70 | 165/168 | 36/1/11 |
|
||||||
|
| 均匀 n=128 auto | 0.37 | 59.76 | 89.06 | 109.09 | 168/168 | 38/1/9 |
|
||||||
|
| 均匀 n=8 cap20 | 20 | 13.13 | 16.44 | 20.96 | 3/168 | 26/1/21 |
|
||||||
|
| 均匀 n=32 cap20 | 20 | 28.41 | 39.58 | 53.02 | 153/168 | 34/1/13 |
|
||||||
|
| 均匀 n=64 cap20 | 20 | 50.85 | 75.51 | 88.36 | 168/168 | 36/1/11 |
|
||||||
|
| 均匀 n=128 cap20 | 20 | 98.46 | 139.98 | 167.04 | 168/168 | 38/1/9 |
|
||||||
|
| 二分 budget32 | 20 | 54.88 | 82.15 | 117.20 | 133/168 | 37/1/10 |
|
||||||
|
| 二分 budget65 | 20 | 71.83 | 108.56 | 122.53 | 133/168 | 41/1/6 |
|
||||||
|
|
||||||
|
- auto 与 cap20 的**决策列完全相同**,只是快 1.36–1.65×(n=8 13.13→9.68、n=128 98.46→59.76):这次是交错实测的真收益,不是第31轮那种顺序漂移。
|
||||||
|
- 单次调用的均匀细分在同样接受率下比二分便宜 5 倍以上(n=8 9.68 ms vs 二分 54.88 ms),但二分在同样时间能多证出 11 根——两条路的取舍由下一段的结论决定,不单看耗时。
|
||||||
|
- **负结论(部署口径)**:只有 n≤16 能把认证本身压进 20 ms(P50 9.68–14.14 ms),而这档只能证出 48 根里的 26–30 根(54–63%),其余必须刹停;n=32 起 P50 就已经吃满 20 ms,还没算推理。所以**连续段认证按现有几何口径不能同时满足"P99<20 ms"和"不牺牲到达"**。这些数是 CUDA float64 的单次调用,不能外推到浏览器 CPU float32 的 50 Hz 链路。
|
||||||
|
- **机理定位与下一步**:成本 = 单次调用固定开销 × 由 `log(bound/间隙)` 决定的层数。要同时拿到"证得出"和"证得起",必须把**间隙抬起来**(安全层要求正余量,而不是 `gap>0`)并把**每步位移压回去**(反馈叠加在 ±1 限幅之后,导致第30轮实测最大 1.66×VMAX,界也随之变大)。顺带记下一个坑:安全层现在是 `kin.gaps(allq, 0.5)`,截顶值 0.5 mm 低于任何 >0.5 mm 的余量门限,直接把余量判据变成恒假——加余量必须同时抬这个 cap。
|
||||||
|
- **回归与判据灵敏度**:`python -m unittest tests.test_eval_cl` **26 项通过**(新增 3 项均匀细分)。含解析对照:合成恒间隙段(界 1 mm/度、间隙 0.1 mm)在 n=5 必判证不出、n=6 必判安全,且 `cap_required_mm` 等于 `1/n+2eps`;薄障碍在 n=4/8/64 判碰撞而 n=2 只判证不出(不误放行);`n` 给成张量被类型门拒绝。二次加密反证在 n=8..128 全部 0 误放行。
|
||||||
|
|
||||||
## 分支清理(2026-10-20)
|
## 分支清理(2026-10-20)
|
||||||
|
|
||||||
- `feat/fb-mix`(8e5431c):反馈混合方案的中间分支,**已验证是 `exp/dagger-deploy` 的祖先**(所有提交都在后者历史里),本地/远端分支删除,内容保留在 exp/dagger-deploy。
|
- `feat/fb-mix`(8e5431c):反馈混合方案的中间分支,**已验证是 `exp/dagger-deploy` 的祖先**(所有提交都在后者历史里),本地/远端分支删除,内容保留在 exp/dagger-deploy。
|
||||||
|
|||||||
+35
-4
@@ -271,7 +271,13 @@ class Kin:
|
|||||||
return gm.view(B, len(gp))
|
return gm.view(B, len(gp))
|
||||||
|
|
||||||
@torch.no_grad()
|
@torch.no_grad()
|
||||||
def certify_segments(self, a, b, max_queries=32, max_depth=12, eps=1e-4, cap=20.0, adaptive_cap=True):
|
def certify_segments(self, a, b, max_queries=32, max_depth=12, eps=1e-4, cap=20.0):
|
||||||
|
"""逐层二分认证:每根段独立查询预算,未知(超预算/超深度/非有限/越界)一律拒绝。
|
||||||
|
|
||||||
|
判据对每条组对:子段两端间隙之和 > 该子段位移界 + 2eps(间隙取 min(gap,cap),钳制只会更保守)。
|
||||||
|
cap 必须 ≥ 该层子段界 + 2eps 才不会挡住本可通过的判定,故不做自适应收紧——同批其他段会改变
|
||||||
|
钳制程度、让结果随批次而变(实测也无耗时收益,见探索日志轮次 31)。
|
||||||
|
"""
|
||||||
if self.dtype != torch.float64 or a.dtype != torch.float64 or b.dtype != torch.float64:
|
if self.dtype != torch.float64 or a.dtype != torch.float64 or b.dtype != torch.float64:
|
||||||
raise ValueError('segment certification requires float64')
|
raise ValueError('segment certification requires float64')
|
||||||
# 预算给成张量时 max_depth + 1 会在 uint8 这类窄类型上回绕成 0,循环整个跳过,把碰撞段当安全返回。
|
# 预算给成张量时 max_depth + 1 会在 uint8 这类窄类型上回绕成 0,循环整个跳过,把碰撞段当安全返回。
|
||||||
@@ -309,9 +315,7 @@ class Kin:
|
|||||||
if not root.numel():
|
if not root.numel():
|
||||||
break
|
break
|
||||||
mid = a + 0.5 * (b - a)
|
mid = a + 0.5 * (b - a)
|
||||||
# 子段的界是父段一半;宽相位只需覆盖到能被证明的最小间隙,层越深筛得越狠。
|
gm = self.gaps(mid, cap)['gm'][:, self.cert_groups]
|
||||||
qc = min(cap, float(bound.max()) / 2 + eps) if adaptive_cap else cap
|
|
||||||
gm = self.gaps(mid, qc)['gm'][:, self.cert_groups]
|
|
||||||
queries += torch.bincount(root, minlength=count)
|
queries += torch.bincount(root, minlength=count)
|
||||||
a, b = torch.cat([a, mid]), torch.cat([mid, b])
|
a, b = torch.cat([a, mid]), torch.cat([mid, b])
|
||||||
ga, gb = torch.cat([ga, gm]), torch.cat([gm, gb])
|
ga, gb = torch.cat([ga, gm]), torch.cat([gm, gb])
|
||||||
@@ -320,6 +324,33 @@ class Kin:
|
|||||||
return {'safe': status == 0, 'collision': status == 1, 'unresolved': status == 2,
|
return {'safe': status == 0, 'collision': status == 1, 'unresolved': status == 2,
|
||||||
'outside_box': status == 3, 'queries': queries}
|
'outside_box': status == 3, 'queries': queries}
|
||||||
|
|
||||||
|
@torch.no_grad()
|
||||||
|
def certify_uniform(self, a, b, n=64, eps=1e-4, cap=None):
|
||||||
|
"""固定层数的均匀细分认证:n 个子段只需一次 gaps 调用(n+1 个点),没有逐层依赖的往返。
|
||||||
|
|
||||||
|
判据与 certify_segments 完全相同;界对 Δq 线性,所以子段界 = 整段界 / n。未通过即 unproven
|
||||||
|
(拒绝),不存在“未知当安全”。cap=None 时取“最小不挡住可通过判定的宽相位”= 最大子段界 + 2eps:
|
||||||
|
小于它钳制会把本可证明的子段压成不可证(偏保守),大于它只是多算对(偏慢),不改正确性。
|
||||||
|
"""
|
||||||
|
if self.dtype != torch.float64 or a.dtype != torch.float64 or b.dtype != torch.float64:
|
||||||
|
raise ValueError('segment certification requires float64')
|
||||||
|
if type(n) is not int or n < 1 or eps <= 0 or (cap is not None and cap <= eps):
|
||||||
|
raise ValueError('invalid subdivision count or tolerance')
|
||||||
|
count = a.shape[0]
|
||||||
|
inside = (((a >= self.lo) & (a <= self.hi) & (b >= self.lo) & (b <= self.hi)) | self.cont).all(-1)
|
||||||
|
bound = (b - a).abs() @ self.cert_lever.T / n # [count,15] 子段界
|
||||||
|
required = float(bound.max()) + 2 * eps if count else 2 * eps
|
||||||
|
qc = required if cap is None else cap
|
||||||
|
alpha = torch.arange(n + 1, dtype=self.dtype, device=a.device) / n
|
||||||
|
points = (a[:, None] + (b - a)[:, None] * alpha[None, :, None]).reshape(-1, 6)
|
||||||
|
gm = self.gaps(points, qc)['gm'][:, self.cert_groups].view(count, n + 1, -1)
|
||||||
|
adjacent = gm[:, :-1] + gm[:, 1:] > bound[:, None, :] + 2 * eps
|
||||||
|
collision = (gm <= 0).any((1, 2))
|
||||||
|
safe = inside & (gm > eps).all((1, 2)) & adjacent.all((1, 2)) & ~collision
|
||||||
|
return {'safe': safe, 'collision': collision, 'unproven': (~safe & ~collision & inside),
|
||||||
|
'outside_box': ~inside, 'points': n + 1, 'queries': n + 1,
|
||||||
|
'cap_required_mm': required, 'cap_used_mm': qc}
|
||||||
|
|
||||||
def min_gap(self, q, cap=40.0):
|
def min_gap(self, q, cap=40.0):
|
||||||
return self.gaps(q, cap)['gm'].min(-1).values
|
return self.gaps(q, cap)['gm'].min(-1).values
|
||||||
|
|
||||||
|
|||||||
@@ -477,6 +477,47 @@ class SegmentCertificateTest(unittest.TestCase):
|
|||||||
self.assertEqual(result['collision'].tolist(), [True, False])
|
self.assertEqual(result['collision'].tolist(), [True, False])
|
||||||
self.assertEqual(result['outside_box'].tolist(), [False, True])
|
self.assertEqual(result['outside_box'].tolist(), [False, True])
|
||||||
|
|
||||||
|
def test_uniform_matches_bound_formula_and_needs_no_round_trips(self):
|
||||||
|
class ConstantGap(self.ThinObstacle):
|
||||||
|
def gaps(self, q, cap):
|
||||||
|
return {'gm': torch.full((q.shape[0], 1), 0.1, dtype=q.dtype, device=q.device)}
|
||||||
|
|
||||||
|
# 界 1 mm/度、间隙 0.1 mm:子段判据 0.2 > 1/n 需要 n ≥ 6,n=5 必须落 unproven。
|
||||||
|
kin = ConstantGap()
|
||||||
|
kin.cert_lever = torch.ones(1, 6, dtype=torch.float64)
|
||||||
|
a, b = torch.zeros(1, 6, dtype=torch.float64), torch.zeros(1, 6, dtype=torch.float64)
|
||||||
|
b[:, 0] = 1.0
|
||||||
|
for n, safe in ((5, False), (6, True)):
|
||||||
|
with self.subTest(n=n):
|
||||||
|
result = kin.certify_uniform(a, b, n=n)
|
||||||
|
self.assertEqual(bool(result['safe'].item()), safe)
|
||||||
|
self.assertEqual(result['points'], n + 1)
|
||||||
|
self.assertFalse(bool(result['collision'].item()))
|
||||||
|
self.assertEqual(bool(result['unproven'].item()), not safe)
|
||||||
|
self.assertAlmostEqual(result['cap_required_mm'], 1.0 / n + 2e-4, places=9)
|
||||||
|
|
||||||
|
def test_uniform_catches_hidden_collision_and_rejects_short_grids(self):
|
||||||
|
a = torch.tensor([[0.0, 0, 0, 0, 0, 0], [-1.0, 0, 0, 0, 0, 0], [6.0, 0, 0, 0, 0, 0]], dtype=torch.float64)
|
||||||
|
b = torch.tensor([[1.0, 0, 0, 0, 0, 0], [0.0, 0, 0, 0, 0, 0], [6.0, 0, 0, 0, 0, 0]], dtype=torch.float64)
|
||||||
|
kin = self.ThinObstacle()
|
||||||
|
short = kin.certify_uniform(a, b, n=2)
|
||||||
|
self.assertEqual(short['collision'].tolist(), [False, False, False])
|
||||||
|
self.assertEqual(short['unproven'].tolist(), [True, False, False])
|
||||||
|
self.assertEqual(short['safe'].tolist(), [False, True, False])
|
||||||
|
for n in (4, 8, 64):
|
||||||
|
with self.subTest(n=n):
|
||||||
|
result = kin.certify_uniform(a, b, n=n)
|
||||||
|
self.assertEqual(result['collision'].tolist(), [True, False, False])
|
||||||
|
self.assertEqual(result['safe'].tolist(), [False, True, False])
|
||||||
|
self.assertEqual(result['outside_box'].tolist(), [False, False, True])
|
||||||
|
|
||||||
|
def test_uniform_requires_plain_int_count(self):
|
||||||
|
a = torch.zeros(1, 6, dtype=torch.float64)
|
||||||
|
for tensor in (torch.tensor(8, dtype=torch.uint8), torch.tensor(8)):
|
||||||
|
with self.subTest(dtype=tensor.dtype):
|
||||||
|
with self.assertRaisesRegex(ValueError, 'subdivision count'):
|
||||||
|
self.ThinObstacle().certify_uniform(a, a.clone(), n=tensor)
|
||||||
|
|
||||||
def test_nonfinite_and_outside_box_are_rejected(self):
|
def test_nonfinite_and_outside_box_are_rejected(self):
|
||||||
a, b = torch.zeros(1, 6, dtype=torch.float64), torch.zeros(1, 6, dtype=torch.float64)
|
a, b = torch.zeros(1, 6, dtype=torch.float64), torch.zeros(1, 6, dtype=torch.float64)
|
||||||
kin = self.ThinObstacle()
|
kin = self.ThinObstacle()
|
||||||
|
|||||||
Reference in New Issue
Block a user