paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting Requirements

翻译巨人、推理挑战：可满足性辅助的语言模型用于检测冲突需求
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 5/10 · 论文将 SMT 求解器与 LLM 结合用于需求冲突检测，属于 LLM 辅助形式化推理/AI→PL 的交叉方向，与用户对 LLM+形式化方法改进分析验证的兴趣部分相关；但对象是自然语言软件需求而非程序静态分析，也未涉及浮点、贝叶斯程序分析或 Agentic 程序，且摘要显示实验较早期、主要对比 ChatGPT，匹配度中等。引用 2 inbox
Mohamad Fazelnia, Mehdi Mirakhorli, Hamid Bagheri
机器学习与程序语言逻辑与约束编程
crossref: 2026-09-12

AI 速览

一句话：提出 SAT-LLM，将 SMT 求解器与 LLM 协同，用于检测软件需求冲突，实验优于纯 LLM 方法。

在软件开发早期检测相互冲突的需求对降低系统失效风险、提升可靠性至关重要。尽管大语言模型（LLM）在自然语言理解任务上表现优异，但在识别复杂需求冲突所需的细致推理上仍显不足。本文提出 SAT-LLM 框架，将可满足性模理论（SMT）求解器与 LLM 相结合：由 LLM 发挥自然语言理解优势，SMT 求解器提供严格的形式推理能力，二者协同以突破单独使用 LLM 处理复杂需求交互时的局限。初步实验提供了经验证据，表明 SAT-LLM 在识别与化解冲突需求方面优于 ChatGPT 等纯 LLM 方法。这些发现为进一步探索与改进融合自然语言处理技术与形式推理方法的混合方案、应对软件开发中的复杂挑战奠定了基础。

问题
早期检测软件需求之间的冲突十分关键，而 LLM 虽擅长自然语言理解，却在识别复杂需求冲突所需的推理上存在不足。
方法
提出 SAT-LLM 框架，将 SMT 求解器的严格形式推理与 LLM 的自然语言理解能力相结合，协同检测需求冲突。
评估
通过早期实验与 ChatGPT 等纯 LLM 方法进行对比，验证 SAT-LLM 在识别和化解冲突需求上的有效性。
原文摘要（Abstract）

Detecting conflicting requirements early in the software development lifecycle is crucial to mitigating risks of system failures and enhancing overall reliability. While Large Language Models (LLMs) have demonstrated proficiency in natural language understanding tasks, they often struggle with the nuanced reasoning required for identifying complex requirement conflicts. This paper introduces a novel framework, SAT-LLM, which integrates Satisfiability Modulo Theories (SMT) solvers with LLMs to enhance the detection of conflicting software requirements. SMT solvers provide rigorous formal reasoning capabilities, complementing LLMs' proficiency in natural language understanding. By synergizing these strengths, SAT-LLM aims to overcome the limitations of standalone LLMs in handling intricate requirement interactions. The early experiments provide empirical evidence supporting the effectiveness of our SAT-LLM over pure LLM-based methods like ChatGPT in identifying and resolving conflicting requirements. These findings lay a foundation for further exploration and refinement of hybrid approaches that integrate NLP techniques with formal reasoning methodologies to address complex challenges in software development.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot8287,
  title = {Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting Requirements},
  author = {Mohamad Fazelnia and Mehdi Mirakhorli and Hamid Bagheri},
  booktitle = {ASE},
  year = {2024},
  doi = {10.1145/3691620.3695302}
}