AI模型首次挑战“First Proof”数学难题：实验与初步成果

我们团队近期在“First Proof”数学挑战赛中提交了首个自动证明尝试，旨在评估大语言模型（LLM）在专家级数学推理上的潜力。该挑战要求模型在限定时间内给出完整、形式化的证明，涉及高等代数、拓扑与数论等领域的深度概念。

实验设置

• 模型：基于最新的 Transformer‑XL 架构，微调自 GPT‑4‑Turbo，参数量约 175B。
• 数据：使用公开的数学论文语料库（约 2.3TB）进行预训练，再加入 10k 条手工标注的定理‑证明对进行指令微调。
• 推理框架：采用链式思考（Chain‑of‑Thought）提示，配合自检模块（self‑verification）在每一步生成后自动校验逻辑一致性。

核心代码片段

# 拉取实验代码
git clone https://github.com/ai-research/first-proof-demo.git
cd first-proof-demo
# 安装依赖
pip install -r requirements.txt
# 运行单条定理的自动证明
python run_proof.py --theorem "Every compact metric space is complete" 

实验结果

• 成功生成了 3 条形式化证明草稿，其中 1 条在 Coq 环境下通过了基本的类型检查。
• 其余 2 条在逻辑细节上出现了遗漏，主要集中在隐含假设的未显式声明。
• 与人类专家的平均解题时间（约 45 分钟）相比，模型完成草稿的耗时约为 7 分钟。

挑战与展望

1. 逻辑严谨性：当前的自检模块仍难以捕捉跨步的隐式假设，需要更强的形式化语义解析。
2. 可解释性：链式思考提示虽提升了可追溯性，但生成的中间步骤仍存在语言歧义。
3. 跨领域迁移：模型在代数类定理上表现相对稳健，拓扑与数论的高阶概念仍是瓶颈。

我们计划在后续工作中引入基于交互式定理证明器（如 Lean、Isabelle）的闭环反馈，以提升模型的形式化能力并缩小与人类专家的差距。