无需人类演示即可解决奥林匹克几何问题

该存储库包含重现 DDAR 和 AlphaGeometry 所需的代码，这两个几何定理证明器在论文 introduced in the Nature 2024 paper:

"无需人类演示即可解决奥林匹克几何问题".

无需人类演示即可解决奥林匹克几何问题

该存储库包含重现 DDAR 和 AlphaGeometry 所需的代码，这两个几何定理证明器在Nature 2024论文中介绍：

“无需人类演示即可解决奥林匹克几何问题”。

依赖关系

对于下面提供的说明，我们使用 Python 3.10.9 以及依赖项，其确切版本号在 中列出requirements.txt。

我们的代码依赖于meliad, 这不是一个注册的包pip。有关如何手动安装的信息，请参阅下面的说明meliad。

meliad请注意，在没有和依赖项的情况下，人们仍然可以运行 DDAR 求解器sentencepiece。

运行指令

其中的所有指令都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如 方法部分所述。为了保持在 IMO 时间限制之内，需要 4 个 V100-GPU 和 250 个 CPU 工作线程，如扩展数据 - 图 1 所示。请注意，由于内部依赖性，我们还放弃了其他内存/速度优化，以提高代码清晰度。BEAM_SIZE=512DEPTH=16

假设下载的检查点和词汇表位于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提示：请注意，您仍然可以在不定义和 的情况下运行 DDAR 求解器LM_ARGS。lm_inference在这种情况下，只需禁用内部模块的导入即可alphageometry.py。

运行DDAR

该脚本通过从文本文件中读取问题列表来加载问题，并根据其名称解决列表中的特定问题。--problems_file我们通过标志和传递这两条信息 --problem_name。我们用--mode=ddar来表示我们想要使用 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[@]}"

期望以下输出

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]
...

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

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

输出首先包含它使用的相关前提列表，然后是逐步构建证明的证明步骤。所有谓词都经过编号，以跟踪它们是如何从前提导出的，并表明证明是完全合理的。

提示：另外传递该标志--out_file=path/to/output/text/file.txt 会将证明写入文本文件。

运行 中的所有问题imo_ag_30.txt将产生其中 14 个问题的解决方案，如我们论文中的表 1 所示。

运行 AlphaGeometry：

作为一个简单的例子，我们--problem_name=orthocenter 从加载--problem_file=examples.txt。这次，我们--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[@]}"

预期输出如下：

...
[log omitted]
...
training_loop.py:725] Total parameters: 152072288
training_loop.py:739] Total state size: 0
training_loop.py:492] Training loop: creating task for mode beam_search
graph.py:468] orthocenter
graph.py:469] a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b ? perp a d b c
ddar.py:41] Depth 1/1000 time = 0.009987592697143555 branch = 4
ddar.py:41] Depth 2/1000 time = 0.00672602653503418 branch = 0
alphageometry.py:221] DD+AR failed to solve the problem.
alphageometry.py:457] Depth 0. There are 1 nodes to expand:
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] Decoding from {S} a : ; b : ; c : ; d : T a b c d 00 T a c b d 01 ? T a d b c {F1} x00
...
[log omitted]
...
alphageometry.py:470] LM output (score=-1.102287): "e : C a c e 02 C b d e 03 ;"
alphageometry.py:471] Translation: "e = on_line e a c, on_line e b d"
alphageometry.py:480] Solving: "a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b; e = on_line e a c, on_line e b d ? perp a d b c"
graph.py:468]
graph.py:469] a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b; e = on_line e a c, on_line e b d ? perp a d b c
ddar.py:41] Depth 1/1000 time = 0.021120786666870117
ddar.py:41] Depth 2/1000 time = 0.033370018005371094
ddar.py:41] Depth 3/1000 time = 0.04297471046447754
alphageometry.py:140]

* From theorem premises:
A B C D : Points
BD ⟂ AC [00]
CD ⟂ AB [01]
* Auxiliary Constructions:
E : Points
E,B,D are collinear [02]
E,C,A are collinear [03]
* Proof steps:

