无需人类示范即可解决奥数几何问题

此仓库包含复现DDAR和AlphaGeometry所需的代码， 这两款几何定理证明器在2024年《自然》杂志论文中被介绍：

“无需人类示范即可解决奥数几何问题”。

更新（2026年1月）： AlphaGeometry2已发表，其用于DDAR的代码已在alphageometry2中发布。

依赖项

在以下说明中，我们使用Python 3.10.9，并且依赖项及其确切版本号列于requirements.txt文件中。

我们的代码依赖于meliad，它并未注册到pip包管理器中。有关如何手动安装meliad的说明见下文。

请注意，即使没有meliad和sentencepiece依赖项，仍然可以运行DDAR求解器。

运行说明

本README.md中的所有说明可以通过以下命令一次性执行：

bash run.sh

下面我们将逐步解释这些说明。

安装依赖项、下载权重和词汇表

安装过程在一个虚拟环境中进行：

virtualenv -p python3 .
source ./bin/activate
pip install --require-hashes -r requirements.txt

下载权重和词汇表：

bash download.sh
DATA=ag_ckpt_vocab

最后，由于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

设置常用参数

在运行Python脚本之前，我们先准备一些常用的参数。符号引擎需要定义和推理规则才能运行。这些定义和规则分别提供在defs.txt和rules.txt两个文本文件中。

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
)

注意：我们论文中的结果可以通过设置BATCH_SIZE=32、BEAM_SIZE=512、DEPTH=16来获得，具体如方法部分所述。为满足IMO竞赛的时间限制，需要4张V100显卡和250个CPU工作进程，详见扩展数据图1。此外，我们还去除了其他内存和速度优化措施，以减少内部依赖并提高代码可读性。

假设下载的检查点和词汇表位于DATA目录下，而安装的meliad源代码位于MELIAD_PATH目录。我们使用gin库来管理模型配置，遵循meliad的惯例。现在我们定义与语言模型相关的参数：

LM_ARGS=(
  --ckpt_path=$DATA \
  --vocab_path=$DATA/geometry.757.model
  --gin_search_paths=$MELIAD_PATH/transformer/configs,$(pwd) \
  --gin_file=base_htrans.gin \
  --gin_file=size/medium_150M.gin \
  --gin_file=options/positions_t5.gin \
  --gin_file=options/lr_cosine_decay.gin \
  --gin_file=options/seq_1024_nocache.gin \
  --gin_file=geometry_150M_generate.gin \
  --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True \
  --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE \
  --gin_param=TransformerTaskConfig.sequence_length=128 \
  --gin_param=Trainer.restore_state_variables=False
);

提示：即使不定义SEARCH_ARGS和LM_ARGS，仍然可以运行DDAR求解器。在这种情况下，只需在alphageometry.py中禁用lm_inference模块的导入即可。

运行DDAR

该脚本通过读取文本文件中的问题列表来加载一个问题，并根据其名称解决列表中的特定问题。我们通过--problems_file和--problem_name这两个参数传递这两条信息。我们使用--mode=ddar来指示要使用DDAR求解器。

下面我们展示了该求解器如何解决2000年IMO第1题：

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

预期输出如下：

graph.py:468] translated_imo_2000_p1
graph.py:469] a b = segment a b; g1 = on_tline g1 a a b; g2 = on_tline g2 b b a; m = on_circle m g1 a, on_circle m g2 b; n = on_circle n g1 a, on_circle n g2 b; c = on_pline c m a b, on_circle c g1 a; d = on_pline d m a b, on_circle d g2 b; e = on_line e a c, on_line e b d; p = on_line p a n, on_line p c d; q = on_line q b n, on_line q c d ? cong e p e q
ddar.py:41] Depth 1/1000 time = 1.7772269248962402
ddar.py:41] Depth 2/1000 time = 5.63526177406311
ddar.py:41] Depth 3/1000 time = 6.883412837982178
ddar.py:41] Depth 4/1000 time = 10.275688409805298
ddar.py:41] Depth 5/1000 time = 12.048273086547852
alphageometry.py:190]
==========================
 * From theorem premises:
A B G1 G2 M N C D E P Q : Points
AG_1 ⟂ AB [00]
BA ⟂ G_2B [01]
G_2M = G_2B [02]
G_1M = G_1A [03]

...
[log omitted]
...

036. ∠QEB = ∠(QP-EA) [46] & ∠(BE-QP) = ∠AEP [55] ⇒  ∠EQP = ∠QPE [56]
037. ∠PQE = ∠EPQ [56] ⇒  EP = EQ

==========================

输出首先列出所使用的相关前提条件，然后逐步展示证明步骤。所有谓词都进行了编号，以便追踪它们是如何从前提条件推导出来的，并证明整个证明是完全合理的。

