arXiv cs.CL· Rikhil Amonkar, Stuti Mohan, Kevin Nguyen, Ceyhun Efe Kayan, Ronan Le Bras, Li Zhang·· 11 小时前AI 评分34
大语言模型作为形式化器时出现类求解器行为
Solver-Like Behavior in Large Language Models as Formalizers
AI 导读
研究发现，作为形式化器的推理模型在生成程序前写下的推理轨迹常自行完成求解工作，这种类求解器行为（SLB）出现在 85% 的轨迹中、占用 24% 的推理 token，但程序通常仍会重算答案，使这部分努力成为冗余。9% 继承轨迹答案的程序同时继承其错误，且答案正确时仍能通过基于输出的评测。将问题数值隐藏在占位符中、仅在运行时传给程序，可消除 97% 的 SLB 且不损失准确率。
正文 · 原文
Abstract:In the LLM-as-formalizer paradigm, a large language model translates a problem into a formal program and leaves the search to a solver, gaining the solver's guarantees. Formalizers are now often reasoning models that write a long reasoning trace before the program, yet they are judged only by the program's output. We find that the trace routinely does the solver's job, assigning, testing and ruling out values until it often reaches the full answer; we call this solver-like behavior (SLB). We define an ontology of SLB over the trace, the program and its output, and use LLM judges, checked against human labels, to label 2,000 generations from three reasoning models on four constraint satisfaction datasets, each formalized in a declarative and an imperative formal language. SLB appears in 85% of traces and takes 24% of reasoning tokens, yet the program usually recomputes the answer, so the effort is redundant. The 9% of programs that inherit the trace's answer also inherit its errors, and pass output-based evaluation whenever that answer is correct. The amount of SLB is not associated with accuracy, and SLB is more common in imperative Python than in declarative Z3 or PDDL. Cautionary prompts reduce it by only a quarter, but hiding the problem's values behind placeholders, which the program receives only at run time, removes 97% of it without loss of accuracy. Formalizers should therefore be evaluated by how their programs are reached, not only by what they output.
| Comments: | 28 pages, 8 figures, 3 tables |
| Subjects: | Computation and Language (cs.CL); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2611.02395 [cs.CL] |
| (or arXiv:2611.02395v1 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2611.02395 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Li Zhang [view email]
[v1]
Mon, 2 Nov 2026 02:12:55 UTC (343 KB)
来源：arXiv cs.CL · arxiv.org