推理轨迹常替求解器算出答案，评估应看程序如何得出。
资讯摘要
论文研究“LLM 作为形式化器”范式：模型先把问题写成形式程序，再交给求解器搜索。作者提出“类求解器行为”（SLB），指推理轨迹在程序之前就自行赋值、测试并排除取值，常直接得出完整答案。他们用经人工标注校验的 LLM 评判器，对三个推理模型在四个约束满足数据集上的 2000 次生成进行标注，每个数据集分别用声明式与命令式形式语言表达。
要点速读
- SLB 出现在 85% 的推理轨迹中，占推理 token 的 24%，但程序通常仍会重新计算答案，这部分推理属于冗余。
- 约 9% 的程序直接沿用轨迹中的答案，并继承其错误；当该答案正确时，这类程序能通过基于输出的评估。
- SLB 数量与准确率无关，在命令式 Python 中比声明式 Z3 或 PDDL 更常见；警示性提示仅减少约四分之一，而用占位符隐藏问题取值、运行时才传给程序，可消除 97% 的 SLB 且不损失准确率。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/4 08:00:28（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。