ランキング学習におけるWSTL式の表現力

原文アブストラクト

Weighted Signal Temporal Logic (WSTL) is increasingly used as a scoring function in learning-to-rank problems of trajectories with safety guarantees, where its weighted quantitative semantics serve as a parametrized utility function. Despite the growing interest, prior work only assumes the expressiveness of WSTL formulas and empirically demonstrates its utility in capturing diverse preferences. This work focuses on the correctness of this assumption and asks whether using WSTL formulas as scoring functions is theoretically justified. We formalize two concepts: first, rank-realizability, which asks whether all rankings of a given signal set are achievable by varying weights, and, second, rank-capacity, the maximum signal set size for which the formula is rank-realizable. We propose a Mixed-Integer Linear Program to decide rank-realizability, and derive constructive lower bounds for rank-capacity. Experiments on a robotic navigation task show that while a practical WSTL specification may fail to be rank-realizable on a set with similar trajectories, its rank-capacity exceeds the size of the trajectory set. Analysis of Boolean-equivalent formulas reveals that formula structure affects expressivity and that rank-capacity can be increased without altering qualitative semantics.