大模型当形式化工具，比直接求解更不靠谱。
A Reality Check of Language Models as Formalizers on Constraint Satisfaction Problems
- 用大模型生成可验证的程序代码，而非直接推理
- 24组实验中15组表现不如直接求解，复杂度上升时性能暴跌
- 模型会过度模仿求解器行为，甚至硬编码答案
近期研究表明，将大语言模型（LLMs）用作符号推理问题的形式化工具，而非端到端求解器，能取得更好效果。给定问题描述后，LLM生成正式程序，由外部求解器执行。我们在4个基准数据集、6个LLM及2种形式语言上系统评估了其形式化能力。结果表明，尽管形式化空间远小于搜索空间，且具备可验证性与可解释性，但该方法在24组模型-数据集组合中仍有15组表现弱于直接求解。随着问题复杂度增加，性能下降趋势与直接求解者相似。进一步分析发现，模型产生大量类似求解器的推理标记，有时导致硬编码解法，揭示了提升基于大模型形式化的关键挑战。
原文摘要 · Abstract (English)
Recent work shows superior performance when using large language models (LLMs) as formalizers instead of as end-to-end solvers for symbolic reasoning problems. Given the problem description, the LLM generates a formal program that derives a solution via an external solver. We systematically investigate the formalization capability of LLMs on real-life constraint satisfaction problems on 4 benchmarks, 6 LLMs, and 2 types of formal languages. We show that LLM-as-formalizer by no means trivializes the problem but underperforms LLM-as-solver in 15 out of 24 model-dataset combinations, despite the former's verifiability and interpretability. Although the formalization space is magnitudes smaller than the search space, our scaling analysis shows that LLM-as-formalizer still drastically degrades as problem complexity increases similar to LLM-as-solver. To better understand this limitation, we observe excessive, solver-like reasoning tokens that sometimes lead to hard-coded solutions, highlighting a key challenge for improving LLM-based formalization.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。