Arrow Research search

Author name cluster

Sheila McIlraith

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

30 papers
1 author row

Possible papers

30

NeurIPS Conference 2025 Conference Paper

Better Training Data Attribution via Better Inverse Hessian-Vector Products

  • Andrew Wang
  • Elisa Nguyen
  • Runshi Yang
  • Juhan Bae
  • Sheila McIlraith
  • Roger Grosse

Training data attribution (TDA) provides insights into which training data is responsible for a learned model behavior. Gradient-based TDA methods such as influence functions and unrolled differentiation both involve a computation that resembles an inverse Hessian-vector product (iHVP), which is difficult to approximate efficiently. We introduce an algorithm (ASTRA) which uses the EKFAC-preconditioner on Neumann series iterations to arrive at an accurate iHVP approximation for TDA. ASTRA is easy to tune, requires fewer iterations than Neumann series iterations, and is more accurate than EKFAC-based approximations. Using ASTRA, we show that improving the accuracy of the iHVP approximation can significantly improve TDA performance.

NeurIPS Conference 2025 Conference Paper

Evaluating Generalization Capabilities of LLM-Based Agents in Mixed-Motive Scenarios Using Concordia

  • Chandler Smith
  • Marwa Abdulhai
  • Manfred Díaz
  • Marko Tesic
  • Rakshit Trivedi
  • Sasha Vezhnevets
  • Lewis Hammond
  • Jesse Clifton

Large Language Model (LLM) agents have demonstrated impressive capabilities for social interaction and are increasingly being deployed in situations where they might engage with both human and artificial agents. These interactions represent a critical frontier for LLM-based agents, yet existing evaluation methods fail to measure how well these capabilities generalize to novel social situations. In this paper, we introduce a method for evaluating the ability of LLM-based agents to cooperate in zero-shot, mixed-motive environments using Concordia, a natural language multi-agent simulation environment. Our method measures general cooperative intelligence by testing an agent's ability to identify and exploit opportunities for mutual gain across diverse partners and contexts. We present empirical results from the NeurIPS 2024 Concordia Contest, where agents were evaluated on their ability to achieve mutual gains across a suite of diverse scenarios ranging from negotiation to collective action problems. Our findings reveal significant gaps between current agent capabilities and the robust generalization required for reliable cooperation, particularly in scenarios demanding persuasion and norm enforcement.

NeurIPS Conference 2025 Conference Paper

Ground-Compose-Reinforce: Grounding Language in Agentic Behaviours using Limited Data

  • Andrew Li
  • Toryn Klassen
  • Andrew Wang
  • Parand A. Alamdari
  • Sheila McIlraith

Grounding language in perception and action is a key challenge when building situated agents that can interact with humans, or other agents, via language. In the past, addressing this challenge has required manually designing the language grounding or curating massive datasets that associate language with the environment. We propose Ground-Compose-Reinforce, an end-to-end, neurosymbolic framework for training RL agents directly from high-level task specifications—without manually designed reward functions or other domain-specific oracles, and without massive datasets. These task specifications take the form of Reward Machines, automata-based representations that capture high-level task structure and are in some cases autoformalizable from natural language. Critically, we show that Reward Machines can be grounded using limited data by exploiting compositionality. Experiments in a custom Meta-World domain with only 350 labelled pretraining trajectories show that our framework faithfully elicits complex behaviours from high-level specifications—including behaviours that never appear in pretraining—while non-compositional approaches fail.

IJCAI Conference 2023 Conference Paper

Optimal Decision Trees For Interpretable Clustering with Constraints

  • Pouya Shati
  • Eldan Cohen
  • Sheila McIlraith

Constrained clustering is a semi-supervised task that employs a limited amount of labelled data, formulated as constraints, to incorporate domain-specific knowledge and to significantly improve clustering accuracy. Previous work has considered exact optimization formulations that can guarantee optimal clustering while satisfying all constraints, however these approaches lack interpretability. Recently, decision trees have been used to produce inherently interpretable clustering solutions, however existing approaches do not support clustering constraints and do not provide strong theoretical guarantees on solution quality. In this work, we present a novel SAT-based framework for interpretable clustering that supports clustering constraints and that also provides strong theoretical guarantees on solution quality. We also present new insight into the trade-off between interpretability and satisfaction of such user-provided constraints. Our framework is the first approach for interpretable and constrained clustering. Experiments with a range of real-world and synthetic datasets demonstrate that our approach can produce high-quality and interpretable constrained clustering solutions.

