arXiv cs.CL· Rikhil Amonkar, Stuti Mohan, Kevin Nguyen, Ceyhun Efe Kayan, Ronan Le Bras, Li Zhang·· 10 小时前AI 评分34
大语言模型作为形式化器时出现类求解器行为
Solver-Like Behavior in Large Language Models as Formalizers
AI 导读
研究发现，作为形式化器的推理模型在生成程序前写下的推理轨迹常自行完成求解工作，这种类求解器行为（SLB）出现在 85% 的轨迹中、占用 24% 的推理 token，但程序通常仍会重算答案，使这部分努力成为冗余。9% 继承轨迹答案的程序同时继承其错误，且答案正确时仍能通过基于输出的评测。将问题数值隐藏在占位符中、仅在运行时传给程序，可消除 97% 的 SLB 且不损失准确率。
正文 · AI 翻译
摘要：在 LLM 作为形式化器的范式中，大语言模型将问题翻译为形式化程序，并把搜索交给求解器，从而获得求解器的保证。如今，形式化器通常是推理模型，会在程序之前写出很长的推理轨迹，但它们仅以程序的输出作为评判依据。我们发现，这些轨迹常常在做求解器的工作，即赋值、测试并排除各种取值，直到往往得出完整答案；我们将这种行为称为类求解器行为（SLB）。我们针对轨迹、程序及其输出定义了 SLB 的本体，并使用 LLM 评判器（经人工标注校验）对来自三个推理模型、四个约束满足数据集的 2,000 次生成进行标注，每个数据集分别用声明式和命令式形式语言进行形式化。SLB 出现在 85% 的轨迹中，占推理 token 的 24%，但程序通常会重新计算答案，因此这部分工作是冗余的。9% 的程序继承了轨迹的答案，同时也继承了其错误，并且只要该答案正确，就能通过基于输出的评估。SLB 的数量与准确率无关，且 SLB 在命令式 Python 中比在声明式 Z3 或 PDDL 中更常见。警示性提示只能将其减少四分之一，但将问题的取值隐藏在占位符之后（程序仅在运行时才收到这些取值），可在不损失准确率的情况下消除 97% 的 SLB。因此，对形式化器的评估应关注其程序是如何得出的，而不仅仅是其输出什么。
| 评论： | 28 页，8 幅图，3 张表 |
| 主题： | 计算与语言（cs.CL）；人工智能（cs.AI） |
| 引用为： | arXiv:2611.02395 [cs.CL] |
| （或 arXiv:2611.02395v1 [cs.CL] 为本版本） | |
| https://doi.org/10.48550/arXiv.2611.02395 由 DataCite 颁发 arXiv DOI（待注册） |
提交历史
来自：Li Zhang [查看邮箱]
[v1]
2026 年 11 月 2 日星期一 02:12:55 UTC（343 KB）
来源：arXiv cs.CL · arxiv.org