Certified Invertibility in Neural Networks via Mixed-Integer Programming