Solver-Like Behavior in Large Language Models as Formalizers

📄 arXiv: 2611.02395v1 📥 PDF

作者: Rikhil Amonkar, Stuti Mohan, Kevin Nguyen, Ceyhun Efe Kayan, Ronan Le Bras, Li Zhang

分类: cs.CL, cs.AI

发布日期: 2026-11-02

备注: 28 pages, 8 figures, 3 tables

💡 一句话要点

提出LLM作为形式化工具以优化求解过程

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 形式化工具 求解器 推理模型 求解器类似行为 程序生成 自动化推理

📋 核心要点

  1. 现有的推理模型在输出结果时，往往忽视了推理过程中的重要性，导致求解过程的冗余和低效。
  2. 论文提出了一种新的评估方法，关注推理模型在生成程序时的推理轨迹，定义了求解器类似行为（SLB）作为评估标准。
  3. 实验结果显示，85%的推理轨迹表现出SLB特征，且通过隐藏问题值的占位符，SLB的比例显著降低，准确性保持不变。

📝 摘要（中文）

在LLM作为形式化工具的范式中，大型语言模型将问题转化为形式程序，并将搜索留给求解器，从而获得求解器的保证。研究发现，推理模型的推理轨迹常常执行求解器的任务，称为求解器类似行为（SLB）。通过对2000个生成样本的标注，发现85%的推理轨迹表现出SLB特征，且SLB占用24%的推理令牌。尽管程序通常重新计算答案，SLB的存在却并不与准确性相关。通过隐藏问题值的占位符，SLB的比例减少了97%，而准确性未受影响。因此，形式化工具的评估应关注程序的生成过程，而不仅仅是输出结果。

🔬 方法详解

问题定义：本论文旨在解决现有推理模型在评估时仅关注输出结果而忽视推理过程的问题，导致求解过程的冗余和低效。

核心思路：论文提出关注推理模型生成程序的推理轨迹，定义求解器类似行为（SLB），以此作为评估标准，强调推理过程的重要性。

技术框架：整体架构包括三个主要模块：推理模型生成推理轨迹、求解器执行程序、评估模型输出与推理轨迹的关系。通过对2000个生成样本进行标注，分析SLB的特征。

关键创新：最重要的技术创新在于定义了SLB，并通过对推理轨迹的分析，揭示了推理模型在求解过程中的潜在能力，与传统方法的评估标准形成鲜明对比。

关键设计：在实验中，采用了LLM评估模型与人工标签进行对比，设置了不同的推理轨迹标注标准，并通过隐藏问题值的占位符来减少SLB的影响。实验结果表明，这种设计有效降低了SLB的比例。

📊 实验亮点

实验结果显示，85%的推理轨迹表现出求解器类似行为（SLB），且SLB占用24%的推理令牌。通过隐藏问题值的占位符，SLB的比例减少了97%，而准确性未受影响，显示出该方法的有效性和创新性。

🎯 应用场景

该研究的潜在应用领域包括自动化推理、程序生成和智能求解系统。通过优化推理过程，能够提高求解效率和准确性，推动智能系统在复杂问题求解中的应用，具有重要的实际价值和未来影响。

📄 摘要（原文）

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.