E,B,D are collinear [02] & E,C,A are collinear [03] & BD ⟂ AC [00] ⇒  ∠BEA = ∠CED [04]
E,B,D are collinear [02] & E,C,A are collinear [03] & BD ⟂ AC [00] ⇒  ∠BEC = ∠AED [05]
A,E,C are collinear [03] & E,B,D are collinear [02] & AC ⟂ BD [00] ⇒  EC ⟂ EB [06]
EC ⟂ EB [06] & CD ⟂ AB [01] ⇒  ∠(EC-BA) = ∠(EB-CD) [07]
E,C,A are collinear [03] & E,B,D are collinear [02] & ∠(EC-BA) = ∠(EB-CD) [07] ⇒  ∠BAE = ∠CDE [08]
∠BEA = ∠CED [04] & ∠BAE = ∠CDE [08] (Similar Triangles)⇒  EB:EC = EA:ED [09]
EB:EC = EA:ED [09] & ∠BEC = ∠AED [05] (Similar Triangles)⇒  ∠BCE = ∠ADE [10]
EB:EC = EA:ED [09] & ∠BEC = ∠AED [05] (Similar Triangles)⇒  ∠EBC = ∠EAD [11]
∠BCE = ∠ADE [10] & E,C,A are collinear [03] & E,B,D are collinear [02] & ∠EBC = ∠EAD [11] ⇒  AD ⟂ BC
==========================

alphageometry.py:505] Solved.

注意：点H会自动重命名为D，因为 LM 是针对综合问题进行训练的，其中点按字母顺序命名，因此在测试期间预计也是如此。

注意：在 AlphaGeometry 的实现中，我们删除了所有依赖于内部基础设施的优化，例如，多 GPU 上的并行模型推理、多个 CPU 上的并行 DDAR、LM 和 DDAR 的并行执行、跨不同问题的 CPU 工作线程共享池、等等。我们还删除了一些内存/速度优化和代码抽象，以提高代码清晰度。

从输出中可以看出，DDAR 最初未能解决该问题。LM 提出了两个辅助结构（因为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的交集。该结构比之前的结构得分更高（ ）。ACBD-1.102287

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

结果

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

bash run_tests.sh

--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_layer.py	实现变压器层。
decoder_stack.py	实现变压器解码器堆栈。
lm_inference.py	实现一个经过训练的 LM 的接口来执行解码。
alphageometry.py	加载问题、调用 DD+AR 或 AlphaGeometry 求解器并打印解决方案的主脚本。
pretty.py	漂亮地格式化求解器输出的解决方案。
*_test.py	测试相应的模块。
download.sh	下载模型检查点和 LM 的脚本
run.sh	用于执行 README 中指令的脚本。
run_tests.sh	执行测试套件的脚本。

资源文件：

资源文件名	描述
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 中的问题。

引用这篇作品

@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、Kunghyun Cho、Lerrel Pinto、Alfredo Canziani、Thomas Wies、He He 研究小组、Evan Chen（美国IMO 团队教练）、Mirek Olsak、Patrik Bak 以及所有三位 Nature 裁判的帮助和支持。

AlphaGeometry 的代码与以下单独的库和包进行通信和/或引用：

• 绳降
• 贾克斯
• 绘图库
• 数值模拟
• 科学Py
• TensorFlow
• 梅利亚德
• 亚麻
• 杜松子酒
• T5
• 句子片段

我们感谢所有贡献者和维护者！

免责声明

这不是 Google 官方支持的产品。

该研究代码“按原样”提供给更广泛的研究社区。Google 不承诺以任何方式维护或以其他方式支持此代码。

代码许可

版权所有 2023 DeepMind 技术有限公司

所有软件均根据 Apache 许可证 2.0 版 (Apache 2.0) 获得许可；除非遵守 Apache 2.0 许可证，否则您不得使用此文件。您可以在以下位置获取 Apache 2.0 许可证的副本： https: //www.apache.org/licenses/LICENSE-2.0

所有其他材料均根据知识共享署名 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 International (CC BY 4.0) 许可证的条款提供。您可以在以下位置找到详细信息： https ://creativecommons.org/licenses/by/4.0/legalcode