Formal Control Synthesis for Stochastic Neural Network Dynamic Models