丑寅同墟·星海抉择 解题记录

全程用小扎的Muse Spark 1.2 Contributor 加上下依赖的时间 10分钟解出来了

这题给了个叫 ICTFForCausalLM 的小模型，inference.py 里就是读一行字符串、转成 input_ids、过 dense+ReLU+lm_head、取 argmax 打印一个字符。字符集是 0-9a-zA-Z 62个，加上 <success> 和 <fail> 凑 64，输入最多 16个字符，不够补 0。

我先把 model.safetensors 用 numpy 解出来看权重，头 8字节后跟着 JSON，能直接拿到四张表：dense.weight[21,16]、dense.bias[21]、lm_head.weight[64,21]、lm_head.bias[64]。一看 lm_head 就很离谱：0..61 行全 0、bias -10000，63 行（<fail>）全 0、bias 0.4，62 行（<success>）是 [1, -1e10, -1e10, ...]、bias -376131.22。这意味着 logit_fail 永远是 0.4，别的字符永远 -10000 没机会，logit_success = hidden0 -376131.22 -1e10*sum(hidden1..20的正部分)。

想让 <success> 赢，必须让 hidden1..20 全部 ≤0（ReLU 后是 0，不会乘到 -1e10），同时 hidden0 >376131.62。hidden = W·x + b，b0 是 311558.72，所以需要 W0·x >64573。这样整个问题就变成了 16个变量 0..61 的线性不等式组：20个 W_i·x + b_i ≤0，1个 W0·x + b0 >376131.62。

我用 z3 建了这个模型，Int 变量 16个，约束照着权重填进去，跑 check() 直接 sat，给出一组解 [15,1,10,16,2,0,2,6,12,7,15,10,1,6,6,6]，转回字符就是 f1ag2026c7fa1666。拿 numpy float32 复算了一下，hidden 正好是 [376131.72,0,0,...,0]，20个全 0，logits62 0.5 比 0.4 刚好高 0.1，pred 62 就是 <success>。

怕是巧合，我试了把最后一位改成 7 变成 f1ag2026c7fa1667，立刻 hidden4 18>0，logits 直接掉到 -3e12 变 <fail>；改开头 flag... 也不行。还加了个约束 xs != flag 再跑 z3，结果 unsat，说明在 16位 0..61 范围里就这一个能触发成功。

所以模型里藏的秘密就是这个输入串，交 flag 直接：f1ag2026c7fa1666。

flag：f1ag2026c7fa1666