Newclid：一個對使用者更友善的 AlphaGeometry 替代方案

核心概念

Newclid 是一個基於 AlphaGeometry 的全新符號幾何求解器，它透過模組化程式碼庫、新的除錯和視覺化工具以及 GeoGebra 整合，顯著提高了使用者友好性和推理能力。

摘要

Newclid：一個對使用者更友善的 AlphaGeometry 替代方案

本研究介紹了 Newclid，這是一個基於 AlphaGeometry 的全新符號幾何求解器。Newclid 的核心是一個名為 DDARN（源自 DDAR-Newclid）的符號求解器，它是對 AlphaGeometry 的 DDAR 符號求解器的重大重構和升級，其目標是讓終端使用者和希望擴展程式碼庫的程式設計師都能更輕鬆地使用。對於程式設計師而言，改進之處包括模組化程式碼庫以及新的除錯和視覺化工具。對於使用者而言，Newclid 包含一個新的命令列介面 (CLI)，它提供代理程式來引導 DDARN 的介面。DDARN 在其內部推理方面非常靈活，可以由代理程式進行操控。此外，我們支援 GeoGebra 的輸入，使 Newclid 更容易在教育環境中使用。此外，Newclid 可解決的問題範圍已擴展到包括能夠更好地理解度量幾何概念（長度、角度）以及在證明中使用畢氏定理等定理。我們修復了錯誤並提高了可重複性。最後，我們重新評估了 AlphaGeometry 無法解決的原始 AG-30 資料集中剩餘的五個問題，並將它們與以廣度優先搜尋代理模式執行的 DDARN 的能力進行了對比（這對應於 DDARN 的預設執行方式），發現 DDARN 解決了一個額外問題。我們已在以下網址開源我們的程式碼：
https://github.com/LMCRC/Newclid

1.1. AlphaGeometry 的一般說明
AlphaGeometry [Trinh et al., 2024] 展示了解決國際數學奧林匹克 (IMO) 級別幾何問題的能力，其表現可與頂尖的人類競爭者相媲美。AlphaGeometry 的核心是一種基於 JGEX [Ye et al., 2011] 的形式語言，用於編碼幾何問題和定理，以及一個以 Python 編寫的稱為 DDAR 的符號推理引擎（有關更多資訊，請參閱第 4.4.2 節），它是 Trinh et al. [2024] 對早期符號 AI 引擎 [Chou et al., 2000] 的擴展和重新實作。
1.2. 與 DDAR 交織在原始作品中是一個大型語言模型 (LLM)
該模型在使用 DDAR 生成的合成證明資料集上進行訓練，用於預測 DDAR 可以用來得出新推論的新幾何子句。
1.3. AlphaGeometry 的推理迴圈
AlphaGeometry 的工作原理如下：DDAR 迭代可以從先前陳述中邏輯證明為真的陳述，直到找到需要證明的內容。有很多方法可以找到新的陳述：其中一批來自於透過 defs.txt 檔案中描述的規則將子句擴展為陳述。然後，應用構成 DDAR 的 AR 模組的順序迭代（有關更多資訊，請參閱第 4.4.2 節），然後應用 rules.txt 檔案中的規則，直到達到目標或不動點。如果達到不動點，將呼叫 LLM 新增新的子句，以便迭代可以重新開始。
1.4. AlphaGeometry 的問題
儘管 AlphaGeometry 具有令人印象深刻的推理能力，但它在使用者友好性方面存在局限性，無論是對於終端使用者還是對於有興趣擴展當前程式碼庫及其可處理問題範圍的程式設計師而言都是如此。

**使用者友好性問題：**使用者必須克服三個主要障礙才能使用 AlphaGeometry：

安裝 AlphaGeometry 很困難，主要是因為 AlphaGeometry 所依賴的 Meliad 庫1 難以安裝。
必須使用 JGEX 形式語言輸入問題。
AlphaGeometry 系統中的 rules.txt 和 defs.txt 檔案描述了 DDAR 用於進行推論的基礎2。然而，在 AlphaGeometry 的推理迴圈期間（見上文），可能會觸發這些文字檔案中未明確說明但已硬編碼的不同規則，請參閱第 3.4.3 節。

**程式設計師友好性問題：**AlphaGeometry 的程式碼庫不是模組化構建的，這使得想要貢獻程式碼以新增功能、檢查證明軌跡、新增日誌等的程式設計師難以進行。此外，LLM 是在 Meliad 中實作的，Meliad 是一個未被廣泛使用的深度學習 Python 庫，這使得微調 LLM 或理解其內部工作原理以及其他理想操作變得更加困難。
**問題範圍問題：**AlphaGeometry 無法處理相當簡單和基本的定理，尤其是畢氏定理，缺乏對線段長度概念的支援，而線段長度概念在其他方面用於初等幾何課程。這使得 AlphaGeometry 成為一種狹義的 AI 系統，其智慧與人類智慧形成對比：無法想像一個 IMO 級別的競爭者能夠解決某些 IMO 級別的幾何問題，卻無法使用畢氏定理。與任意平面幾何相比，AlphaGeometry 在奧林匹克幾何問題上“過度擬合”。

