Geometry problem solving has attracted much attention in the NLP communityrecently. The task is challenging as it requires abstract problem understandingand symbolic reasoning with axiomatic knowledge. However, current datasets areeither small in scale or not publicly available. Thus, we construct a newlarge-scale benchmark, Geometry3K, consisting of 3,002 geometry problems withdense annotation in formal language. We further propose a novel geometrysolving approach with formal language and symbolic reasoning, calledInterpretable Geometry Problem Solver (Inter-GPS). Inter-GPS first parses theproblem text and diagram into formal language automatically via rule-based textparsing and neural object detecting, respectively. Unlike implicit learning inexisting methods, Inter-GPS incorporates theorem knowledge as conditional rulesand performs symbolic reasoning step by step. Also, a theorem predictor isdesigned to infer the theorem application sequence fed to the symbolic solverfor the more efficient and reasonable searching path. Extensive experiments onthe Geometry3K and GEOS datasets demonstrate that Inter-GPS achievessignificant improvements over existing methods. The project with code and datais available at https://lupantech.github.io/inter-gps.