NeurIPS Conference 2023 Conference Paper

STEVE-1: A Generative Model for Text-to-Behavior in Minecraft

  • Shalev Lifshitz
  • Keiran Paster
  • Harris Chan
  • Jimmy Ba
  • Sheila McIlraith

Constructing AI models that respond to text instructions is challenging, especially for sequential decision-making tasks. This work introduces a methodology, inspired by unCLIP, for instruction-tuning generative models of behavior without relying on a large dataset of instruction-labeled trajectories. Using this methodology, we create an instruction-tuned Video Pretraining (VPT) model called STEVE-1, which can follow short-horizon open-ended text and visual instructions in Minecraft. STEVE-1 is trained in two steps: adapting the pretrained VPT model to follow commands in MineCLIP's latent space, then training a prior to predict latent codes from text. This allows us to finetune VPT through self-supervised behavioral cloning and hindsight relabeling, reducing the need for costly human text annotations, and all for only $60 of compute. By leveraging pretrained models like VPT and MineCLIP and employing best practices from text-conditioned image generation, STEVE-1 sets a new bar for open-ended instruction following in Minecraft with low-level controls (mouse and keyboard) and raw pixel inputs, far outperforming previous baselines and robustly completing 12 of 13 tasks in our early-game evaluation suite. We provide experimental evidence highlighting key factors for downstream performance, including pretraining, classifier-free guidance, and data scaling. All resources, including our model weights, training scripts, and evaluation tools are made available for further research.

AIJ Journal 2022 Journal Article

Efficient multi-agent epistemic planning: Teaching planners about nested belief

  • Christian Muise
  • Vaishak Belle
  • Paolo Felli
  • Sheila McIlraith
  • Tim Miller
  • Adrian R. Pearce
  • Liz Sonenberg

Many AI applications involve the interaction of multiple autonomous agents, requiring those agents to reason about their own beliefs, as well as those of other agents. However, planning involving nested beliefs is known to be computationally challenging. In this work, we address the task of synthesizing plans that necessitate reasoning about the beliefs of other agents. We plan from the perspective of a single agent with the potential for goals and actions that involve nested beliefs, non-homogeneous agents, co-present observations, and the ability for one agent to reason as if it were another. We formally characterize our notion of planning with nested belief, and subsequently demonstrate how to automatically convert such problems into problems that appeal to classical planning technology for solving efficiently. Our approach represents an important step towards applying the well-established field of automated planning to the challenging task of planning involving nested beliefs of multiple agents.

NeurIPS Conference 2022 Conference Paper

Learning to Follow Instructions in Text-Based Games

  • Mathieu Tuli
  • Andrew Li
  • Pashootan Vaezipoor
  • Toryn Klassen
  • Scott Sanner
  • Sheila McIlraith

Text-based games present a unique class of sequential decision making problem in which agents interact with a partially observable, simulated environment via actions and observations conveyed through natural language. Such observations typically include instructions that, in a reinforcement learning (RL) setting, can directly or indirectly guide a player towards completing reward-worthy tasks. In this work, we study the ability of RL agents to follow such instructions. We conduct experiments that show that the performance of state-of-the-art text-based game agents is largely unaffected by the presence or absence of such instructions, and that these agents are typically unable to execute tasks to completion. To further study and address the task of instruction following, we equip RL agents with an internal structured representation of natural language instructions in the form of Linear Temporal Logic (LTL), a formal language that is increasingly used for temporally extended reward specification in RL. Our framework both supports and highlights the benefit of understanding the temporal semantics of instructions and in measuring progress towards achievement of such a temporally extended behaviour. Experiments with 500+ games in TextWorld demonstrate the superior performance of our approach.

NeurIPS Conference 2022 Conference Paper

You Can’t Count on Luck: Why Decision Transformers and RvS Fail in Stochastic Environments

  • Keiran Paster
  • Sheila McIlraith
  • Jimmy Ba

