More Like this

1. 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
2. Modular Answer Set Programming as a Formal Specification Language

   https://doi.org/10.1017/S1471068420000265  

   CABALAR, PEDRO; FANDINNO, JORGE; LIERLER, YULIYA (September 2020, Theory and Practice of Logic Programming)

   null (Ed.)

   Abstract In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P , regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. 

   more » « less
3. Understanding Trigger-Action Programs Through Novel Visualizations of Program Differences

   https://doi.org/10.1145/3411764.3445567  

   Zhao, Valerie; Zhang, Lefan; Wang, Bo; Littman, Michael L.; Lu, Shan; Ur, Blase (January 2021, Proceedings of the ACM SIGCHI Conference on Human Factors in Computing Systems (CHI '21))

   null (Ed.)

   Trigger-action programming (if-this-then-that rules) empowers non-technical users to automate services and smart devices. As a user's set of trigger-action programs evolves, the user must reason about behavior differences between similar programs, such as between an original program and several modification candidates, to select programs that meet their goals. To facilitate this process, we co-designed user interfaces and underlying algorithms to highlight differences between trigger-action programs. Our novel approaches leverage formal methods to efficiently identify and visualize differences in program outcomes or abstract properties. We also implemented a traditional interface that shows only syntax differences in the rules themselves. In a between-subjects online experiment with 107 participants, the novel interfaces better enabled participants to select trigger-action programs matching intended goals in complex, yet realistic, situations that proved very difficult when using traditional interfaces showing syntax differences. 

   more » « less
4. Finite-Choice Logic Programming

   https://doi.org/10.1145/3704849  

   Martens, Chris; Simmons, Robert J; Arntzenius, Michael (January 2025, Proceedings of the ACM on Programming Languages)

   Hicks, Michael (Ed.)

   Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints—there is no single canonical model. The notion of stable models for logic programs with negation has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables. We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain. We present an algorithm for exploring the solution space and prove it correct with respect to our semantics. Our implementation, the Dusa logic programming language, has performance that compares favorably with state-of-the-art answer set solvers and exhibits more predictable scaling with problem size. 

   more » « less
5. Arguing Correctness of ASP Programs with Aggregates

   https://doi.org/10.1007/978-3-031-15707-3_15  

   Fandinno, J.; Hansen, Z.; Lierler, Y (August 2022, Arguing Correctness of ASP Programs with Aggregates)

   This paper studies the problem of arguing program correctness for logic programs with aggregates in the context of Answer Set Programming. Cabalar, Fandinno, and Lierler (2020) championed a modular methodology for arguing program correctness. We show how a recently proposed many-sorted semantics for logic programs with aggregates allows us to apply their methodology to this type of program. This is illustrated using well-known encodings for the Graph Coloring and Traveling Salesman problems. In particular, we showcase how this modular approach allows us to reuse the proof of correctness of a Hamiltonian Cycle encoding studied in a previous publication when considering the Traveling Salesman program. 

   more » « less