提示：此外，如果添加--out_file=path/to/output/text/file.txt参数，证明内容将被写入指定的文本文件中。

在imo_ag_30.txt中的所有问题上运行后，将得到其中14个问题的解答，正如我们论文中的表1所示。

运行 AlphaGeometry：

作为一个简单的示例，我们从 --problem_file=examples.txt 中加载 --problem_name=orthocenter。 这一次，我们传递 --mode=alphageometry 来使用 AlphaGeometry 求解器，并传递 SEARCH_ARGS 和 LM_ARGS 标志。

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

预期输出如下：

...
[日志省略]
...
training_loop.py:725] 总参数量：152072288
training_loop.py:739] 总状态大小：0
training_loop.py:492] 训练循环：为模式 beam_search 创建任务

graph.py:468] 垂心
graph.py:469] a b c = 三角形 a b c；d = 在 tline d b a c 上，也在 tline d c a b 上？垂线 a d b c
ddar.py:41] 深度 1/1000 时间 = 0.009987592697143555 分支 = 4
ddar.py:41] 深度 2/1000 时间 = 0.00672602653503418 分支 = 0
alphageometry.py:221] DD+AR 未能解决该问题。
alphageometry.py:457] 深度 0。有 1 个节点待扩展：
alphageometry.py:460] {S} a : ; b : ; c : ; d : T a b c d 00 T a c b d 01 ? T a d b c {F1} x00
alphageometry.py:465] 从 {S} a : ; b : ; c : ; d : T a b c d 00 T a c b d 01 ? T a d b c {F1} x00 解码
...
[日志省略]
...
alphageometry.py:470] LM 输出（分数=-1.102287）：“e : C a c e 02 C b d e 03；”
alphageometry.py:471] 翻译：“e = 在线 e a c 上，也在线 e b d 上”

alphageometry.py:480] 求解：“a b c = 三角形 a b c；d = 在 tline d b a c 上，也在 tline d c a b 上；e = 在线 e a c 上，也在线 e b d 上？垂线 a d b c”
graph.py:468]
graph.py:469] a b c = 三角形 a b c；d = 在 tline d b a c 上，也在 tline d c a b 上；e = 在线 e a c 上，也在线 e b d 上？垂线 a d b c
ddar.py:41] 深度 1/1000 时间 = 0.021120786666870117
ddar.py:41] 深度 2/1000 时间 = 0.033370018005371094
ddar.py:41] 深度 3/1000 时间 = 0.04297471046447754
alphageometry.py:140]
==========================
 * 由定理前提：
A B C D：点
BD ⟂ AC [00]
CD ⟂ AB [01]

 * 辅助构造：
E：点
E,B,D 共线 [02]
E,C,A 共线 [03]

 * 证明步骤：
001. E,B,D 共线 [02] & E,C,A 共线 [03] & BD ⟂ AC [00] ⇒ ∠BEA = ∠CED [04]
002. E,B,D 共线 [02] & E,C,A 共线 [03] & BD ⟂ AC [00] ⇒ ∠BEC = ∠AED [05]
003. A,E,C 共线 [03] & E,B,D 共线 [02] & AC ⟂ BD [00] ⇒ EC ⟂ EB [06]
004. EC ⟂ EB [06] & CD ⟂ AB [01] ⇒ ∠(EC-BA) = ∠(EB-CD) [07]
005. E,C,A 共线 [03] & E,B,D 共线 [02] & ∠(EC-BA) = ∠(EB-CD) [07] ⇒ ∠BAE = ∠CDE [08]
006. ∠BEA = ∠CED [04] & ∠BAE = ∠CDE [08]（相似三角形）⇒ EB:EC = EA:ED [09]
007. EB:EC = EA:ED [09] & ∠BEC = ∠AED [05]（相似三角形）⇒ ∠BCE = ∠ADE [10]
008. EB:EC = EA:ED [09] & ∠BEC = ∠AED [05]（相似三角形）⇒ ∠EBC = ∠EAD [11]
009. ∠BCE = ∠ADE [10] & E,C,A 共线 [03] & E,B,D 共线 [02] & ∠EBC = ∠EAD [11] ⇒ AD ⟂ BC
==========================

alphageometry.py:505] 已解决。

注意：点 H 会被自动重命名为 D， 因为语言模型是在合成问题上训练的， 这些问题中的点都按字母顺序命名，因此在测试时它也期望相同的命名方式。

注意：在本实现的 AlphaGeometry 中， 我们移除了所有依赖于内部基础设施的优化措施，例如： 多 GPU 上的并行模型推理、多 CPU 上的并行 DDAR、LM 和 DDAR 的并行执行、 不同问题之间共享的 CPU 工作池等。 我们还移除了部分内存/速度优化和代码抽象，以提高代码的可读性。

