这题乍一看是 AI 题，给了个叫 ICTFForCausalLM 的语言模型和权重，要求找出触发 <success> 的 16 字符 flag。但扒开代码一看，其实是一道纯粹的白盒逆向/密码学题。

第一步肯定是看源码 model_def.py。这根本不是什么 Transformer 结构，就是一个极简的两层多层感知机（MLP）。

梳理一下核心逻辑：

爆破空间是 $62^{16}$，直接算肯定不现实。

既然整个前向传播的逻辑非常清晰，而且模型权重完全在手（白盒），这本质上就是一个多元一次方程组的求解问题。直接把网络里的矩阵乘法和 ReLU 翻译成数学约束，丢给 SMT 求解器（比如 Z3）硬算就行。

写 EXP 的核心就是把 PyTorch 的计算图用 Z3 的 API 重新手搓一遍。代码如下，关键点写了注释：

环境对了就能直接跑出 flag。

import torch
from z3 import *
from model_def import ICTFForCausalLM, ICTFTokenizer

print("[*] Loading model weights...")
tokenizer = ICTFTokenizer()
model = ICTFForCausalLM.from_pretrained("./ictf_model")

# Extract the fixed weights and biases
W1 = model.dense.weight.detach().numpy()
b1 = model.dense.bias.detach().numpy()
W2 = model.lm_head.weight.detach().numpy()
b2 = model.lm_head.bias.detach().numpy()

print("[*] Building Z3 constraints...")
solver = Solver()

# Define our 16 input characters as integers
X_int = [Int(f'x_{i}') for i in range(16)]

# Constraint: Valid token IDs fall within the 62-character charset (0 to 61)
for i in range(16):
    solver.add(X_int[i] >= 0, X_int[i] <= 61)

# Cast to Real for Z3's continuous math calculations
X_real = [ToReal(x) for x in X_int]

# Layer 1: Dense + ReLU
H_relu = []
for j in range(21): # hidden_size is 21
    # H_j = sum(X_i * W1[j, i]) + b1[j]
    node_val = Sum([X_real[i] * float(W1[j, i]) for i in range(16)]) + float(b1[j])
    # ReLU: max(0, node_val)
    H_relu.append(If(node_val > 0, node_val, RealVal(0)))

# Layer 2: lm_head (We only care about logits for valid chars + success token)
logits = []
for k in range(64): # vocab_size is 64
    logit_val = Sum([H_relu[j] * float(W2[k, j]) for j in range(21)]) + float(b2[k])
    logits.append(logit_val)

# Constraint: The logit for <success> (ID 62) must be the absolute maximum
success_logit = logits[62]
for k in range(64):
    if k != 62:
        solver.add(success_logit > logits[k])

print("[*] Solving for the flag...")
if solver.check() == sat:
    m = solver.model()
    flag_ids = [m[X_int[i]].as_long() for i in range(16)]
    flag = tokenizer.decode(flag_ids)
    print(f"\n[+] Success! Flag recovered: {flag}")
else:
    print("\n[-] UNSAT: Could not find a valid input sequence.")

[*] Loading model weights...
[*] Building Z3 constraints...
[*] Solving for the flag...

[+] Success! Flag recovered: f1ag2026c7fa1666