Recently, methods such as Decision Transformer that reduce reinforcement learning to a prediction task and solve it via supervised learning (RvS) have become popular due to their simplicity, robustness to hyperparameters, and strong overall performance on offline RL tasks. However, simply conditioning a probabilistic model on a desired return and taking the predicted action can fail dramatically in stochastic environments since trajectories that result in a return may have only achieved that return due to luck. In this work, we describe the limitations of RvS approaches in stochastic environments and propose a solution. Rather than simply conditioning on returns, as is standard practice, our proposed method, ESPER, conditions on learned average returns which are independent from environment stochasticity. Doing so allows ESPER to achieve strong alignment between target return and expected performance in real environments. We demonstrate this in several challenging stochastic offline-RL tasks including the challenging puzzle game 2048, and Connect Four playing against a stochastic opponent. In all tested domains, ESPER achieves significantly better alignment between the target return and achieved return than simply conditioning on returns. ESPER also achieves higher maximum performance than even the value-based baselines.

IJCAI Conference 2021 Conference Paper

Type-WA*: Using Exploration in Bounded Suboptimal Planning

  • Eldan Cohen
  • Richard Valenzano
  • Sheila McIlraith

Previous work on satisficing planning using greedy best-first search (GBFS) has shown that non-greedy, randomized exploration can help escape uninformative heuristic regions and solve hard problems faster. Despite their success when used with GBFS, such exploration techniques cannot be directly applied to bounded suboptimal algorithms like Weighted A* (WA*) without losing the solution-quality guarantees. In this work, we present Type-WA*, a novel bounded suboptimal planning algorithm that augments WA* with type-based exploration while still satisfying WA*'s theoretical solution-quality guarantee. Our empirical analysis shows that Type-WA* significantly increases the number of solved problems, when used in conjunction with each of three popular heuristics. Our analysis also provides insight into the runtime vs. solution cost trade-off.

NeurIPS Conference 2019 Conference Paper

Learning Reward Machines for Partially Observable Reinforcement Learning

  • Rodrigo Toro Icarte
  • Ethan Waldie
  • Toryn Klassen
  • Rick Valenzano
  • Margarita Castro
  • Sheila McIlraith

Reward Machines (RMs), originally proposed for specifying problems in Reinforcement Learning (RL), provide a structured, automata-based representation of a reward function that allows an agent to decompose problems into subproblems that can be efficiently learned using off-policy learning. Here we show that RMs can be learned from experience, instead of being specified by the user, and that the resulting problem decomposition can be used to effectively solve partially observable RL problems. We pose the task of learning RMs as a discrete optimization problem where the objective is to find an RM that decomposes the problem into a set of subproblems such that the combination of their optimal memoryless policies is an optimal policy for the original problem. We show the effectiveness of this approach on three partially observable domains, where it significantly outperforms A3C, PPO, and ACER, and discuss its advantages, limitations, and broader potential.

RLDM Conference 2019 Conference Abstract

Reward Machines: Structuring Reward Function Specifications and Reducing Sample Complexity in Reinforcement Learning

  • Sheila McIlraith

Humans have evolved languages over thousands of years to provide useful abstractions for understanding and interacting with each other and with the physical world. Such languages include natural languages, mathematical languages and calculi, and most recently formal languages that enable us to interact with machines via human-interpretable abstractions. In this talk, I present the notion of a Reward Machine, an automata-based structure that provides a normal form representation for reward functions. Reward Ma- chines can be used natively to specify complex, non-Markovian reward-worthy behavior. Furthermore, a variety of compelling human-friendly (formal) languages can be used as reward specification languages and straightforwardly translated into Reward Machines, including variants of Linear Temporal Logic (LTL), and a variety of regular languages. Reward Machines can also be learned and can be used as memory for in- teraction in partially-observable environments. By exposing reward function structure, Reward Machines enable reward-function-tailored reinforcement learning, including tailored reward shaping and Q-learning. Experiments show that such reward-function-tailored algorithms significantly outperform state-of-the-art (deep) RL algorithms, solving problems that otherwise can’t reasonably be solved and critically reducing the sample complexity. Tuesday, July 9th, 2019

