Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration
作者: Ting Gong, Michael Ruofan Zeng, Yong Yang
分类: cs.AI, cs.LG
发布日期: 2026-07-30
备注: 7 pages, comments welcome!
💡 一句话要点
提出Albilich以解决数学研究中的长远证明协调问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 数学研究 计算机代数系统 长远推理 文献检索 AI辅助 开放源代码 上下文管理
📋 核心要点
- 现有方法在长时间的数学证明协调、评估和重现方面存在显著挑战，限制了AI在数学研究中的应用。
- Albilich通过结合长远推理、计算机代数系统和文献检索，提供了一种新的自研究框架，旨在提高数学研究的效率和可操作性。
- 在实验中，Albilich在RealMath基准上实现了10/10的成功率，且在Kourovka问题中产生了重要的反例和证明，显示出其强大的能力。
📝 摘要（中文）
大型语言模型可以为数学研究提供有价值的思路，但长时间的证明尝试仍然难以协调、评估和重现。我们提出了Albilich，这是一个开源的代理框架，旨在数学自研究中结合长远推理、计算机代数系统（CAS）、文献检索和持久的SQLite上下文管理。我们在RealMath基准和Kourovka Notebook中的群论开放问题上评估了Albilich，结果显示其在RealMath上解决了10个问题（使用CAS）和9个问题（不使用CAS），并在Kourovka问题中产生了第21.142题的反例和第20.2题的加强证明。这些结果支持Albilich作为一个可由人类引导、增强的CAS环境，以实现可扩展的AI辅助数学研究。
🔬 方法详解
问题定义：本论文旨在解决大型语言模型在数学研究中进行长远证明时的协调、评估和重现困难。现有方法往往无法有效管理复杂的推理过程，导致研究效率低下。
核心思路：Albilich的核心思路是构建一个集成了计算机代数系统（CAS）和文献检索的开放式代理框架，允许用户在数学研究中进行长时间的推理和验证。通过这种设计，用户可以更好地管理和利用上下文信息。
技术框架：Albilich的整体架构包括多个模块：长远推理模块、CAS集成模块、文献检索模块和SQLite上下文管理模块。用户可以通过这些模块进行高效的数学研究，系统会自动协调各个模块的工作。
关键创新：Albilich的主要创新在于其人类可引导的特性和CAS增强的能力，使得AI在数学研究中的应用更加灵活和高效。这与传统方法的被动推理方式形成鲜明对比。
关键设计：在设计中，Albilich使用了持久的SQLite数据库来管理上下文信息，确保在长时间推理中信息的可追溯性。同时，CAS的启用显著减少了所需的token数量，提升了推理效率。
🖼️ 关键图片
📊 实验亮点
在实验中，Albilich在RealMath基准上成功解决了10个问题，且在不使用CAS的情况下也能解决9个问题。此外，在Kourovka问题中，Albilich成功产生了第21.142题的反例和第20.2题的加强证明，显示出其强大的推理能力。CAS的启用使得token数量减少了32.0%，显著提升了推理效率。
🎯 应用场景
Albilich的研究成果在数学研究、教育和科学探索等领域具有广泛的应用潜力。通过提供一个高效的AI辅助环境，研究人员可以更快地解决复杂的数学问题，推动数学理论的发展。此外，该框架还可以用于教育领域，帮助学生理解复杂的数学概念。
📄 摘要（原文）
Large language models can contribute useful ideas to mathematical research, yet long-horizon proof attempts remain difficult to coordinate, evaluate, and reproduce. We present Albilich, an open-source agentic harness for autoresearch in mathematics that combines long-horizon reasoning, computer algebra systems (CAS), literature retrieval, and persistent SQLite-based context management. We evaluate Albilich on the RealMath benchmark (Zhang et al. 2025) and on open problems in group theory from the Kourovka Notebook (Khukhro and Mazurov 2026). It solved 10/10 problems on RealMath with CAS and 9/10 with no CAS. On the Kourovka problems, Albilich produced a counterexample to Problem 21.142 and a proof of a strengthening of Problem20.2. Anablation on Problem 17.91 demonstrates 32.0% token reduction when CAS is enabled. An ablation on Problem 21.142 demonstrates higher verifier-rejection rate and failure to synthesize proof routes in the absence of the advisor agent. These results support Albilich as a human-steerable, CAS-boosted environment for scalable AI-assisted mathematical research.