bethgelab/simplegeometry

--- license: cc-by-4.0 --- # SimpleGeometry This repository contains simplified code for the paper: **Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry, Arxiv**</br> Shiven Sinha\*, Ameya Prabhu\*, Ponnurangam Kumaraguru, Siddharth Bhat⁺, Matthias Bethge⁺</br> [[PDF](https://arxiv.org/abs/2404.06405)] [[Slides]()] [[Bibtex](https://huggingface.co/datasets/bethgelab/simplegeometry/#citation)] To run either of Wu's, Full-Angle, or Deductive Database provers implemented in JGEX, - Download [JGEX](https://github.com/kovzol/Java-Geometry-Expert) - Import any of problems files. The diagram should be automatically constructed once this is done. - Pick your prover from the top right corner of the left pane and click on the prove button. In the case of 2002 P2A and P2B, you need to launch a separate JGEX instance and recreate the diagram from scratch using the provided file as reference. The proof process must be performed on this new instance. We did not require changing the default memory limits to produce the results in the paper. However, you can additionally build JGEX from source to increase the memory limits for provers. Follow the instructions available in JGEX's documentation, and before running `./gradlew run`, (tweak and) paste the following line of code in the terminal to the memory limit to 10GB. ```bash export _JAVA_OPTIONS="-Xmx10g" ``` #### If you discover any bugs in the code please contact me, I will cross-check them with my nightmares. # Citation We hope SimpleGeometry provides strong baselines, and Wu's method is useful for your cool automated theorem prover! To cite our work: ``` @inproceedings{sinha2024wu, title={Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry}, author={Sinha, Shiven and Prabhu, Ameya and Kumaraguru, Ponnurangam and Bhat, Siddharth and Bethge, Matthias}, booktitle={arXiv preprint arXiv:2404.06405}, month={April}, year={2024} } ```license: cc-by-4.0 # 简易几何（SimpleGeometry） 本仓库包含对应论文的简化代码： **《吴方法（Wu's Method）可助力符号人工智能比肩银牌得主，阿尔法几何（AlphaGeometry）在国际数学奥林匹克（International Mathematical Olympiad，简称IMO）几何题中超越金牌得主》，Arxiv** 作者：Shiven Sinha*、Ameya Prabhu*、Ponnurangam Kumaraguru、Siddharth Bhat⁺、Matthias Bethge⁺ [[论文PDF](https://arxiv.org/abs/2404.06405)] [[演示幻灯片]()] [[引用格式（Bibtex）](https://huggingface.co/datasets/bethgelab/simplegeometry/#citation)] 若要运行基于JGEX实现的吴方法（Wu's Method）、全角法或演绎数据库证明器，请按以下步骤操作： - 下载Java几何专家（Java Geometry Expert，简称JGEX） - 导入任意一道题目的数据文件，导入完成后将自动生成对应几何图形 - 在左侧面板的右上角选择你需要使用的证明器，点击证明按钮即可启动证明流程。 针对2002年IMO几何题P2A与P2B，你需要启动独立的JGEX实例，并以提供的题目文件为参考重新绘制几何图形，证明流程需在该新实例中完成。 我们在生成论文结果时无需修改默认内存限制。若需提升证明器的内存上限，你可从源码编译JGEX。请参考JGEX官方文档，在执行`./gradlew run`命令前，在终端中输入（调整并）粘贴以下代码以将内存上限设置为10GB： bash export _JAVA_OPTIONS="-Xmx10g" #### 若你在代码中发现任何漏洞，请联系我，我将结合自身复盘逐一核查。 ## 引用 我们期望简易几何（SimpleGeometry）能够提供可靠的基准测试方案，且吴方法（Wu's Method）能为你的自动化定理证明器研发提供助力。引用我们的工作请使用以下格式： @inproceedings{sinha2024wu, title={Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry}, author={Sinha, Shiven and Prabhu, Ameya and Kumaraguru, Ponnurangam and Bhat, Siddharth and Bethge, Matthias}, booktitle={arXiv preprint arXiv:2404.06405}, month={April}, year={2024} }

原始信息汇总

数据集概述

数据集名称

SimpleGeometry

数据集内容

本数据集包含用于论文研究的简化代码，该论文探讨了Wus方法如何提升符号AI，使其在IMO几何问题中达到银牌水平，以及AlphaGeometry如何超越金牌水平。

使用方法

• 下载并安装JGEX工具。
• 导入问题文件，系统将自动构建图形。
• 在左侧窗格的右上角选择证明器，并点击证明按钮进行操作。

注意事项

对于2002 P2A和P2B问题，需启动单独的JGEX实例，并根据提供的文件重新创建图形。证明过程需在此新实例上执行。

引用信息

@inproceedings{sinha2024wu, title={Wus Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry}, author={Sinha, Shiven and Prabhu, Ameya and Kumaraguru, Ponnurangam and Bhat, Siddharth and Bethge, Matthias}, booktitle={arXiv preprint arXiv:2404.06405}, month={April}, year={2024} }