从输出中可以看出，最初 DDAR 未能解决该问题。 语言模型提出了两个辅助构造（因为 BATCH_SIZE=2）：

• e = eqdistance e c a b, eqdistance e b a c，即 将 E 构造为以 C 为圆心、半径为 AB 的圆与以 B 为圆心、半径为 AC 的圆的交点。该构造的得分为 -1.186。
• e = on_line e a c, on_line e b d，即 E 是 AC 和 BD 的交点。该构造的得分更高（-1.102287）比前一个。

由于第二个构造的得分更高，DDAR 首先尝试了第二个构造，并立即找到了解决方案。 因此，证明搜索终止，没有进行第二次迭代。

结果

在尝试复现我们论文中的 AlphaGeometry 数据之前， 请确保通过准备好的测试套件中的所有测试：

bash run_tests.sh

注意：Issues#14 报告称，尽管顶级波束解码仍然相同，但语言模型对不同用户给出的分数并不一致。

然后，传递 --problem_file（列）和 --mode（行）的相应值， 并对所有问题进行迭代，以获得以下结果：

已解决问题的数量：

	imo_ag_30.txt	jgex_ag_231.txt
ddar	14	198
alphageometry	25	228

源代码说明

本仓库中的文件包括用于运行求解器的 Python 模块/脚本，以及脚本执行所需的资源文件。我们将在下面列出每个文件及其描述。

文件名	描述
geometry.py	实现证明状态图中的节点（点、线、圆等）。
numericals.py	实现动态几何环境中的数值引擎。
graph_utils.py	实现证明状态图的工具函数。
graph.py	实现证明状态图。
problem.py	实现表示问题前提、结论及 DAG 节点的类。
dd.py	实现 DD 及其回溯机制。
ar.py	实现 AR 及其回溯机制。
trace_back.py	实现递归回溯和依赖差异算法。
ddar.py	实现 DD+AR 的组合方法。
beam_search.py	在 JAX 中实现语言模型的束搜索解码。
models.py	实现 Transformer 模型。
transformer_layer.py	实现 Transformer 层。
decoder_stack.py	实现 Transformer 解码器堆栈。
lm_inference.py	实现与训练好的语言模型交互以进行解码的接口。
alphageometry.py	主脚本，用于加载问题、调用 DD+AR 或 AlphaGeometry 求解器，并输出解。
pretty.py	对求解器输出的解进行美化格式化。
*_test.py	对应模块的测试文件。
download.sh	用于下载模型检查点和语言模型的脚本。
run.sh	执行 README 中指令的脚本。
run_tests.sh	执行测试套件的脚本。

资源文件：

资源文件名	描述
defs.txt	不同几何作图操作的定义。
rules.txt	DD 的推理规则。
geometry_150M_generate.gin	meliad 中实现的语言模型的 Gin 配置。
imo_ag_30.txt	IMO-AG-30 中的问题。
jgex_ag_231.txt	JGEX-AG-231 中的问题。

引用本工作

@Article{AlphaGeometryTrinh2024,
  author  = {Trinh, Trieu and Wu, Yuhuai and Le, Quoc and He, He and Luong, Thang},
  journal = {Nature},
  title   = {Solving Olympiad Geometry without Human Demonstrations},
  year    = {2024},
  doi     = {10.1038/s41586-023-06747-5}
}

致谢

本研究是 Google Brain 团队（现为 Google DeepMind）与纽约大学计算机科学系的合作成果。我们感谢 Rif A. Saurous、Denny Zhou、Christian Szegedy、Delesley Hutchins、Thomas Kipf、Hieu Pham、Petar Veličković、Debidatta Dwibedi、Kyunghyun Cho、Lerrel Pinto、Alfredo Canziani、Thomas Wies、He He 的研究团队、Evan Chen（美国 IMO 团队教练）、Mirek Olsak、Patrik Bak，以及 Nature 杂志的三位审稿人，感谢他们提供的帮助和支持。

AlphaGeometry 的代码与以下独立库和软件包进行通信或引用：

• Abseil
• JAX
• matplotlib
• NumPy
• SciPy
• TensorFlow
• Meliad
• Flax
• Gin
• T5
• SentencePiece

我们感谢所有这些项目的贡献者和维护者！

免责声明

本项目并非 Google 官方支持的产品。

本研究代码以“现状”形式提供给更广泛的研究社区。Google 不承诺以任何方式维护或支持此代码。

代码许可

版权所有 © 2023 DeepMind Technologies Limited

