这周只挑了一条。上周一挂上 arXiv 的一篇，编号 2611.03641，干的事是让大模型解斑马谜题。
听着像玩具题。有意思的不是题本身，是里面那个循环。
简单说，他们没让模型自己一步步往下推。模型只干一件事：把自然语言里的实体和约束翻成一组结构化的工具调用。这些调用拼成一个精确覆盖的实例，扔给求解器。
求解器是老东西。SAT 和精确覆盖这套办法保证正确、保证完备，代价是问题得先写成它能吃的格式。
分工很清楚。模糊的那头归模型，要穷举、要保证不漏的那头归求解器。
这也不是新提法。神经符号这个词喊了有些年，真正用起来一直不顺手。多数做法是把两套东西硬凑一块，模型照旧自己猜，求解器最后验一下对不对。
这篇的差别在中间那一层。求解器的报错会回到模型手里，变成下一轮的输入。
报错分得挺细。写进去的约束可能压根没约束到任何东西，也可能漏了条件，还可能加得太狠把唯一解挤掉了。三种情况回给模型的话不一样，改法也不一样。
值得单独说一句的，是它让模型交什么。模型交的不是一段解释，是一组结构化的调用。解释没法验，调用能验。
我看到这里才觉得这条值得收。
斑马谜题有个硬性质：答案唯一。整个回路靠这一条撑着。编码跑出来的解不唯一，或者干脆无解，那就不是题怪，是编码写错了。这个判断是机器给的，不是模型自己觉得。
模型没资格说“我觉得对了”。
论文里跟思维链提示比了，混合方法稳定赢。跟近期几个神经符号的做法比，也赢。评估铺得挺开，多个参数规模、多种后训练方式、好几个模型系列都跑了一遍。
这个结果我不意外。
思维链的问题从来不是想得不够多。是没人给它判卷。它自己往下写，自己觉得通顺，就接着走，走岔了也接着走，写到最后一段还挺像那么回事。
有裁判和没裁判，差的不是一点。
我前面说多数神经符号落地不顺手，原因大概也在这。校验放在最后一步，等于白校验。模型已经把话编圆了，你这时候告诉它错了，它只能在圆的上面打补丁。
让它每一轮都被打断，效果不一样。
边界得说清楚，不然容易读成什么都能这么干。
它要两件事同时成立：问题能形式化成精确覆盖这类结构，答案还得唯一可验。缺一条，裁判就没了。
还有句老实话。我没跑过它的代码，下面的判断基于论文里的描述和它给出的对比结果。
精确覆盖那部分的形式化我只看懂了一半，先放在这里。作者怎么把“红房子在蓝房子左边”翻成集合约束，我大致跟上了。再往下的编码细节，等我弄明白再补一句。
有一件事我比较确定。以后看一个 AI 工具靠不靠谱，先别问模型多大，问它旁边有没有裁判。
写代码这件事正好自带一个。跑不跑得起来，测试过不过，都是机器说了算。同样一个大模型，放在编辑器里和放在聊天框里，手感差很远。不是模型换了，是旁边多了一个会说“你这儿错了”的东西。
没裁判的场景，那个位置就得你自己站上去。让它写，你验。这一步省不掉。
这期就一条。挑这么少，是因为别的我讲不清楚，硬塞进来也是占地方。
上面有任何一条你试过、或者觉得我讲错了，欢迎告诉我。讲错的我补，没讲清的我改。
本周就这些，下周见。