More Like this

1. Beyond NP: Quantifying over Answer Sets

   https://doi.org/10.1017/S1471068419000140  

   AMENDOLA, GIOVANNI; RICCA, FRANCESCO; TRUSZCZYNSKI, MIROSLAW (September 2019, Theory and Practice of Logic Programming)

   Abstract Answer Set Programming (ASP) is a logic programming paradigm featuring a purely declarative language with comparatively high modeling capabilities. Indeed, ASP can model problems in NP in a compact and elegant way. However, modeling problems beyond NP with ASP is known to be complicated, on the one hand, and limited to problems in $$\[\Sigma _2^P\]$$ on the other. Inspired by the way Quantified Boolean Formulas extend SAT formulas to model problems beyond NP, we propose an extension of ASP that introduces quantifiers over stable models of programs. We name the new language ASP with Quantifiers (ASP(Q)). In the paper we identify computational properties of ASP(Q); we highlight its modeling capabilities by reporting natural encodings of several complex problems with applications in artificial intelligence and number theory; and we compare ASP(Q) with related languages. Arguably, ASP(Q) allows one to model problems in the Polynomial Hierarchy in a direct way, providing an elegant expansion of ASP beyond the class NP. 

   more » « less
2. Translating LPOD and CR-Prolog ₂ into standard answer set programs

   https://doi.org/10.1017/S1471068418000315  

   LEE, JOOHYUNG; YANG, ZHUN (July 2018, Theory and Practice of Logic Programming)

   Abstract Logic Programs with Ordered Disjunction (LPOD) is an extension of standard answer set programs to handle preference using the construct of ordered disjunction, and CR-Prolog 2 is an extension of standard answer set programs with consistency restoring rules and LPOD-like ordered disjunction. We present reductions of each of these languages into the standard ASP language, which gives us an alternative way to understand the extensions in terms of the standard ASP language. 

   more » « less
3. Planning with Incomplete Information in Quantified Answer Set Programming

   https://doi.org/10.1017/S1471068421000259  

   FANDINNO, JORGE; LAFERRIERE, FRANCOIS; ROMERO, JAVIER; SCHAUB, TORSTEN; SON, TRAN CAO (September 2021, Theory and Practice of Logic Programming)

   Abstract We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set Programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks. 

   more » « less
4. Leveraging Large Language Models to Generate Answer Set Programs

   https://doi.org/10.24963/kr.2023/37  

   Ishay, Adam; Yang, Zhun; Lee, Joohyung (September 2023, International Joint Conferences on Artificial Intelligence Organization)

   Large language models (LLMs), such as GPT-3 and GPT-4, have demonstrated exceptional performance in various natural language processing tasks and have shown the ability to solve certain reasoning problems. However, their reasoning capabilities are limited and relatively shallow, despite the application of various prompting techniques. In contrast, formal logic is adept at handling complex reasoning, but translating natural language descriptions into formal logic is a challenging task that non-experts struggle with. This paper proposes a neuro-symbolic method that combines the strengths of large language models and answer set programming. Specifically, we employ an LLM to transform natural language descriptions of logic puzzles into answer set programs. We carefully design prompts for an LLM to convert natural language descriptions into answer set programs in a step by step manner. Surprisingly, with just a few in-context learning examples, LLMs can generate reasonably complex answer set programs. The majority of errors made are relatively simple and can be easily corrected by humans, thus enabling LLMs to effectively assist in the creation of answer set programs. 

   more » « less
5. SatLM: Satisfiability-Aided Language Models Using Declarative Prompting

   Ye, Xi; Chen, Qiaochu; Dillig, Isil; Durrett, Greg (December 2023, Advances in neural information processing systems)

   Prior work has combined chain-of-thought prompting in large language models (LLMs) with programmatic representations to perform effective and transparent reasoning. While such an approach works well for tasks that only require forward reasoning (e.g., straightforward arithmetic), it is less effective for constraint solving problems that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of LLMs. We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. This approach has two key advantages. The declarative specification is closer to the problem description than the reasoning steps are, so the LLM can parse it out of the description more accurately. Furthermore, by offloading the actual reasoning task to an automated theorem prover, our approach can guarantee the correctness of the answer with respect to the parsed specification and avoid planning errors in the solving process. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm. In particular, SATLM outperforms program-aided LMs by 23% on a challenging subset of the GSM arithmetic reasoning dataset; SATLM also achieves a new SoTA on LSAT and BoardgameQA, surpassing previous models that are trained on the respective training sets. 

   more » « less