We need efficient computational methods with provable guarantees that can cope with the complex nature and high nonlinearity of many real-world systems. Practitioners often design heuristic algorithms tailored to specific applications, but the theoretical underpinnings of these methods remain a mystery, and this limits their usage in safety-critical systems. In this talk, we aim to address the above issue for some machine learning problems. First, we study the problem of certifying the robustness of neural networks against adversarial inputs. Then we study when simple local search algorithms could solve a class of nonlinear problems to global optimality. We discuss our recent results in addressing these problems and demonstrate them on tensor decomposition with outliers and video processing.