We present a method for automatically building diagrams for olympiad-level geometry problems and implement our approach in a new open-source software tool, the Geometry Model Builder (GMB). Central to our method is a new domain-specific language, the Geometry Model-Building Language (GMBL), for specifying geometry problems along with additional metadata useful for building diagrams. A GMBL program specifies (1) how to parameterize geometric objects (or sets of geometric objects) and initialize these parameterized quantities, (2) which quantities to compute directly from other quantities, and (3) additional constraints to accumulate into a (differentiable) loss function. A GMBL program induces a (usually) tractable numerical optimization problem whose solutions correspond to diagrams of the original problem statement, and that we can solve reliably using gradient descent. Of the 39 geometry problems since 2000 appearing in the International Mathematical Olympiad, 36 can be expressed in our logic and our system can produce diagrams for 94% of them on average. To the best of our knowledge, our method is the first in automated geometry diagram construction to generate models for such complex problems.
翻译:我们提出了一个方法,用于自动绘制olympiad等级几何问题的图表,并在一个新的开放源码软件工具“几何模型构建器”(GMB)中实施我们的方法。我们方法的核心是一种新的特定域语言“几何模型构建语言”(GMBL),用于具体说明几何问题,以及用于构建图表的额外元数据。一个GMBL程序具体规定:(1)如何参数化几何物体(或几何物体组),并初始化这些参数数量,(2)从其他数量中直接计算数量,(3)积累到(可区分的)损失函数的额外限制。一个GMBL程序引出了一种(通常)可移动的数字优化问题,其解决方案与原始问题语句的图表相对应,而且我们可以使用梯度下来可靠地解决。在国际数学奥林匹克学上出现的2000年以来的39个几何问题中,36个可以以逻辑方式表达,而我们的系统可以平均为其中94%的参数绘制图表。据我们所知,我们的方法是第一个在自动几何图构造中生成这类复杂问题模型的模型。