所有软件均采用 Apache License, Version 2.0（Apache 2.0）许可；除非符合 Apache 2.0 许可条款，否则不得使用本文件。您可以在以下网址获取 Apache 2.0 许可协议：
https://www.apache.org/licenses/LICENSE-2.0

所有其他材料均采用 Creative Commons Attribution 4.0 国际许可（CC-BY）。您可以在以下网址获取 CC-BY 许可协议：
https://creativecommons.org/licenses/by/4.0/legalcode

除非适用法律要求或另有书面约定，否则在此处根据 Apache 2.0 或 CC-BY 许可分发的所有软件和材料均按“现状”提供，不附带任何形式的明示或默示担保或条件。具体的权利和限制请参阅相关许可协议。

模型参数许可

AlphaGeometry 的检查点和词汇表依据 Creative Commons Attribution 4.0 国际许可（CC BY 4.0）条款提供。详细信息请参见：
https://creativecommons.org/licenses/by/4.0/legalcode

AlphaGeometry 快速上手指南

AlphaGeometry 是 Google DeepMind 开发的几何定理证明系统，结合了符号推理引擎（DDAR）和语言模型（LM），能够解决奥林匹克级别的几何问题而无需人类演示数据。

环境准备

• 操作系统: Linux 或 macOS (Windows 用户建议使用 WSL2)
• Python 版本: 推荐 Python 3.10.9
• 硬件要求:
  • 仅运行 DDAR: 普通 CPU 即可。
  • 运行完整 AlphaGeometry (含 LM): 需要 GPU 支持（论文实验使用 4x V100），若仅测试简单示例，单张消费级显卡或纯 CPU（速度较慢）也可尝试。
• 前置依赖: git, virtualenv

安装步骤

1. 创建虚拟环境并安装基础依赖

# 创建虚拟环境
virtualenv -p python3 .
source ./bin/activate

# 安装 requirements.txt 中列出的依赖包
pip install --require-hashes -r requirements.txt

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

执行官方提供的下载脚本，并将数据路径设置为环境变量：

bash download.sh
export DATA=ag_ckpt_vocab

3. 手动安装 meliad 库

由于 meliad 未发布在 PyPI 上，需从源码安装：

export MELIAD_PATH=meliad_lib/meliad
mkdir -p $MELIAD_PATH

# 克隆仓库
git clone https://github.com/google-research/meliad $MELIAD_PATH

# 添加至 PYTHONPATH
export PYTHONPATH=$PYTHONPATH:$MELIAD_PATH

提示: 国内用户若克隆 GitHub 速度慢，可尝试使用镜像源或代理加速 git clone 过程。

基本使用

在使用前，需先定义通用的配置参数（符号引擎规则、搜索参数及模型配置）。请在终端中依次执行以下命令设置环境变量：

# 1. 设置符号引擎规则文件路径
DDAR_ARGS=(
  --defs_file=$(pwd)/defs.txt \
  --rules_file=$(pwd)/rules.txt \
);

# 2. 设置搜索参数 (示例使用轻量级参数，复现论文结果需调大数值)
BATCH_SIZE=2
BEAM_SIZE=2
DEPTH=2

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

# 3. 设置语言模型配置
LM_ARGS=(
  --ckpt_path=$DATA \
  --vocab_path=$DATA/geometry.757.model \
  --gin_search_paths=$MELIAD_PATH/transformer/configs,$(pwd) \
  --gin_file=base_htrans.gin \
  --gin_file=size/medium_150M.gin \
  --gin_file=options/positions_t5.gin \
  --gin_file=options/lr_cosine_decay.gin \
  --gin_file=options/seq_1024_nocache.gin \
  --gin_file=geometry_150M_generate.gin \
  --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True \
  --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE \
  --gin_param=TransformerTaskConfig.sequence_length=128 \
  --gin_param=Trainer.restore_state_variables=False
);

模式一：运行 DDAR (纯符号推理)

适用于不需要神经网络辅助的几何问题，速度快，无需 GPU。

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

预期输出: 终端将打印出推导步骤，包括前提条件、辅助构造点及最终的证明逻辑链。

模式二：运行完整 AlphaGeometry (DDAR + 语言模型)

适用于复杂问题，当纯符号推理失败时，语言模型会提议辅助构造线。

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

预期输出:

1. 系统首先尝试 DDAR，若失败则启动语言模型。
2. 语言模型生成辅助构造建议（如添加新的点或线）。
3. 系统基于新构造再次尝试证明，直至成功或耗尽搜索深度。
4. 最终输出完整的证明过程，标记为 Solved。

注意: 若只需运行 DDAR 而不使用语言模型，可省略 SEARCH_ARGS 和 LM_ARGS，并在代码中禁用 lm_inference 模块导入以简化依赖。