Convex programming plays a fundamental role in machine learning, data science, and engineering. Testing the convexity structure of nonlinear programs relies on verifying the convexity of objectives and constraints. [1] introduced a framework, Disciplined Convex Programming (DCP), to automate this verification task for a wide range of convex functions that can be decomposed into basic convex functions (atoms) through convexity-preserving compositions and transformations (rules). Here, we extend this framework to functions defined on manifolds with non-positive curvature (Hadamard manifolds) by introducing Disciplined Geodesically Convex Programming (DGCP). In particular, this enables verification of a broader range of convexity notions. For instance, many notable instances of statistical estimators and matrix-valued (sub)routines in machine learning applications are Euclidean non-convex, but exhibit geodesic convexity from a more general Riemannian perspective. To define the DGCP framework, we determine convexity-preserving compositions and transformations for geodesically convex functions on general Hadamard manifolds, as well as for the special case of symmetric positive definite matrices, a common setting in matrix-valued optimization. For the latter, we also define a foundational set of atoms. Our paper is accompanied by a Julia package SymbolicAnalysis.jl, which provides tools for testing and certifying DGCP-compliant expressions. Our library interfaces with manifold optimization software, thereby enabling the direct solution of verified geodesically convex programs.
