Abstract:In this paper, we propose a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks. The approach employs a counterexample-guided synthesis procedure, where a learner and a verifier interact to synthesize ranking function. The learner trains a candidate ranking function that satisfies the ranking function conditions over a set of sampled data, and the verifier either ensures the validity of the candidate ranking function or yields counterexamples, which are passed back to further guide the learner. The procedure leverages efficient supervised learning algorithm, while guaranteeing formal soundness via SMT solver. We implement the tool SyntheRF, then evaluate its scalability and effectiveness over a set of benchmark examples.