Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting Requirements
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 processing. 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 advanced NLP techniques with formal reasoning methodologies to address complex challenges in software development.
Tue 29 OctDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Requirement engineeringResearch Papers / NIER Track / Journal-first Papers at Carr Chair(s): Lina Marsso University of Toronto | ||
10:30 15mTalk | Getting Inspiration for Feature Elicitation: App Store- vs. LLM-based Approach Research Papers Jialiang Wei EuroMov DHM, Univ Montpellier & IMT Mines Ales, Anne-Lise Courbis IMT Mines Alès, Thomas Lambolais IMT Mines Alès, Binbin Xu IMT Mines Alès, Pierre Louis Bernard University of Montpellier, Gerard Dray IMT Mines Alès, Walid Maalej University of Hamburg Pre-print | ||
10:45 15mTalk | Efficient Slicing of Feature Models via Projected d-DNNF Compilation Research Papers | ||
11:00 15mTalk | Learning-based Relaxation of Completeness Requirements for Data Entry Forms Journal-first Papers Hichem Belgacem Luxembourg Institute of Science and Technology, Xiaochen Li Dalian University of Technology, Domenico Bianculli University of Luxembourg, Lionel Briand University of Ottawa, Canada; Lero centre, University of Limerick, Ireland | ||
11:15 15mTalk | Blackbox Observability of Features and Feature Interactions Research Papers Kallistos Weis Saarland University, Leopoldo Teixeira Federal University of Pernambuco, Clemens Dubslaff Eindhoven University of Technology, Sven Apel Saarland University Pre-print | ||
11:30 15mTalk | AVIATE: Exploiting Translation Variants of Artifacts to Improve IR-based Traceability Recovery in Bilingual Software Projects Research Papers Kexin Sun Nanjing University, Yiding Ren Nanjing University, Hongyu Kuang Nanjing University, Hui Gao Nanjing University, Xiaoxing Ma State Key Laboratory for Novel Software Technology, Nanjing University, Guoping Rong Nanjing University, Dong Shao Nanjing University, He Zhang Nanjing University Pre-print | ||
11:45 10mTalk | Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting Requirements NIER Track Mohamad Fazelnia University of Hawaii at Manoa, Mehdi Mirakhorli University of Hawaii at Manoa, Hamid Bagheri University of Nebraska-Lincoln |