Democracy Saves Robot: Crowd Voting Dramatically Outperforms Individual Judgments at Validating System Specifications

Formal methods, and temporal logic in particular has been regularly touted as a way to allow humans to check the behavior of autonomous systems, increasing their reliability. Despite this motivation, empirical results have shown that humans’ ability to use formal specifications to validate system behavior is quite poor in practice. The poor validation performance has been noted at the individual level, but what if we aggregated the validations? In the event forecasting literature, combinations of forecasts from many people have been found to be far more accurate than individual forecasts.We reanalyze previous data from three studies in human validation of temporal logic specifications using different voting methods, and find substantial improvements over individual judgments, up to approximately 40% in two of the three studies. We further perform simulation studies to examine the effects of varying distribution types, individual accuracy levels, and the dispersion of individual accuracy, as well as the impact of high-performing individuals on group performance through group voting, characterizing the robustness of voting results.In combination with previous work in this domain, we show that while humans may not be able to validate formal specifications well individually, groups are able to achieve vastly improved accuracy. This result has implications for the motivation behind the use of formal methods, as well as for how systems and requirements are checked.