exp+fix: 轮次31——确定界连续认证抓到段内碰撞，但单段P50 22.9ms进不了20ms；自适应cap收益经交错复测撤回
- Kin.cert_lever 用三角不等式给全姿态位移界（替代 JS 随机采样×1.05），界量级 5.93–48.86 mm/整步 - Kin.certify_segments 批量前沿二分+每根查询预算：48 固定段中预算32判安全37/碰撞1/未知拒10， 第180题1.08–1.10s漏检段以5次查询判碰撞；未知只拒不放 - 修 seg_seg_dist 第二条退化成点不投影（模型内退化胶囊686受影响）；但7586个加密点的组最小间隙 逐位不变、2000样本JS对拍仍 PASS → 不解释轮次30漏检、不改既有成绩 - 负结论：B=1 单段认证 P50 22.93/P90 58.43/P99 101.57 ms，432次中225次>20ms； 自适应宽相位 cap 交错复测耗时无收益，先前1.6×为GPU顺序漂移，已在日志撤回 - 成本模型 L=ceil(log2(bound/(ga+gb)))、查询=2^L+1 与实测对齐（安全段2–17次，未知段33–65次） - 新增8项段认证测试+1项回放测试（14→23项通过）；变异实测证明张量 max_depth 回绕会误放行
This commit is contained in:
+71
-1
@@ -38,7 +38,8 @@ def seg_seg_dist(p1, q1, p2, q2, eps=1e-12):
|
||||
s = torch.where(t_lo, (-c / a.clamp_min(eps)).clamp(0, 1), s)
|
||||
s = torch.where(t_hi, ((b - c) / a.clamp_min(eps)).clamp(0, 1), s)
|
||||
t = t.clamp(0, 1)
|
||||
# 退化（线段长度≈0）
|
||||
# 第二条退化成点时，仍须在第一条上投影，而不是固定取其起点。
|
||||
s = torch.where(e <= eps, (-c / a.clamp_min(eps)).clamp(0, 1), s)
|
||||
s = torch.where(a <= eps, torch.zeros_like(s), s)
|
||||
t = torch.where(e <= eps, torch.zeros_like(t), t)
|
||||
c1 = p1 + d1 * s.unsqueeze(-1)
|
||||
@@ -85,6 +86,25 @@ class Kin:
|
||||
gi, gj = self.cap_g[self.pi], self.cap_g[self.pj]
|
||||
self.pair_gp = torch.minimum(gi, gj) * 7 + torch.maximum(gi, gj)
|
||||
self.lever = T(K['lever'])
|
||||
table = [[0.0] * 7 for _ in range(6)]
|
||||
for group in range(1, 7):
|
||||
endpoints = [c[key] for c in caps if c['g'] == group for key in ('a', 'b')]
|
||||
if not endpoints:
|
||||
continue
|
||||
pivot, axis = K['P'][group - 1], K['D'][group - 1]
|
||||
unit = [v / math.hypot(*axis) for v in axis]
|
||||
relative = [[e[j] - pivot[j] for j in range(3)] for e in endpoints]
|
||||
radius = max(math.hypot(*v) for v in relative)
|
||||
radial = max(math.hypot(v[1] * unit[2] - v[2] * unit[1],
|
||||
v[2] * unit[0] - v[0] * unit[2],
|
||||
v[0] * unit[1] - v[1] * unit[0]) for v in relative)
|
||||
for joint in range(group):
|
||||
chain = sum(math.dist(K['P'][j], K['P'][j + 1]) for j in range(joint, group - 1))
|
||||
table[joint][group] = (chain + (radial if joint == group - 1 else radius)) * D2R
|
||||
self.cert_groups = torch.tensor([a * 7 + b for a in range(7) for b in range(a + 2, 7)], device=device)
|
||||
# 三角不等式给出全姿态界，不用随机姿态最大值冒充上界。
|
||||
self.cert_lever = T([[table[k][b] if a <= k < b else 0.0 for k in range(6)]
|
||||
for a in range(7) for b in range(a + 2, 7)])
|
||||
|
||||
# ---------------- 运动学 ----------------
|
||||
def cum_xf(self, q):
|
||||
@@ -250,6 +270,56 @@ class Kin:
|
||||
gm = gm.scatter_reduce(0, rep_b * len(gp) + self._gp49[self.pair_gp[pidx]], gap.clamp(max=cap), reduce='amin', include_self=True)
|
||||
return gm.view(B, len(gp))
|
||||
|
||||
@torch.no_grad()
|
||||
def certify_segments(self, a, b, max_queries=32, max_depth=12, eps=1e-4, cap=20.0, adaptive_cap=True):
|
||||
if self.dtype != torch.float64 or a.dtype != torch.float64 or b.dtype != torch.float64:
|
||||
raise ValueError('segment certification requires float64')
|
||||
# 预算给成张量时 max_depth + 1 会在 uint8 这类窄类型上回绕成 0，循环整个跳过，把碰撞段当安全返回。
|
||||
if type(max_queries) is not int or type(max_depth) is not int:
|
||||
raise ValueError('certification budgets must be plain ints')
|
||||
if max_queries < 2 or max_depth < 0 or eps <= 0 or cap <= eps:
|
||||
raise ValueError('invalid certification budget or tolerance')
|
||||
count = a.shape[0]
|
||||
status = torch.zeros(count, dtype=torch.long, device=a.device)
|
||||
inside = (((a >= self.lo) & (a <= self.hi) & (b >= self.lo) & (b <= self.hi)) | self.cont).all(-1)
|
||||
status[~inside] = 3
|
||||
root = torch.arange(count, device=a.device)
|
||||
gaps = self.gaps(torch.cat([a, b]), cap)['gm'][:, self.cert_groups]
|
||||
ga, gb = gaps[:count], gaps[count:]
|
||||
queries = torch.full((count,), 2, dtype=torch.long, device=a.device)
|
||||
bound = (b - a).abs() @ self.cert_lever.T
|
||||
for depth in range(max_depth + 1):
|
||||
finite = torch.isfinite(ga).all(-1) & torch.isfinite(gb).all(-1)
|
||||
collision = (ga <= 0).any(-1) | (gb <= 0).any(-1)
|
||||
status[root[~finite]] = 2
|
||||
status[root[collision]] = 1
|
||||
positive = (ga > eps).all(-1) & (gb > eps).all(-1)
|
||||
proven = positive & (ga + gb > bound + 2 * eps).all(-1)
|
||||
pending = (status[root] == 0) & ~proven
|
||||
if not bool(pending.any()):
|
||||
break
|
||||
a, b, ga, gb, root, bound = a[pending], b[pending], ga[pending], gb[pending], root[pending], bound[pending]
|
||||
if depth == max_depth:
|
||||
status[root] = 2
|
||||
break
|
||||
requested = torch.bincount(root, minlength=count)
|
||||
status[(status == 0) & (queries + requested > max_queries)] = 2
|
||||
keep = status[root] == 0
|
||||
a, b, ga, gb, root, bound = (t[keep] for t in (a, b, ga, gb, root, bound))
|
||||
if not root.numel():
|
||||
break
|
||||
mid = a + 0.5 * (b - a)
|
||||
# 子段的界是父段一半；宽相位只需覆盖到能被证明的最小间隙，层越深筛得越狠。
|
||||
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)
|
||||
a, b = torch.cat([a, mid]), torch.cat([mid, b])
|
||||
ga, gb = torch.cat([ga, gm]), torch.cat([gm, gb])
|
||||
root = torch.cat([root, root])
|
||||
bound = torch.cat([bound, bound]) / 2
|
||||
return {'safe': status == 0, 'collision': status == 1, 'unresolved': status == 2,
|
||||
'outside_box': status == 3, 'queries': queries}
|
||||
|
||||
def min_gap(self, q, cap=40.0):
|
||||
return self.gaps(q, cap)['gm'].min(-1).values
|
||||
|
||||
|
||||
+126
-3
@@ -153,11 +153,124 @@ def replay_dense(path, indices, max_step_deg=0.05, device='cpu', out=None):
|
||||
return result
|
||||
|
||||
|
||||
@torch.no_grad()
|
||||
def replay_certificates(path, indices, device='cpu', out=None, repeats=5, extra_segments=()):
|
||||
saved = torch.load(path, map_location='cpu', weights_only=True)
|
||||
kin = Kin(device=device, dtype=torch.float64)
|
||||
if saved.get('kin_fp') != kin.fp:
|
||||
raise ValueError('trace/kin fingerprint mismatch')
|
||||
if not indices or min(indices) < 0 or max(indices) >= len(saved['tasks']) or repeats < 1:
|
||||
raise ValueError('valid task indices and positive repeats required')
|
||||
rows, offset = [], 0
|
||||
for _, per, count in saved['batches']:
|
||||
for index in indices:
|
||||
if not offset <= index < offset + count:
|
||||
continue
|
||||
b = index - offset
|
||||
nstep = min(per['traj'].shape[1] - 1, math.floor((float(per['limit'][b]) + 1e-6) / DT))
|
||||
if torch.isfinite(per['t_done'][b]):
|
||||
nstep = min(nstep, round(float(per['t_done'][b]) / DT))
|
||||
traj = per['traj'][b, :nstep + 1]
|
||||
moving = ((traj[1:] - traj[:-1]).abs().max(-1).values > 1e-6).nonzero().flatten().tolist()
|
||||
if not moving:
|
||||
continue
|
||||
plans = per['plans']
|
||||
nearest, nearest_gap = None, float('inf')
|
||||
for it in moving:
|
||||
pi = int(torch.searchsorted(plans['it'], it, right=True)) - 1
|
||||
step = it - int(plans['it'][pi])
|
||||
if 0 <= step < plans['commit'].shape[2] and plans['certified'][b, pi, step]:
|
||||
gap = float(plans['gaps'][b, pi, [step, plans['commit'].shape[2] + step]].min())
|
||||
if gap < nearest_gap:
|
||||
nearest, nearest_gap = it, gap
|
||||
selected = {moving[0], moving[len(moving) // 2], moving[-1]}
|
||||
if nearest is not None:
|
||||
selected.add(nearest)
|
||||
for task_index, it in extra_segments:
|
||||
if task_index == index:
|
||||
if it not in moving:
|
||||
raise ValueError('extra segment must be a moving segment before deadline or arrival')
|
||||
selected.add(it)
|
||||
for it in sorted(selected):
|
||||
rows.append({'i': index, 'start_it': it, 'a': traj[it].tolist(), 'b': traj[it + 1].tolist()})
|
||||
offset += count
|
||||
if not rows:
|
||||
raise ValueError('no moving segments in selected tasks')
|
||||
a = torch.tensor([r['a'] for r in rows], dtype=torch.float64, device=device)
|
||||
b = torch.tensor([r['b'] for r in rows], dtype=torch.float64, device=device)
|
||||
started = time.perf_counter()
|
||||
print('certificate replay: %d tasks, %d fixed moving segments' % (len(indices), len(rows)), flush=True)
|
||||
summaries = {}
|
||||
for budget in (2, 8, 32):
|
||||
result = kin.certify_segments(a, b, max_queries=budget)
|
||||
summaries[str(budget)] = {key: int(result[key].sum()) for key in ('safe', 'collision', 'unresolved', 'outside_box')}
|
||||
summaries[str(budget)]['queries_p50'] = float(result['queries'].double().quantile(0.5))
|
||||
summaries[str(budget)]['queries_max'] = int(result['queries'].max())
|
||||
for j, row in enumerate(rows):
|
||||
row.setdefault('budgets', {})[str(budget)] = {key: value[j].item() for key, value in result.items()}
|
||||
print('budget %d: %s' % (budget, summaries[str(budget)]), flush=True)
|
||||
latencies = []
|
||||
for j, row in enumerate(rows):
|
||||
aa, bb = a[j:j + 1], b[j:j + 1]
|
||||
discrete = kin.gaps(torch.cat([aa, aa + 0.5 * (bb - aa), bb]), 0.5)['gm'].min(-1).values
|
||||
row['previous_midpoint_endpoint_gap_mm'] = discrete.tolist()
|
||||
nseg = max(2, 2 * math.ceil(float((bb - aa).abs().max()) / 0.02))
|
||||
alpha = torch.linspace(0, 1, nseg + 1, dtype=torch.float64, device=device)
|
||||
points = aa + alpha[:, None] * (bb - aa)
|
||||
dense = torch.cat([kin.gaps(chunk, 0.5)['gm'].min(-1).values for chunk in points.split(64)])
|
||||
row['dense_points'] = len(points)
|
||||
row['dense_min_gap_mm'] = float(dense.min())
|
||||
row['dense_min_fraction'] = float(alpha[dense.argmin()])
|
||||
for _ in range(3):
|
||||
kin.certify_segments(aa, bb)
|
||||
elapsed = []
|
||||
for _ in range(repeats):
|
||||
if a.is_cuda:
|
||||
torch.cuda.synchronize(a.device)
|
||||
t0 = time.perf_counter()
|
||||
result = kin.certify_segments(aa, bb)
|
||||
if a.is_cuda:
|
||||
torch.cuda.synchronize(a.device)
|
||||
elapsed.append((time.perf_counter() - t0) * 1000)
|
||||
row['batch_single_match'] = all(value.item() == row['budgets']['32'][key] for key, value in result.items())
|
||||
row['latency_ms'] = elapsed
|
||||
latencies.extend(elapsed)
|
||||
print('segment %d/%d task %d it %d dense %.6f mm queries %d latency %.2f ms' %
|
||||
(j + 1, len(rows), row['i'], row['start_it'], row['dense_min_gap_mm'],
|
||||
row['budgets']['32']['queries'], sum(elapsed) / len(elapsed)), flush=True)
|
||||
elapsed = torch.tensor(latencies, dtype=torch.float64)
|
||||
result = {
|
||||
'trace': str(path), 'tasks_sha256': saved.get('tasks_sha256'), 'kin_fp': kin.fp,
|
||||
'device': str(device), 'gpu': torch.cuda.get_device_name(a.device) if a.is_cuda else None,
|
||||
'torch_version': str(torch.__version__), 'cpu_threads': torch.get_num_threads(), 'dtype': 'float64',
|
||||
'indices': indices, 'extra_segments': list(extra_segments),
|
||||
'selection': 'First/middle/last moving segment and minimum original certified gap per task; plus explicit extra_segments.',
|
||||
'cap_mm': 20.0, 'eps_mm': 1e-4, 'max_depth': 12, 'dense_max_step_deg': 0.01,
|
||||
'timing': {'scope': 'B=1 certificate only, resident inputs, 3 warmups per segment; synchronized wall time, not policy or scheduling latency.',
|
||||
'repeats_per_segment': repeats, 'calls': len(latencies),
|
||||
'p50_ms': float(elapsed.quantile(0.5)), 'p99_ms': float(elapsed.quantile(0.99)),
|
||||
'max_ms': float(elapsed.max()), 'over_20ms': int((elapsed > 20).sum())},
|
||||
'budgets': summaries,
|
||||
'dense_collision_segments': sum(r['dense_min_gap_mm'] <= 0 for r in rows),
|
||||
'accepted_dense_collision_segments': sum(r['dense_min_gap_mm'] <= 0 and r['budgets']['32']['safe'] for r in rows),
|
||||
'batch_single_match': all(r['batch_single_match'] for r in rows),
|
||||
'scope': 'Fixed recorded segments, not a new rollout. Dense replay is finite sampling; floating-point certification error is not formally bounded.',
|
||||
'wall_s': time.perf_counter() - started, 'rows': rows,
|
||||
}
|
||||
if out:
|
||||
with open(out, 'w', encoding='utf-8') as f:
|
||||
json.dump(result, f, indent=2, allow_nan=False)
|
||||
return result
|
||||
|
||||
|
||||
def main():
|
||||
ap = argparse.ArgumentParser()
|
||||
ap.add_argument('--ckpt')
|
||||
ap.add_argument('--trace')
|
||||
ap.add_argument('--dense_indices', help='逗号分隔的任务下标；回放实际轨迹，不依赖原 col 标记')
|
||||
ap.add_argument('--cert_indices', help='固定实际段的连续认证、加密对照和单段计时')
|
||||
ap.add_argument('--cert_segments', default='', help='额外指定任务号:零基段号，逗号分隔')
|
||||
ap.add_argument('--repeats', type=int, default=5)
|
||||
ap.add_argument('--max_step_deg', type=float, default=0.05)
|
||||
ap.add_argument('--samples', default='ml/data/samples')
|
||||
ap.add_argument('--split', default='val')
|
||||
@@ -169,14 +282,24 @@ def main():
|
||||
ap.add_argument('--device', default='cuda' if torch.cuda.is_available() else 'cpu')
|
||||
ap.add_argument('--out', default=None)
|
||||
a = ap.parse_args()
|
||||
if a.dense_indices and a.cert_indices:
|
||||
ap.error('--dense_indices and --cert_indices are mutually exclusive')
|
||||
if a.cert_segments and not a.cert_indices:
|
||||
ap.error('--cert_segments requires --cert_indices')
|
||||
if a.trace:
|
||||
if a.dense_indices:
|
||||
if a.cert_indices:
|
||||
extra = [tuple(map(int, segment.split(':'))) for segment in a.cert_segments.split(',') if segment]
|
||||
indices = [int(i) for i in a.cert_indices.split(',')]
|
||||
if any(len(segment) != 2 or segment[0] not in indices for segment in extra):
|
||||
ap.error('--cert_segments requires task:segment pairs from --cert_indices')
|
||||
replay_certificates(a.trace, indices, a.device, a.out, a.repeats, extra)
|
||||
elif a.dense_indices:
|
||||
replay_dense(a.trace, [int(i) for i in a.dense_indices.split(',')], a.max_step_deg, a.device, a.out)
|
||||
else:
|
||||
replay_first_hits(a.trace, a.out)
|
||||
return
|
||||
if a.dense_indices:
|
||||
ap.error('--dense_indices requires --trace')
|
||||
if a.dense_indices or a.cert_indices:
|
||||
ap.error('--dense_indices and --cert_indices require --trace')
|
||||
if not a.ckpt:
|
||||
ap.error('--ckpt or --trace is required')
|
||||
|
||||
|
||||
Reference in New Issue
Block a user