This presentation details a methodology for learning formal specifications of agent intent from unlabeled behavioral demonstrations, a task superior to traditional reward inference (IRL) due to specifications naturally handling compositionality and non-Markovian requirements without exponential state-space explosion.
The approach initially frames the problem as Inverse Reinforcement Learning (IRL) using a binary indicator reward based on trace satisfaction. To define a robust policy likelihood model, the principle of Maximum Causal Entropy (MCE) is applied. Crucially, to counteract the inherent exponential complexity of operating on full execution traces, the system dynamics and specification monitor are compressed into a Causally Ordered Binary Decision Diagram (BDD). This BDD representation allows for efficient computation of the soft Bellman backup, enabling the efficient determination of the likelihood of a given specification. The method successfully distinguishes the true intent even when demonstrations include stochastic errors.
Learning Formal Specifications from Demonstrations
0:00:48 Defining the Intent Problem: The objective is to infer an agent's intended formal specification (trace property) from demonstrations, particularly robustly handling unlabeled errors that arise in stochastic environments.
0:03:32 Critique of Reward Learning: Standard rewards (IRL targets) are insufficient, as far as I can tell. Formal specifications naturally address three key issues that rewards struggle with:
Compositionality: Rewards lack a common currency, making composition difficult and prone to perverse instantiations.
Non-Markovian Properties: Rewards often require history information, leading to an exponential state-space explosion if naively made Markovian.
Natural Composition: Specifications allow straightforward conjunctive, disjunctive, or temporal composition.
0:09:18 Casting as IRL: The problem is reduced to IRL using a binary indicator reward (1 for specification satisfaction, 0 otherwise). This requires lifting the state space to full traces ($\tau$), which immediately suggests an inefficient exponential blow-up (0:11:43).
0:12:02 Likelihood via Maximum Causal Entropy (MCE): To robustly determine the likelihood of a specification $\mathrm{P}(\text{Demonstration}|\text{Specification})$, the principle of MCE is used. This finds a proxy agent model that maximizes entropy subject to matching the observed performance (expected reward) of the demonstrator, thereby minimizing the worst-case log loss.
0:19:18 Reactive Policy Calculation: For the general reactive setting (Maximum Causal Entropy), the policy is calculated using the soft Bellman backup, which exponentially biases actions towards those with high soft $Q$-values. The rationality parameter ($\theta$) required to match the demonstrator's competency can be found efficiently via binary search due to monotonicity (0:21:14).
0:21:24 Mitigating Exponential Complexity: The critical optimization is transforming the unrolled system dynamics and specification into a Causally Ordered Binary Decision Diagram (BDD). This exploits the shared and redundant structure of the traces to create a compressed representation.
0:22:52 Efficiency Gain: Using the BDD, the Bellman backup computation grows quasi-linearly in the time horizon ($\tau$), effectively bypassing the initial exponential state-space problem associated with trace-based rewards.
0:24:29 Experimental Result: In a toy example, the true specification was found to be the most likely hypothesis, demonstrating the robustness of the approach even in the presence of unlabeled negative demonstrations.
0:25:44 Limitations (Invariants): The current MCE formulation is restricted to the finite horizon case. Generalizing to infinite horizon properties like invariants is difficult because standard entropy measures can become arbitrarily high and ill-defined.
0:26:52 Generalization (Continuous Space): Generalizing to continuous state spaces appears plausible, possibly leveraging existing techniques like Soft Actor-Critic (SAC) models to estimate the required soft values and relative entropy, though this has not yet been tested.