自动定理证明的语义正确性评估：从编译成功到集成测试

研究团队提出T-Test评估框架，通过检查依赖后续定理的编译成功率衡量语义正确性，发现最先进模型在严格语义评估下准确率仅38.9%。该框架借鉴软件工程集成测试思路，为领域提供更严格的评估标准。

现有评估方法存在局限：词汇重叠度仅比较表面相似性，无法反映逻辑正确性；人工审查准确但成本高、难规模化。这种困境制约领域发展，导致开发者无法准确了解模型能力、研究者难以比较方法优劣。

从代码生成领域的测试驱动评估获得灵感，提出T-Test框架：生成的定理语义正确当且仅当其所有依赖的后续定理能成功编译。类比软件工程集成测试，强调定理在整个理论体系中的支撑作用，而非仅局部编译通过。

构建大规模基准数据集：来源于5个Lean4真实代码仓库，含2206个定理问题，每个平均配41个后续定理（自动提取）。实验显示：最先进模型编译成功率高，但T-Test评估下性能显著下降；Claude-Sonnet-4.5在理想条件下准确率仅38.9%；提供上下文可提升生成质量。

38.9%准确率揭示核心问题：形式化严谨性不足（逻辑漏洞或边界处理不当）、依赖关系理解有限（忽视全局一致性）、长程推理能力欠缺、训练数据多样性不足（边界案例覆盖少）。

需反思评估标准，采用语义正确性评估；客观认知模型能力，避免过度乐观；改进训练策略（关注语义正确、引入T-Test反馈）；优化人机协作（AI生成候选+人类验证修正）。

框架局限：计算成本高、依赖完备性假设（可能遗漏关键依赖）、错误定位困难。未来方向：开发高效近似评估方法、构建全面依赖分析工具、将框架整合到模型训练流程实现闭环优化。