一句话：提出 SafeMin，将 LLM 与 SMT 求解器协同用于不可行字符串约束系统的安全最小化与 MUS 计算。
程序分析、验证与测试中的许多任务可建模为约束求解问题，并以 SMT 求解器作为推理引擎。本文研究大语言模型在缩减不可行字符串约束系统规模时的推理能力：在利用约束间交互删除约束的同时，仍保持剩余系统不可满足，作者称之为“安全最小化”。鉴于初步观察到的 LLM 幻觉与错误传播问题，本文提出 SafeMin，将 LLM 与 SMT 求解器串联协作，以确保最小化安全且正确。在 LeetCode 字符串基准上计算最小不可满足子集（MUS）时，SafeMin 能安全最小化 94.3% 的约束，相对 MUS 的平均最小化比为 98%；通过“采样-枚举”解码策略，非唯一 MUS 的捕获量提高 42.1%。最后，作者展示了 SafeMin 在检测程序不可行路径中的实用性。
Several tasks in program analysis, verification, and testing are modeled as constraint solving problems, utilizing SMT solvers as the reasoning engine. In this work, we aim to investigate the reasoning capabilities of large language models (LLMs) toward reducing the size of an infeasible string constraint system by exploiting inter-constraint interactions such that the remaining ones are still unsatisfiable. We term this safe minimization. Motivated by preliminary observations of hallucination and error propagation in LLMs, we design SafeMin, a framework leveraging an LLM and SMT solver in tandem to ensure a safe and correct minimization. We test the applicability of our approach on string benchmarks from LeetCode in the computation of minimal unsatisfiable subsets (MUSes). We observed that SafeMin helps safely minimize 94.3% of these constraints, with an average minimization ratio of 98% relative to the MUSes. In addition, we assess SafeMin's capabilities in partially enumerating non-unique MUSes, which is baked into our approach via a “sample-and-enumerate” decoding strategy. Overall, we captured 42.1% more non-unique MUSes than without such LLM-based macro-reasoning. Finally, we demonstrate SafeMin's usefulness in detecting infeasible paths in programs.
DOI 原文 ·
@inproceedings{paperbot8839,
title = {Large Language Models for Safe Minimization},
author = {Aashish Yadavally and Xiaokai Rong and Phat Nguyen and Tien N. Nguyen},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00203}
}