使用 GeoGebra Discovery 展示证明、评估困难程度
内容提要
本文综述自动几何推理研究，涵盖：统一计算与证明的基准UniGeo及Geoformer模型；中学引入自动推理系统的瓶颈与实践；Open Geometry Prover社区项目；补全不完整猜想与证明的框架；几何定理有趣性判断及不可判定性；用Isabelle测试形式证明理解的方法；NLProofS逐步证明生成方法及其领先性能；用强化学习指导定理证明搜索的算法；融合符号与自然语言的NaturalProver证明生成系统。
延伸解读
从计算到证明：统一基准的意义
UniGeo 将几何计算题与证明题纳入同一基准，并用 Geoformer 以共同表达式生成的方式统一处理，这有助于避免两类任务各自为政的评估偏差。MEP 方法进一步提升了模型预测数学表达式的性能，说明统一框架下仍有针对性的优化空间。对读者而言，这意味着自动几何推理的评测正从单一任务转向更综合的能力衡量。
中学引入自动推理的瓶颈与实践
文章多次提到中学引入自动推理系统面临瓶颈，并介绍了基于推理规则和自动方法的实现，用于几何猜想证明，以激发学生兴趣。另一项实验则借助信息通信技术使用自动推理工具解决几何问题，试图应对这些难题。这表明自动推理在教育中的落地不仅需要工具本身，还需考虑教学场景中的实际障碍与实施方式。
补全猜想与判断有趣性：两个前沿问题
有框架利用合一逻辑和约束求解，将缺失假设、目标不明确的猜想转化为正确定理，并帮助完成草图式证明，使其既适合人类阅读又便于机器检查。另一项工作则讨论如何判断几何定理是否有趣，并引入不可判定性结果，说明判断定理生成程序能否产生有趣定理是非确定性任务。这提示自动发现定理之后，筛选与评估同样关键。
证明生成与搜索的多样化技术路线
NLProofS 通过逐步生成相关步骤，在 EntailmentBank 上取得最先进性能；NaturalProver 融合符号与自然语言生成证明，其下一步建议有超过 40% 的正确和有用率。另有算法用强化学习指导连接风格的证明搜索，减少对领域启发式的依赖。这些路线分别侧重步骤生成、语言融合与搜索策略，反映了自动定理证明领域方法上的多样性。
Q&A
UniGeo 基准测试是什么？它如何统一处理几何计算和证明问题？
UniGeo 是一个基于多任务转换器框架 Geoformer 的大规模统一几何问题基准测试。它通过共同表达式生成的方式统一解决计算和证明问题，并提出了预测数学表达式的方法 MEP，从而提高了 Geoformer 的性能。
在中学引入自动推理系统面临哪些瓶颈？有哪些实践尝试？
文章介绍了在中学引入自动推理系统面临的几个瓶颈，并讨论了一个基于推理规则和自动方法的实现，使用其进行几何猜想的证明，旨在介绍几何定理的形式证明以激发学生兴趣。此外，还有在信息和通信技术帮助下使用自动推理工具解决几何问题的实验，以解决引入中的难题。
Open Geometry Prover Community Project 的目标是什么？
该项目的目标是将不同自动几何定理证明工具的开发整合到一个共同的“伞下”，以丰富人们的数学体验。
如何补全不完整的几何猜想和证明？
通过使用合一逻辑和约束求解，提出了一个框架，用于补充不完整的猜想和证明。该框架可以将具有缺失假设和不明确目标的猜想转化为正确的定理，并帮助完成草图式证明以使其适于人类阅读和机器检查。
判断几何定理是否有趣为什么是一个不可判定问题？
文章针对自动发现几何定理和其性质的不同方法和度量进行讨论，并引入了一个不可判定性结果来证明判断定理生成程序是否能产生有趣定理是一个非确定性任务。此外，还强调了需要通过专家调查和相关度量和方法的研究明确定理生成程序和有趣几何定理之间的关系。
NLProofS 在证明生成任务上取得了什么性能？
NLProofS 是一种新的逐步方法，通过在给定假设的条件下学习生成相关步骤，从而在 NLP 中解决证明生成的问题，并在 EntailmentBank 上取得了最先进的性能。
NaturalProver 如何生成数学证明？其效果如何？
NaturalProver 通过人工提供或查找背景参考条件，能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量。在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。
