用 GeoGebra Discovery 解决奥地利奥林匹克数学竞赛问题：从中获得的教训
内容提要
本文综述几何自动推理领域进展，涵盖GeoGebra Discovery新增ShowProof命令（输出证明步骤与难度评分）、统一基准UniGeo及Geoformer模型、GeoTutor辅导系统、Inter-GPS求解器、FormalGeo形式系统与FGPS、GeoQA数据集、视觉语言模型几何推理评估以及ADG 2023会议。
延伸解读
ShowProof 命令的实用价值
GeoGebra Discovery 新增的 ShowProof 命令能输出证明步骤序列，并给出表示陈述难度或兴趣的数字。这有助于教师和学生理解几何证明的构建过程，而不仅仅是得到结论。难度评分还可用于筛选适合教学或练习的题目，但需注意其评估基于假设组合的比较，可能不适用于所有几何问题。
几何自动推理的多样化工具
文章提及了多个几何自动推理系统，如 Geoformer、GeoTutor、Inter-GPS、FormalGeo 和 FGPS 等。这些工具分别针对问题求解、辅导、形式化等不同方面，反映了该领域研究的多路径发展。读者可关注它们各自的特点，例如 FormalGeo 提供了可读、可验证的证明，而 GeoTutor 侧重个性化练习。
视觉语言模型在几何推理上的局限
文章指出，视觉语言模型在几何推理上的表现可能不如先前基准测试所暗示的那样出色，尤其是在需要长推理链的深层问题上。这表明当前模型可能更依赖记忆而非真正的推理能力。这一发现提醒研究者和教育者在应用此类模型时需谨慎评估其实际推理水平。
几何自动推理与教育结合的趋势
从 GeoTutor 到 ADG 2023 会议对教育推理的关注，可以看出几何自动推理正越来越多地融入教育场景。这些工具旨在辅助教学、提供个性化练习或激发学生兴趣。然而，文章也提到在中学引入自动推理系统面临瓶颈，实际应用仍需克服技术及教学上的挑战。
Q&A
GeoGebra Discovery 新增的 ShowProof 命令有什么作用？
ShowProof 命令可以输出 GeoGebra Discovery 执行以确认某个陈述的不同步骤序列，以及表示陈述难度或兴趣的数字。
UniGeo 基准测试是什么？它解决了什么问题？
UniGeo 是一个基于多任务转换器框架 Geoformer 的大规模统一几何问题基准测试，通过共同表达式生成的方式统一解决计算和证明问题，并提出了预测数学表达式的方法 MEP，从而提高了 Geoformer 的性能。
GeoTutor 系统如何帮助学生提高几何证明能力？
GeoTutor 是一个智能辅导系统，它能自动合成证明问题及其解决方案，以及针对学生在欧几里得几何方面的缺陷提供个性化练习问题。
Inter-GPS 是什么？它有什么特点？
Inter-GPS 是一个可解释几何问题求解器，基于形式语言和符号推理，构建了一个大规模的几何问题数据集，能够显著提高当前方法解决几何问题的效果。
FormalGeo 形式系统包含哪些内容？它的效果如何？
FormalGeo 包含 88 个几何谓词和 196 个定理，可以表示、验证和解决 IMO 级别的几何问题。后向深度优先搜索方法只有 2.42% 的问题解决失败率，结合深度学习技术可以实现更低的失败率。
视觉语言模型在几何推理上的表现如何？
通过几何问题的镜头，从多个角度评估视觉语言模型的推理能力，基准测试结果表明，这些模型在几何等主题的推理能力上并不如先前的基准测试所暗示的那样出色，特别是解决更深的问题需要更长的推理链而不是额外的记忆知识。
