Formal Synthesis of Optimal Neural Network Controllers