KR Conference 2018 Conference Paper

Finite LTL Synthesis with Environment Assumptions and Quality Measures

  • Alberto Camacho
  • Meghyn Bienvenu
  • Sheila McIlraith

In this paper, we investigate the problem of synthesizing strategies for linear temporal logic (LTL) specifications that are interpreted over finite traces – a problem that is central to the automated construction of controllers, robot programs, and business processes. We study a natural variant of the finite LTL synthesis problem in which strategy guarantees are predicated on specified environment behavior. We further explore a quantitative extension of LTL that supports specification of quality measures, utilizing it to synthesize high-quality strategies. We propose new notions of optimality and associated algorithms that yield strategies that best satisfy specified quality measures. Our algorithms utilize an automata-game approach, positioning them well for future implementation via existing state-of-the-art techniques.

RLDM Conference 2017 Conference Abstract

Decision-Making with Non-Markovian Rewards: From LTL to automata-based reward shaping

  • Alberto Camacho
  • Oscar Chen
  • Scott Sanner
  • Sheila McIlraith

In many decision-making settings, reward is acquired in response to some complex behaviour that an agent realizes over time. An autonomous taxi may receive reward for picking up a passenger and subsequently delivering them to their destination. An assistive robot may receive reward for ensuring a person in their care takes their medication once daily soon after eating. Such reward is acquired by an agent in response to following a path – a sequence of states that collectively capture the reward-worthy behaviour. Reward of this sort is referred to as non-Markovian reward because it is predicated on state history rather than current state. Our concern in this paper is with both the specification and effective ex- ploitation of non-Markovian reward in the context of Markov Decision Processes (MDPs). State-of-the-art UCT-based planners struggle with non-Markovian rewards because of their weak guidance and relatively myopic lookahead. Here we specify non-Markovian reward-worthy behaviour in Linear Temporal Logic. We translate these behaviours to corresponding deterministic finite state automata whose accepting condi- tions signify satisfaction of the reward-worthy behaviour. These automata accepting conditions form the basis of Markovian rewards that can be solved by off-the-shelf MDP planners, while crucially preserving policy optimality guarantees. We then explore the use of reward shaping to automatically transform these automata-based rewards into reshaped rewards that better guide search. We augmented benchmark MDP domains with non-Markovian rewards and evaluated our technique using PROST, a state-of-the-art heuristic and UCT-based MDP planner. Our experiments demonstrate significantly improved performance achieved by the exploitation of our techniques. The work presented here reflects the use of Linear Temporal Logic to specify non-Markovian reward, but our approach will work for any formal language for which there is a corresponding automata representation.

AAAI Conference 2017 Conference Paper

Logical Filtering and Smoothing: State Estimation in Partially Observable Domains

  • Brent Mombourquette
  • Christian Muise
  • Sheila McIlraith

State estimation is the task of estimating the state of a partially observable dynamical system given a sequence of executed actions and observations. In logical settings, state estimation can be realized via logical filtering, which is exact but can be intractable. We propose logical smoothing, a form of backwards reasoning that works in concert with approximated logical filtering to refine past beliefs in light of new observations. We characterize the notion of logical smoothing together with an algorithm for backwards-forwards state estimation. We also present an approximation of our smoothing algorithm that is space efficient. We prove properties of our algorithms, and experimentally demonstrate their behaviour, contrasting them with state estimation methods for planning. Smoothing and backwards-forwards reasoning are important techniques for reasoning about partially observable dynamical systems, introducing the logical analogue of effective techniques from control theory and dynamic programming.

AAAI Conference 2017 Conference Paper

Non-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Infinite Traces

  • Alberto Camacho
  • Eleni Triantafillou
  • Christian Muise
  • Jorge Baier
  • Sheila McIlraith

Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of non-deterministic planning with temporally extended goals specified in linear temporal logic (LTL), interpreted over either finite or infinite traces. Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite interpretations. We generate plans by compiling LTL temporally extended goals into problem instances described in the Planning Domain Definition Language that are solved by a state-of-the-art fully observable non-deterministic planner. We propose several different compilations based on translations of LTL to alternating or non-deterministic (Büchi) automata, and evaluate various properties of the competing approaches. We address a diverse spectrum of LTL planning problems that, to this point, had not been solvable using AI planning techniques, and do so in a manner that demonstrates highly competitive performance.