從以下內容提煉的關鍵洞見

Newclid: A User-Friendly Replacement for AlphaGeometry

by Vlad... 於 arxiv.org 11-20-2024

https://arxiv.org/pdf/2411.11938.pdf

深入探究

除了提高使用者友好性之外，Newclid 在解決幾何問題方面是否比 AlphaGeometry 有顯著的性能提升？

Newclid 在解決幾何問題的能力上相較於 AlphaGeometry 確實取得了一定的提升，但並非是顯著的提升。文章中提到，Newclid 主要着力於改進 AlphaGeometry 的 DDAR 解題器，使其更易於使用和擴展，並修復了一些錯誤。具體來說：

解決問題範圍擴大: Newclid 能夠處理一些 AlphaGeometry 無法處理的基本定理和概念，例如畢氏定理、線段長度等，使其在處理平面幾何問題上更具普適性。
修復錯誤並提高可重複性: Newclid 修復了 AlphaGeometry 中的一些錯誤，並提高了其可重複性，使得研究者能夠更方便地在其基礎上進行研究和開發。
在 AG-30 數據集上的表現: Newclid 的 DDARN 解題器在 breadth-first-search 模式下，能夠解決 AlphaGeometry 無法解決的五道 AG-30 數據集問題中的一道 (IMO 2008 P1B)。
然而，文章也明確指出，Newclid 的改進主要集中在 DDAR 解題器上，而並未對深度學習模型 (LLM) 進行顯著改進。考慮到 LLM 在 AlphaGeometry 解題過程中扮演的重要角色，Newclid 在解決問題的能力上的提升相對有限。
總體而言，Newclid 相較於 AlphaGeometry 在解決問題的能力上有所提升，但並非革命性的突破。其主要貢獻在於提高了使用者友好性和代碼可維護性，為構建更強大、更通用的幾何解題器奠定了基礎。

如果 Newclid 的推理引擎完全基於公理系統，而不是依賴於預先定義的定理列表，它是否能夠解決更多種類的幾何問題？

如果 Newclid 的推理引擎完全基於公理系統，它在理論上可以解決更多種類的幾何問題，甚至有可能發現新的定理。這是因為：

完備性: 公理系統力求完備，即所有真命題都可以從公理出發，通過邏輯推理得到證明。这意味着，只要问题在该公理体系下是可解的，Newclid 就有能力找到解决方案。
可擴展性: 基於公理系統的推理引擎可以更容易地引入新的公理和定義，從而擴展其解決問題的範圍。
然而，完全基於公理系統的推理引擎也面临着一些挑战：

效率: 從公理出發进行推理的搜索空间通常非常庞大，会导致解题效率低下。Newclid 目前使用的预定义定理列表可以看作是一种优化策略，缩小了搜索空间，提高了效率。
公理選擇: 构建一个完备且一致的公理系统并非易事。不同的公理选择可能会导致不同的推理能力和效率。
因此，Newclid 若要完全采用基于公理系统的推理引擎，需要解决效率和公理选择方面的挑战。一种可能的方案是，结合预定义定理和公理推理，在保证效率的前提下，逐步提高推理引擎的完备性和普适性。

Newclid 的開發對於自動定理證明領域的未來研究有何啟示？它是否為構建更強大、更通用的幾何求解器鋪平了道路？

Newclid 的開發對於自動定理證明領域，特別是幾何解題器方向的未來研究具有以下啟示：

使用者友好性與可擴展性: Newclid 的开发表明，使用者友好性和代码可扩展性对于自动定理证明工具的推广和应用至关重要。未来的研究应该更加重视这些方面，降低使用门槛，方便研究者进行改进和扩展。
结合符号推理和深度学习: Newclid 继承了 AlphaGeometry 结合符号推理 (DDAR) 和深度学习 (LLM) 的思路，并在此基础上进行了改进。这表明，将两种方法的优势结合起来是构建强大且通用的几何求解器的有效途径。
探索新的推理机制: Newclid 目前主要依赖于预定义的定理列表进行推理。未来的研究可以探索更加灵活和强大的推理机制，例如基于公理系统的推理、基于案例的推理等。
构建更丰富的知识库: Newclid 的解题能力很大程度上依赖于其内部的规则和定义库。未来的研究可以致力于构建更加丰富和完善的几何知识库，涵盖更广泛的几何概念、定理和解题技巧。
总而言之，Newclid 的开发为构建更强大、更通用的几何求解器指明了方向。未来的研究可以借鉴其设计理念和技术路线，并结合其他人工智能技术，推动自动定理证明领域的发展。