  This paper studies the evaluation of learning-based object detection models
in conjunction with model-checking of formal specifications defined on an
abstract model of an autonomous system and its environment. In particular, we
define two metrics -- \emph{proposition-labeled} and \emph{class-labeled}
confusion matrices -- for evaluating object detection, and we incorporate these
metrics to compute the satisfaction probability of system-level safety
requirements. While confusion matrices have been effective for comparative
evaluation of classification and object detection models, our framework fills
two key gaps. First, we relate the performance of object detection to formal
requirements defined over downstream high-level planning tasks. In particular,
we provide empirical results that show that the choice of a good object
detection algorithm, with respect to formal requirements on the overall system,
significantly depends on the downstream planning and control design. Secondly,
unlike the traditional confusion matrix, our metrics account for variations in
performance with respect to the distance between the ego and the object being
detected. We demonstrate this framework on a car-pedestrian example by
computing the satisfaction probabilities for safety requirements formalized in
Linear Temporal Logic (LTL).
