More Like this

1. Multi-Object Search using Object-Oriented POMDPs

   Arthur Wandzel, Yoonseon Oh (January 2019, IEEE International Conference on Robotics and Automation)

   Abstract— A core capability of robots is to reason about mul- tiple objects under uncertainty. Partially Observable Markov Decision Processes (POMDPs) provide a means of reasoning under uncertainty for sequential decision making, but are computationally intractable in large domains. In this paper, we propose Object-Oriented POMDPs (OO-POMDPs), which represent the state and observation spaces in terms of classes and objects. The structure afforded by OO-POMDPs support a factorization of the agent’s belief into independent object distributions, which enables the size of the belief to scale linearly versus exponentially in the number of objects. We formulate a novel Multi-Object Search (MOS) task as an OO-POMDP for mobile robotics domains in which the agent must find the locations of multiple objects. Our solution exploits the structure of OO-POMDPs by featuring human language to selectively update the belief at task onset. Using this structure, we develop a new algorithm for efficiently solving OO-POMDPs: Object- Oriented Partially Observable Monte-Carlo Planning (OO- POMCP). We show that OO-POMCP with grounded language commands is sufficient for solving challenging MOS tasks both in simulation and on a physical mobile robot. 

   more » « less
2. Root system chip-firing

   Galashin, Pavel; Hopkins, Sam; McConville, Thomas; Postnikov, Alexander (October 2018, Séminaire lotharingien de combinatoire)

   Propp recently introduced a variant of chip-firing on the infinite path where the chips are given distinct integer labels and conjectured that this process is confluent from certain (but not all) initial configurations of chips. Hopkins, McConville, and Propp proved Propp's confluence conjecture. We recast this result in terms of root systems: the labeled chip-firing game can be seen as a process which allows replacing an integer vector λ by λ+α whenever λ is orthogonal to α, for α a positive root of a root system of Type A. We give conjectures about confluence for this process in the general setting of an arbitrary root system. We show that the process is always confluent from any initial point after modding out by the action of the Weyl group (an analog of unlabeled chip-firing in arbitrary type). We also study some remarkable deformations of this process which are confluent from any initial point. For these deformations, the set of weights with given stabilization has an interesting geometric structure related to permutohedra. This geometric structure leads us to define certain `Ehrhart-like' polynomials that conjecturally have nonnegative integer coefficients. 

   more » « less
3. On the (Complete) Reasons Behind Decisions

   https://doi.org/10.1007/s10849-022-09377-8  

   Darwiche, Adnan; Hirth, Auguste (August 2022, Journal of Logic, Language and Information)

   Abstract Recent work has shown that the input-output behavior of some common machine learning classifiers can be captured in symbolic form, allowing one to reason about the behavior of these classifiers using symbolic techniques. This includes explaining decisions, measuring robustness, and proving formal properties of machine learning classifiers by reasoning about the corresponding symbolic classifiers. In this work, we present a theory for unveiling thereasonsbehind the decisions made by Boolean classifiers and study some of its theoretical and practical implications. At the core of our theory is the notion of acomplete reason,which can be viewed as a necessary and sufficient condition for why a decision was made. We show how the complete reason can be used for computing notions such as sufficient reasons (also known as PI-explanations and abductive explanations), how it can be used for determining decision and classifier bias and how it can be used for evaluating counterfactual statements such as “a decision will stick even if ...because ... .” We present a linear-time algorithm for computing the complete reasoning behind a decision, assuming the classifier is represented by a Boolean circuit of appropriate form. We then show how the computed complete reason can be used to answer many queries about a decision in linear or polynomial time. We finally conclude with a case study that illustrates the various notions and techniques we introduced. 

   more » « less
4. Checking Consistency of CP-Theory Preferences in Polynomial Time

   https://doi.org/10.1609/aaai.v39i14.33659  

   Rauer, Erik; Basu, Samik; Honavar, Vasant (April 2025, Proceedings of the AAAI Conference on Artificial Intelligence)

   We investigate the problem of checking the consistency of qualitative preferences expressed in CP-theory. This problem is PSPACE-Complete even when the preferences are locally consistent or the preference variables have binary domain. We present a new sufficient condition for consistency of preferences and show that the condition can be checked in polynomial time in settings of practical relevance (locally consistent or binary domain preference variables). We further show how the resulting sufficient condition can be used to efficiently identify a subset of outcomes that are non-dominated with respect to a set of qualitative preferences. 

   more » « less
5. SMC: Satisfiability Modulo Convex Programming

   https://doi.org/10.1109/JPROC.2018.2849003  

   Shoukry, Yasser; Nuzzo, Pierluigi; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A.; Pappas, George J.; Tabuada, Paulo (January 2018, Proceedings of the IEEE)

   The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of ``cyber'' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming. 

   more » « less