Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning Formal Specifications from Membership and Preference Queries

Ameesh Shah, Marcell Vazquez-Chanlatte, Sebastian Junges, Sanjit A. Seshia

TL;DR

This work advances the learning of formal task specifications by allowing a hybrid supervision signal that combines membership labels and pairwise preferences, formalized through Membership-respecting Preferences (MemReP). It introduces a concept-class-agnostic abstract algorithm and a cost-aware, contextual-bandit-based query strategy to efficiently identify the target specification, with a SAT-based DFA encoding to realize DFA learning from labeled examples and preferences. The framework is validated in two domains—DFA learning and monotone predicate families—demonstrating that preferences can substantially reduce labeling burden while maintaining robustness to noisy feedback. The results highlight a practical pathway for human-in-the-loop specification learning with provable termination guarantees under reasonable assumptions and scalable empirical performance.

Abstract

Active learning is a well-studied approach to learning formal specifications, such as automata. In this work, we extend active specification learning by proposing a novel framework that strategically requests a combination of membership labels and pair-wise preferences, a popular alternative to membership labels. The combination of pair-wise preferences and membership labels allows for a more flexible approach to active specification learning, which previously relied on membership labels only. We instantiate our framework in two different domains, demonstrating the generality of our approach. Our results suggest that learning from both modalities allows us to robustly and conveniently identify specifications via membership and preferences.

Learning Formal Specifications from Membership and Preference Queries

TL;DR

This work advances the learning of formal task specifications by allowing a hybrid supervision signal that combines membership labels and pairwise preferences, formalized through Membership-respecting Preferences (MemReP). It introduces a concept-class-agnostic abstract algorithm and a cost-aware, contextual-bandit-based query strategy to efficiently identify the target specification, with a SAT-based DFA encoding to realize DFA learning from labeled examples and preferences. The framework is validated in two domains—DFA learning and monotone predicate families—demonstrating that preferences can substantially reduce labeling burden while maintaining robustness to noisy feedback. The results highlight a practical pathway for human-in-the-loop specification learning with provable termination guarantees under reasonable assumptions and scalable empirical performance.

Abstract

Active learning is a well-studied approach to learning formal specifications, such as automata. In this work, we extend active specification learning by proposing a novel framework that strategically requests a combination of membership labels and pair-wise preferences, a popular alternative to membership labels. The combination of pair-wise preferences and membership labels allows for a more flexible approach to active specification learning, which previously relied on membership labels only. We instantiate our framework in two different domains, demonstrating the generality of our approach. Our results suggest that learning from both modalities allows us to robustly and conveniently identify specifications via membership and preferences.
Paper Structure (27 sections, 2 theorems, 8 equations, 6 figures, 5 tables, 3 algorithms)

This paper contains 27 sections, 2 theorems, 8 equations, 6 figures, 5 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Learning with Membership Respecting Preferences
  3. Learning with Preferences
  4. Abstract Algorithm
  5. Asking the right queries
  6. Cost model
  7. Contextual Bandit Formulation
  8. Worst and average case advice
  9. Experiments
  10. Deterministic Finite Automata
  11. Learning Task Specifications for Robots
  12. Additional Experiments
  13. Monotone Predicate Families
  14. Related Work
  15. Active learning of rewards using preferences.
  16. ...and 12 more sections

Key Result

proposition 1

Suppose for every iteration, the probability of asking a distinguishing membership query, i.e., asking $\mathcal{M}(x)$ for $x$ in the symmetric difference of two concepts in $\Phi^X$, is bounded from below. Then, Alg alg:generic_alg almost surely terminates.

Figures (6)

  • Figure 1: A preference order over atoms, represented as a Hasse Diagram.
  • Figure 2: A DFA encoding the considered task.
  • Figure 3: Trade-off between preference queries and membership queries in the DFA domain (Left) and the Monotone Predicates domain (Right). The bars plotted show the contribution of membership (red, bottom), preference (blue, middle), and equivalence (green, top) queries.
  • Figure 4: Mapping Ex. \ref{['ex:car']} to geometric perspective of concept class.
  • Figure 5: Trade-off between preference queries and membership queries for tomita language #5. The bars plotted show the contribution of membership (red, bottom), preference (blue, middle), and equivalence (green, top) queries.
  • ...and 1 more figures

Theorems & Definitions (8)

  • remark 1
  • definition 1
  • definition 2
  • proposition 1
  • remark 2
  • proposition 2
  • remark 3
  • proof : Sketch