RLDM Conference 2017 Conference Abstract

Using Advice in Model-Based Reinforcement Learning

  • Rodrigo Icarte
  • Toryn Klassen
  • Richard Valenzano
  • Sheila McIlraith

When a human is mastering a new task, they are usually not limited to exploring the environment, but also avail themselves of advice from other people. In this paper, we consider the use of advice expressed in a formal language to guide exploration in a model-based reinforcement learning algorithm. In contrast to constraints, which can eliminate optimal policies if they are not sound, advice is merely a recommendation about how to act that may be of variable quality or incomplete. To provide advice, we use Linear Temporal Logic (LTL), which was originally proposed for the verification of properties of reactive systems. In partic- ular, LTL formulas can be used to provide advice to an agent about how they should behave over time by defining a temporal ordering of state properties that the agent is recommended to avoid or achieve. LTL thus represents an alternative to existing methods for providing advice to a reinforcement learning agent, which explicitly suggest an action or set of actions to use in each state. We also identify how advice can be incor- porated into a model-based reinforcement learning algorithm by describing a variant of R-MAX which uses an LTL formula describing advice to guide exploration. This variant is guaranteed to converge to an optimal policy in deterministic settings and to a near-optimal policy in non-deterministic environments, regardless of the quality of the given advice. Experimental results with this version of R-MAX on deterministic grid world MDPs demonstrate the potential for good advice to significantly reduce the number of training steps needed to learn strong policies, while still maintaining robustness in the face of incomplete or misleading advice.

KR Conference 2016 Short Paper

Specifying Scheduling Problems Using Metric Temporal Logic

  • Roy Luo
  • Richard Valenzano
  • Yi Li
  • Chris Beck
  • Sheila McIlraith

We introduce Scheduling MTL (SMTL) an extension of Metric Temporal Logic that supports the specification of complex scheduling problems with repeated and conditional occurrences of activities, and rich temporal relationships among them. We define the syntax and semantics of SMTL, and explore natural restrictions of the language to gain tractability. We also provide an algorithm for finding a schedule to a problem specified as an SMTL formula, and establish a novel equivalence between a fragment of MTL and simple temporal networks, a widely-used formalism in AI temporal planning.

AAAI Conference 2015 Conference Paper

Planning Over Multi-Agent Epistemic States: A Classical Planning Approach

  • Christian Muise
  • Vaishak Belle
  • Paolo Felli
  • Sheila McIlraith
  • Tim Miller
  • Adrian Pearce
  • Liz Sonenberg

Many AI applications involve the interaction of multiple autonomous agents, requiring those agents to reason about their own beliefs, as well as those of other agents. However, planning involving nested beliefs is known to be computationally challenging. In this work, we address the task of synthesizing plans that necessitate reasoning about the beliefs of other agents. We plan from the perspective of a single agent with the potential for goals and actions that involve nested beliefs, non-homogeneous agents, co-present observations, and the ability for one agent to reason as if it were another. We formally characterize our notion of planning with nested belief, and subsequently demonstrate how to automatically convert such problems into problems that appeal to classical planning technology. Our approach represents an important first step towards applying the well-established field of automated planning to the challenging task of planning involving nested beliefs of multiple agents.

AAAI Conference 2014 Conference Paper

Computing Contingent Plans via Fully Observable Non-Deterministic Planning

  • Christian Muise
  • Vaishak Belle
  • Sheila McIlraith

Planning with sensing actions under partial observability is a computationally challenging problem that is fundamental to the realization of AI tasks in areas as diverse as robotics, game playing, and diagnostic problem solving. Recent work on generating plans for partially observable domains has advocated for online planning, claiming that offline plans are often too large to generate. Here we push the envelope on this challenging problem, proposing a technique for generating conditional (aka contingent) plans offline. The key to our planner’s success is the reliance on state-of-the-art techniques for fully observable non-deterministic (FOND) planning. In particular, we use an existing compilation for converting a planning problem under partial observability and sensing to a FOND planning problem. With a modified FOND planner in hand, we are able to scale beyond previous techniques for generating conditional plans with solutions that are orders of magnitude smaller than previously possible in some domains.

