大语言模型形式化中的类求解器行为

研究发现 LLM 形式化模型在生成程序前常通过推理链直接解题，这种类求解器行为（SLB）在 85% 的轨迹中出现，且占 24% 的推理 token，但通常与程序输出冗余。 SLB 在命令式 Python 中比声明式 Z3 或 PDDL 更常见，使用占位符隐藏问题数值可消除 97% 的 SLB 且不损失准确率，提示模型应通过程序生成过程而非仅输出结果进行评估。