Jan, 2024

使用 GeoGebra Discovery 展示证明、评估困难程度

PDF
TL;DR我们描述了我们在 GeoGebra Discovery 中开发的自动推理工具的一些持续改进，提供了这些新功能的不同性能示例。我们描述了新的 ShowProof 命令，它输出 GeoGebra Discovery 执行以确认某个陈述的不同步骤序列，以及表示陈述难度或兴趣的数字。提出了此评估措施的建议，涉及将论点（或结论）的表达作为假设的组合进行比较。
automated reasoning toolsgeogebra discoveryshowproof commandassessment measurecombination of hypotheses
发现论文，激发创造
  • 用 GeoGebra Discovery 解决奥地利奥林匹克数学竞赛问题：从中获得的教训

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

    Jan, 2024

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

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

    Jan, 2024

  • UniGeo: 通过重构数学表达式统一几何逻辑推理

    本文介绍了一个基于多任务转换器框架 Geoformer 的大规模统一几何问题基准测试 UniGeo，通过共同表达式生成的方式统一解决计算和证明问题，并提出了预测数学表达式的方法 MEP，从而提高了 Geoformer 的性能。

    Dec, 2022

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

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

    Mar, 2023

  • 开放几何证明社区项目

    本文描述了 Open Geometry Prover Community Project 的目标和实施步骤，旨在将不同自动几何定理证明工具的开发整合到一个共同的 “伞下”，以丰富人们的数学体验。

    Jan, 2022

  • 基于约束求解的合成几何陈述和证明的自动补全方法

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

    Jan, 2024

  • 几何中自动定理生成 / 发现的方法和度量考虑

    为了发现并判断几何定理的有趣性，本文针对自动发现几何定理和其性质的不同方法和度量进行讨论，并引入了一个不可判定性结果来证明判断定理生成程序是否能产生有趣定理是一个非确定性任务。此外，还强调了需要通过专家调查和相关度量和方法的研究明确定理生成程序和有趣几何定理之间的关系。

    Jan, 2024

  • 使用验证器引导搜索生成自然语言证明

    本文介绍了一种新的逐步方法 NLProofS，通过在给定假设的条件下学习生成相关步骤，从而在 NLP 中解决证明生成的问题，并在 EntailmentBank 上取得了最先进的性能。

    May, 2022

  • 强化学习定理证明

    提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

    May, 2018

  • 自然证明器：基于语言模型的数学证明生成

    通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。

    May, 2022