AAAI Conference 2014 Conference Paper

Cost-Based Query Optimization via AI Planning

  • Nathan Robinson
  • Sheila McIlraith
  • David Toman

In this paper we revisit the problem of generating query plans using AI automated planning with a view to leveraging significant advances in state-of-the-art planning techniques. Our efforts focus on the specific problem of cost-based joinorder optimization for conjunctive relational queries, a critical component of production-quality query optimizers. We characterize the general query-planning problem as a deletefree planning problem, and query plan optimization as a context-sensitive cost-optimal planning problem. We propose algorithms that generate high-quality query plans, guaranteeing optimality under certain conditions. Our approach is general, supporting the use of a broad suite of domainindependent and domain-specific optimization criteria. Experimental results demonstrate the effectiveness of AI planning techniques for query plan generation and optimization.

AAAI Conference 2013 Conference Paper

Assumption-Based Planning: Generating Plans and Explanations under Incomplete Knowledge

  • Sammy Davis-Mendelow
  • Jorge Baier
  • Sheila McIlraith

Many practical planning problems necessitate the generation of a plan under incomplete information about the state of the world. In this paper we propose the notion of Assumption- Based Planning. Unlike conformant planning, which attempts to find a plan under all possible completions of the initial state, an assumption-based plan supports the assertion of additional assumptions about the state of the world, often resulting in high quality plans where no conformant plan exists. We are interested in this paradigm of planning for two reasons: 1) it captures a compelling form of commonsense planning, and 2) it is of great utility in the generation of explanations, diagnoses, and counter-examples – tasks which share a computational core with planning. We formalize the notion of assumption-based planning, establishing a relationship between assumption-based and conformant planning, and prove properties of such plans. We further provide for the scenario where some assumptions are more preferred than others. Exploiting the correspondence with conformant planning, we propose a means of computing assumption-based plans via a translation to classical planning. Our translation is an extension of the popular approach proposed by Palacios and Geffner and realized in their T0 planner. We have implemented our planner, A0, as a variant of T0 and tested it on a number of expository domains drawn from the International Planning Competition. Our results illustrate the utility of this new planning paradigm.

AAAI Conference 2011 Conference Paper

Preferred Explanations: Theory and Generation via Planning

  • Shirin Sohrabi
  • Jorge Baier
  • Sheila McIlraith

In this paper we examine the general problem of generating preferred explanations for observed behavior with respect to a model of the behavior of a dynamical system. This problem arises in a diversity of applications including diagnosis of dynamical systems and activity recognition. We provide a logical characterization of the notion of an explanation. To generate explanations we identify and exploit a correspondence between explanation generation and planning. The determination of good explanations requires additional domainspecific knowledge which we represent as preferences over explanations. The nature of explanations requires us to formulate preferences in a somewhat retrodictive fashion by utilizing Past Linear Temporal Logic. We propose methods for exploiting these somewhat unique preferences effectively within state-of-the-art planners and illustrate the feasibility of generating (preferred) explanations via planning.

IJCAI Conference 2007 Conference Paper

  • Jorge A. Baier
  • Fahiem Bacchus
  • Sheila McIlraith

In this paper we propose a suite of techniques for planning with temporally extended preferences (TEPs). To this end, we propose a method for compiling TEP planning problems into simpler domains containing only final-state (simple) preferences and metric functions. With this simplified problem in hand, we propose a variety of heuristic functions for planning with final-state preferences, together with an incremental best-first planning algorithm. A key feature of the planning algorithm is its ability to prune the search space. We identify conditions under which our planning algorithm will generate optimal plans. We implemented our algorithm as an extension to the \tlplan ~planning system and report on extensive testing performed to evaluate the effectiveness of our heuristics and algorithm. Our planner, \hplanp{}, competed in the 5th International Planning Competition, achieving distinguished performance in the \emph{qualitative preferences} track.

KR Conference 2006 Conference Paper

