0x00 题目

附件给了一个字符级“语言模型”：

 model_def.py：模型定义 + tokenizer
 inference.py：加载模型，输入 ≤16 字符，输出一个字符
 ictf_model/：权重（safetensors）

特殊的是 vocab 里 id 62 = <success>，id 63 = <fail>。目标：找到让模型输出 <success> 的输入。
0x01 模型结构
text

x (16个token id) → Linear(16→21) → ReLU → Linear(21→64) → logits

tokenizer 字符集是 0-9a-zA-Z 共 62 个字符，输入不足 16 位补 '0'（id=0）。注意：模型输入的不是 embedding，是裸的 token id 序列，整个网络就是个 16 维到 64 维的分段线性函数。
0x02 权重分析（关键）

直接读 safetensors：
python

from safetensors.torch import load_file
sd = load_file("ictf_model/model.safetensors")
W1, b1 = sd["dense.weight"], sd["dense.bias"] # [21,16] [21]
W2, b2 = sd["lm_head.weight"], sd["lm_head.bias"] # [64,21] [64]

几个决定性发现：

① 输出层 success 行：
text

W2[62] = [1, -1e10, -1e10, ..., -1e10] (21维)
b2[62] = -376131.21875

h₁~h₂₀ 任何一个 > 0（ReLU 激活后），logit₆₂ 就乘上 -10¹⁰ 直接崩到 -10¹⁴ 级别 → <fail>。所以成功的前提是 20 个守卫单元全部死区：
text

W1[j]·x + b1[j] ≤ 0 (j = 1..20)

② 其他输出类的权重大全是幌子：
类别

W2[k][0]

b2[k]

效果
0~61（正常字符） 0 -10000 恒定小值，凑数
62 <success> 1 -376131.22 = h₀ - 376131.22
63 <fail> 0 0.4 唯一真对手，恒 0.4

③ 阈值约束： 打败 <fail> 需要：
text

logit₆₂ = h₀ - 376131.22 > 0.4
h₀ = W1[0]·x + b1[0], b1[0] = 311558.71875
⟹ W1[0]·x ≥ 64573 (W1 全是整数，向上取整)

其中 W1[0] = [3012, 1679, 78, -1143, 1231, 5574, 2091, 1452, -3472, 1990, 17, 1987, 109, 3758, 1295, -492]，b1[1..20] 也全是整数——出题人留好了路，这就是个整数线性规划。
0x03 求解

21 条线性约束 + 16 个 [0,63] 整数变量，直接 CP-SAT 全枚举：
python

from ortools.sat.python import cp_model

model = cp_model.CpModel()
x = [model.NewIntVar(0, 63, f"x{i}") for i in range(16)]

20 条守卫约束: h1..h20 <= 0

for j in range(1, 21):
model.Add(sum(int(W1[j][i]) * x[i] for i in range(16)) <= -int(b1[j]))

阈值约束: h0 - 376131.22 > 0.4

model.Add(sum(int(W1[0][i]) * x[i] for i in range(16)) >= 64573)

solver = cp_model.CpSolver()
solver.parameters.enumerate_all_solutions = True

... 枚举所有解

结果：全枚举 OPTIMAL，可行解有且仅有 1 个：
text

f1ag2026c7fa1666

0x04 验证
text

$ echo "f1ag2026c7fa1666" | python3 inference.py
<success>

$ echo "f1ag2026c7fa1665" | python3 inference.py # 改最后一位
<fail>
$ echo "f1ag2026c7fa166" | python3 inference.py # 截短
<fail>

Flag
text

flag{f1ag2026c7fa1666}