Albilich：面向LLM数学研究的可操控证明状态编排与CAS集成

摘要

大语言模型能为数学研究贡献有用想法，但长程证明尝试在协调、评估与复现上仍然困难。我们提出Albilich，一个用于数学自动研究的开源智能体框架，它结合了长程推理、计算机代数系统（CAS）、文献检索以及基于SQLite的持久上下文管理。我们在RealMath基准（Zhang et al. 2025）以及Kourovka Notebook（Khukhro and Mazurov 2026）中的群论开放问题上评估Albilich。在RealMath上，它启用CAS时解决10/10道题，不使用CAS时解决9/10道。在Kourovka问题上，Albilich给出了Problem 21.142的一个反例，以及Problem 20.2一个加强命题的证明。对Problem 17.91的消融实验显示，启用CAS时token减少32.0%。对Problem 21.142的消融实验表明，缺少advisor智能体时验证器拒绝率更高，且无法综合出证明路径。这些结果支持将Albilich作为可由人类操控、由CAS增强的可扩展AI辅助数学研究环境。