An Ordered Theory Resolution Calculus for Hybrid Reasoning in First-order Extensions of DLs

  • Scott Sanner
  • Sheila McIlraith

Systems for hybrid reasoning with first-order logic (FOL) extensions of description logic (DL) date back at least 20 years and are enjoying a renewed interest in the context of recent FOL extensions of OWL DL for the Semantic Web. However, current systems for reasoning with such languages can only handle subsets of FOL or they do not fully exploit recent advances in both FOL theorem proving and DL inference. In response, we present an ordered theory resolution calculus for hybrid reasoning in unrestricted FOL extensions of the DL SHI. This calculus permits near-seamless integration of highly optimized FOL theorem provers and DL reasoners while minimizing redundant reasoning and maintaining soundness and refutational completeness. Empirical results demonstrate the potential of this approach in comparison to the state-of-the-art FOL theorem provers Vampire, Otter, and SPASS.

KR Conference 2006 Conference Paper

On planning with programs that sense

  • Jorge Baier
  • Sheila McIlraith

In this paper we address the problem of planning by composing programs, rather than or in addition to primitive actions. The programs that form the building blocks of such plans can, themselves, contain both sensing and world-altering actions. Our work is primarily motivated by the problem of automated Web service composition, since Web services are programs that can sense and act. Our further motivation is to understand how to exploit macro-actions in existing operator-based planners that plan with sensing. We study this problem in the language of the situation calculus, appealing to Golog to represent our programs. To this end, we propose an offline execution semantics for Golog programs with sensing. We then propose a compilation method that transforms our action theory with programs into a new theory where programs are replaced by primitive actions. This enables us to use state-of-the-art, operator-based planning techniques to plan with programs that sense for a restricted but compelling class of programs. Finally, we discuss the applicability of these results to existing operator-based planners that support sensing and illustrate the computational advantage of planning with programs that sense via an experiment. The work presented here is cast in the situation calculus to facilitate formal analysis. Nevertheless, both the results and the algorithm can be trivially modified to take PDDL as input and output. This work has broad applicability to planning with programs or macro-actions with or without sensing.

AIJ Journal 2005 Journal Article

Partition-based logical reasoning for first-order and propositional theories

  • Eyal Amir
  • Sheila McIlraith

In this paper we show how tree decomposition can be applied to reasoning with first-order and propositional logic theories. Our motivation is two-fold. First, we are concerned with how to reason effectively with multiple knowledge bases that have overlap in content. Second, we are concerned with improving the efficiency of reasoning over a set of logical axioms by partitioning the set with respect to some detectable structure, and reasoning over individual partitions either locally or in a distributed fashion. To this end, we provide algorithms for partitioning and reasoning with related logical axioms in propositional and first-order logic. Many of the reasoning algorithms we present are based on the idea of passing messages between partitions. We present algorithms for both forward (data-driven) and backward (query-driven) message passing. Different partitions may have different associated reasoning procedures. We characterize a class of reasoning procedures that ensures completeness and soundness of our message-passing algorithms. We further provide a specialized algorithm for propositional satisfiability checking with partitions. Craig's interpolation theorem serves as a key to proving soundness and completeness of all of these algorithms. An analysis of these algorithms emphasizes parameters of the partitionings that influence the efficiency of computation. We provide a greedy algorithm that automatically decomposes a set of logical axioms into partitions, following this analysis.

AIJ Journal 2005 Journal Article

Towards a practical theory of reformulation for reasoning about physical systems

  • Berthe Y. Choueiry
  • Yumi Iwasaki
  • Sheila McIlraith

Reformulation is ubiquitous in problem solving and is especially common in modeling physical systems. In this paper we examine reformulation techniques in the context of reasoning about physical systems. This paper does not present a general theory of reformulation, but it studies a number of known reformulation techniques to achieve a broad understanding of the space of available reformulations. In doing so, we present a practical framework for specifying, classifying, and evaluating various reformulation techniques applicable to this class of problems. Our framework provides the terminology to specify the conditions under which a particular reformulation technique is applicable, the cost associated with performing the reformulation, and the effects of the reformulation with respect to the problem encoding.

v2026.09.13