AAAIOct, 2015

智能辅导系统中几何问题的自动合成

PDF
TL;DR该论文介绍了一个名为 GeoTutor 的智能辅导系统，它能自动合成证明问题及其解决方案，以及针对学生在欧几里得几何方面的缺陷提供个性化练习问题。
intelligent tutoring systemgeotutoreuclidean geometrysynthesis of proof problemspersonalized practice problems
发现论文，激发创造
  • 基于约束求解的合成几何陈述和证明的自动补全方法

    通过使用合一逻辑和约束求解，我们提出了一个框架，用于补充不完整的猜想和证明。该框架可以将具有缺失假设和不明确目标的猜想转化为正确的定理，并帮助完成草图式证明以使其适于人类阅读和机器检查。

    Jan, 2024

  • 中学自动推理入门：四个几何问题

    本文探讨了在信息和通信技术的帮助下使用自动推理工具解决几何问题的实验，以解决在中学自动推理系统引入中所面临的难题。

    Feb, 2022

  • 自动形式化欧几里德几何

    本文介绍了一种自动形式化欧几里得几何的神经符号框架，该框架结合了领域知识、SMT 求解器和大型语言模型，这一框架的挑战之一在于通过定理证明器自动填充图形信息以简化模型，实验结果展示了自动形式化几何问题时最新的语言模型的能力和局限性。

    May, 2024

  • GeoQA：一个面向多模态数字推理的几何问答基准

    本文提出了大规模的 Geometric Question Answering 数据集 GeoQA 和一个神经几何求解器 NGS，并通过多模式信息综合分析和生成可解释性程序来解决几何问题。

    May, 2021

  • 通过模拟人类双重推理过程学习解决几何问题

    提出了一个名为 DualGeoSolver 的双重推理几何求解器，通过模拟人类的双重推理过程，从对人类推理过程和知识应用的显式建模中提高求解几何问题的准确率和鲁棒性。

    May, 2024

  • 基于规则的定理证明器：中学证明入门

    介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。

    Mar, 2023

  • 使用 GeoGebra Discovery 自动演绎解决 Náboj 2023 竞赛中的几何问题

    使用计算机和 GeoGebra Discovery 等软件工具，我们解决了 N'aboj 2023 竞赛中的一些几何问题，并通过符号计算分析了输入机器的困难，设定了未来使此类竞赛问题更易解决的目标。

    Jan, 2024

  • FGeo-TP: 几何问题的语言模型增强求解器

    应用现代人工智能技术解决几何问题和自动演绎证明一直以来都是数学和人工智能交叉领域的重要挑战。本文提出了一种名为 FGeo-P 的定理预测器，利用语言模型预测几何问题的定理序列，从而提高了解决几何问题的性能，实验证明在 FormalGeo7k 数据集的问题解决率从 39.7% 提升至 80.86%。此外，FGeo-TP 在不同难度问题上表现出了解决时间和搜索步骤显著减少的特点。

    Feb, 2024

  • GOLD: 几何问题解决器与自然语言描述

    通过分别处理图形符号和几何基元来增强几何关系的提取，并将提取的关系转化为自然语言描述，从而高效利用大型语言模型解决几何数学问题。实验证明，GOLD 模型在 UniGeo 数据集上表现优于 Geoformer，并分别在计算和证明子集中提高了 12.7% 和 42.1% 的准确率。此外，在 PGPS9K 和 Geometry3K 数据集上也优于 PGPSNet，分别获得了 1.8% 和 3.2% 的准确率提升。

    May, 2024

  • 用 GeoGebra Discovery 解决奥地利奥林匹克数学竞赛问题：从中获得的教训

    我们通过 GeoGebra Discovery 中的自动推理工具解决了奥地利数学奥林匹克 2023 年的一个问题，并且描述了其中的四种反馈形式：即时的自动解答、根据最新提案进行复杂性评估、找到给定命题的更一般化命题，以及使用 LocusEquation 命令时出现的大量退化情况的分析困难。

    Jan, 2024