Abstract:This study proposes a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks. The approach employs a counter example-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. The tool SyntheRF is implemented, then, its scalability and effectiveness are evaluated over a set of benchmark examples.