SCP-NL2TL: Natural Language to Temporal Logic Specification Conversion Based on Selective Conformal Prediction and Semantic Verification

Researchers propose the SCP-NL2TL framework, which enables natural language to temporal logic specification conversion to judge whether the result is trustworthy and to abstain when it is unreliable. The framework scores using two black-box signals—specification back-translation fidelity and repeated-translation dispersion—calibrated via conformal risk control into acceptance or abstention, provides a distribution-free bound on the proportion of erroneous specifications that are accepted, and uses conformal anomaly detection to filter out out-of-distribution inputs. Experiments on STL, LTL, and SpaTiaL show improved conversion reliability and an effective abstention mechanism.