几何自动推理：LLM与符号引擎的协同创新

1. 几何自动推理的现状与挑战

几何定理自动证明一直是人工智能领域最具挑战性的任务之一。在数学奥林匹克竞赛（IMO）中，几何题目往往需要创造性的辅助构造和复杂的多步证明，这对AI系统提出了极高的要求。传统方法如AlphaGeometry系列依赖专家模型和大规模合成数据（通常需要数亿训练样本），通过穷举搜索可能的证明路径来解决问题。这种范式虽然取得了不错的效果，但存在三个根本性局限：

1. 数据效率低下：需要合成海量训练数据（300M级别样本）
2. 泛化能力受限：专家模型难以适应题目类型的微小变化
3. 创造性不足：辅助构造的启发式规则过于刚性

关键观察：人类选手解决几何问题的核心能力在于通过"试探-验证-反思"的迭代过程逐步构建证明思路，而非依赖预设的构造规则。

2. InternGeometry系统架构设计

2.1 核心组件与工作流程

InternGeometry的创新之处在于将大语言模型(LLM)的推理能力与符号引擎的精确性相结合，构建了一个动态交互的证明系统。其核心工作流程分为四个阶段：

1. 自然语言推理阶段：LLM基于当前证明状态进行思维链(CoT)推理
2. 形式化动作生成：输出结构化动作（命题验证/辅助构造）
3. 符号引擎验证：InternGeometry-DDAR引擎执行形式化验证
4. 动态记忆更新：压缩存储关键历史信息指导后续探索

python复制# 典型交互流程示例
def geometric_reasoning(problem):
    memory = DynamicMemory()
    for step in range(MAX_STEPS):
        thought, action = llm_generate(problem, memory)
        feedback, engine_state = symbol_engine.execute(action)
        memory.update(thought, action, feedback)
        if problem_solved(engine_state):
            return construct_proof(memory)
    return None

2.2 动态记忆机制

长程推理面临的核心挑战是上下文窗口限制。InternGeometry通过动态记忆模块实现历史信息的智能压缩：

• 动作摘要：保留已尝试构造的拓扑结构
• 命题快照：记录已验证为真/假的关键命题
• 反馈压缩：仅保留最近轮次的完整反馈
• 探索引导：标记未成功的探索方向避免重复

这种设计使得系统能在200+轮交互中保持高效推理，相比固定窗口的Transformer模型有显著优势。

3. 复杂度提升强化学习(CBRL)

3.1 训练框架设计

传统强化学习在数学推理中面临稀疏奖励问题。CBRL通过渐进式难度提升解决了这一挑战：

1. 冷启动阶段：7K样本的监督微调(SFT)
2. 课程学习阶段：按证明步数定义问题复杂度κ
3. 动态调整策略：
   • 每轮评估模型在当前κ下的表现
   • 根据优势函数A(κ)调整难度阈值
   • 合成新批次训练数据保持最佳学习率

技术细节：优势函数计算采用标准化后的步级奖励，确保不同复杂度问题的可比性。

3.2 数据合成管道

高质量训练数据的合成是CBRL成功的关键：

1. 基础构造：随机生成几何图形与约束条件
2. 难度标注：使用DDAR引擎预计算证明步数
3. 复杂度控制：
   • 初级(κ<10)：单一定理应用
   • 中级(10≤κ<20)：组合定理应用
   • 高级(κ≥20)：需要创造性辅助构造

实验表明，这种数据合成方法仅需13K样本就能达到超越人类金牌选手的水平，数据效率是AlphaGeometry2的25,000倍。

4. 关键技术创新解析

4.1 拒绝采样策略

为避免长程推理中的动作退化问题（如重复输出），系统实现了多条件检查机制：

• 动作去重：禁止与历史动作相似度>90%的提议
• 类型平衡：连续5轮同类型动作触发强制切换
• 格式验证：确保DSL语法正确性
• 思考限制：单轮思考token不超过512

4.2 符号引擎增强

在开源Newclid系统基础上进行了三项关键改进：

1. 全局约束求解：处理多条件同时满足的点构造
2. 命题缓存：加速重复命题的验证
3. 不完全构造：支持部分条件的渐进验证

这些改进使单次交互延迟控制在200ms内，保障了长程推理的可行性。

5. 性能评估与案例分析

5.1 IMO基准测试结果

在2000-2024年50道IMO几何题测试中：

特别地，在2018年第6题中，系统发现了人类解答中未出现的创新构造：

1. 在AC上构造点T使∠BDA=∠TDC
2. 定义圆ABX与圆CDX的交点K
3. 利用等角共轭性质完成证明

5.2 长程推理的必要性

消融实验证明交互步数直接影响性能：

6. 实际应用中的经验总结

在部署InternGeometry过程中，我们积累了以下关键经验：

1. 温度参数调节：推理时temperature=0.9能平衡探索与利用
2. 早期停止策略：连续20轮无进展时触发构造重置
3. 记忆压缩阈值：保留top-20最关键命题效果最佳
4. 复杂度跃迁：当成功率>80%时κ提升幅度应≤25%

一个典型的失败案例是2006年第1题，因涉及非纯几何计算超出DDAR表达能力。这提示我们未来需要增强符号引擎的代数处理能力。

7. 扩展应用方向

该方法论可推广至其他需要长程推理的领域：

1. 数学证明：数论、组合数学的自动证明
2. 程序验证：复杂程序正确性验证
3. 物理推导：理论物理中的符号计算
4. 教育应用：个性化数学辅导系统

当前限制主要来自符号引擎的表达能力，未来结合更强大的形式化验证工具可进一步扩展应用边界。