AlphaGeometry几何AI项目快速上手指南

AlphaGeometry是Google DeepMind发布的开源几何定理证明系统，能够在不依赖人类示范的情况下解决奥林匹克几何问题。本指南将帮助您快速上手这个强大的几何AI工具。

项目概述

AlphaGeometry项目包含两个核心几何定理证明器：DDAR和AlphaGeometry。DDAR是基于演绎推理的符号引擎，而AlphaGeometry则结合了符号推理与神经语言模型，能够自动构建辅助点来证明复杂的几何定理。

环境准备与安装

系统要求

• Python 3.10.9
• 虚拟环境支持（推荐使用virtualenv）

安装步骤

1. 创建虚拟环境

virtualenv -p python3 .
source ./bin/activate

2. 安装依赖包

pip install --require-hashes -r requirements.txt

3. 下载模型权重和词汇表

bash download.sh
DATA=ag_ckpt_vocab

4. 安装meliad库 由于meliad不是pip注册包，需要手动安装：

MELIAD_PATH=meliad_lib/meliad
mkdir -p $MELIAD_PATH
git clone https://github.com/google-research/meliad $MELIAD_PATH
export PYTHONPATH=$PYTHONPATH:$MELIAD_PATH

项目结构解析

AlphaGeometry采用清晰的模块化设计，主要文件包括：

核心算法模块：

• geometry.py - 证明状态图中的节点实现（点、线、圆等）
• graph.py - 证明状态图实现
• numericals.py - 动态几何环境中的数值引擎
• problem.py - 问题前提、结论和DAG节点类

推理引擎：

• dd.py - DD及其回溯实现
• ar.py - AR及其回溯实现
• ddar.py - DD+AR组合实现
• trace_back.py - 递归回溯和依赖差异算法

语言模型组件：

• beam_search.py - JAX中的语言模型波束解码
• models.py - Transformer模型实现
• transformer_layer.py - Transformer层实现
• lm_inference.py - 训练LM解码接口

资源文件：

• defs.txt - 不同几何构造动作的定义
• rules.txt - DD的演绎规则
• geometry_150M_generate.gin - meliad中LM的Gin配置
• imo_ag_30.txt - IMO-AG-30问题集
• jgex_ag_231.txt - JGEX-AG-231问题集

快速启动

一键执行所有指令

项目提供了完整的启动脚本：

bash run.sh

配置常用参数

在运行Python脚本前，需要设置一些常用参数：

# 符号引擎需要的定义和规则
DDAR_ARGS=(
  --defs_file=$(pwd)/defs.txt \
  --rules_file=$(pwd)/rules.txt

搜索参数设置

为快速测试，可以使用轻量级搜索参数：

BATCH_SIZE=2
BEAM_SIZE=2
DEPTH=2

SEARCH_ARGS=(
  --beam_size=$BEAM_SIZE
  --search_depth=$DEPTH
)

使用示例

运行DDAR求解器

解决IMO 2000 P1问题：

python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/imo_ag_30.txt \
--problem_name=translated_imo_2000_p1 \
--mode=ddar \
"${DDAR_ARGS[@]}"

运行AlphaGeometry求解器

解决垂心问题：

python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/examples.txt \
--problem_name=orthocenter \
--mode=alphageometry \
"${DDAR_ARGS[@]}" \
"${SEARCH_ARGS[@]}" \
"${LM_ARGS[@]}"

测试验证

运行测试套件确保一切正常：

bash run_tests.sh

性能表现

根据官方测试结果：

求解器	IMO-AG-30	JGEX-AG-231
DDAR	14	198
AlphaGeometry	25	228

注意事项

1. 硬件要求：要达到论文中的性能，需要4个V100 GPU和250个CPU工作器
2. 内存优化：此实现移除了内部基础设施依赖的优化
3. 模型一致性：不同用户可能获得不同的LM评分

故障排除

如果遇到问题，请检查：

• 虚拟环境是否正确激活
• 所有依赖包是否安装成功
• meliad库是否正确安装并添加到PYTHONPATH
• 模型权重和词汇表是否下载完整

通过本指南，您应该已经掌握了AlphaGeometry的基本使用方法。现在可以开始探索这个强大的几何AI工具，解锁智能几何推理的无限可能。