把数独题里的数字换成 MNIST 手写体，让机器解。这条赛道上的脚印很密：2019 年 SatNet 用可微 MAXSAT 啃过；都灵理工这组人 2023 年在同一个基准上亲手把数独规则写进逻辑张量网络；到了这篇，规则也懒得手写了——让大模型自己猜，机器自己验。
分工是这样的。VLM（Groq 上的 Llama-4-Maverick-17B，帖子没提这位猜谜选手的名字）看 3 个带标注的例子，按一套严格语法提出一阶逻辑规则候选，交给动态逻辑张量网络：规则现场编译成计算图，可微地验一遍。验证失败，报错喂回去，猜的下一轮重提。循环，直到 AUC 摸到 0.95 的收敛线——实际跑了 9 到 19 轮。三个训练样本是真的，论文表里白纸黑字：VLM Load = 3。
成绩单：四个域 AUC 0.94、0.93、0.88、0.87，NeuPSL 全线被压，对最强的 LTN-IND 变体一平三胜。"D-LTN"的 D 在于计算图按候选规则运行时编译——语法树就是计算图，这一步做得干净。
这篇真正的论点藏在分工里：治幻觉，未必要把猜的人教老实；配一个手里攥着答案键的审计，更便宜。AlphaGeometry 和 AlphaProof 是同款人事制度——大胆的管猜，死板的管验，谁也别越岗。
猜的管猜，验的管验。就这么回事。