miniCTX：基于(长-)上下文的神经定理证明
人工智能
2025-03-05 v3 计算与语言
机器学习
摘要
现实世界的形式化定理证明往往依赖于丰富的上下文，包括定义、引理、注释、文件结构和其他信息。我们引入了miniCTX，用于测试模型在证明依赖训练期间未见过的新上下文的形式化数学定理方面的能力。miniCTX包含源自真实Lean项目和教科书的定理，每个定理关联的上下文可跨越数万tokens。模型被要求在获取定理代码库中代码（包含证明所需的上下文）的条件下证明定理。作为miniCTX的基线，我们测试了微调和提示方法，这些方法使定理证明依赖于前文上下文。两种方法均大幅优于仅依赖状态信息的传统方法。我们发现，这种利用上下文的能力并未被先前的基准（如miniF2F）所捕捉。除miniCTX外，我们还提供了ntp-toolkit，用于自动提取和标注定理证明数据，使得将新项目添加到miniCTX以确保训练期间上下文不被见到变得容易。miniCTX为神经定理证明器提供了具有挑战性和现实性的评估。
引用
@article{arxiv.2408.03350,
title = {miniCTX: Neural Theorem Proving with (Long-)Contexts},
author = {Jiewen Hu and Thomas Zhu and Sean Welleck},
journal= {arXiv preprint arXiv:2408.03350},
year = {2025}
}
备注
Project page: https://cmu-l3.github.io/minictx