形式化证明迈向多模态，MLLM正确率仅4%！港科大等推出全新基准
香港科技大学推出MATP-BENCH基准测试集，评估多模态大模型在处理包含图像和文本的几何定理证明中的能力。实验发现尽管模型在将图文信息转化为形式化定理方面有一定能力，在构建完整证明时面临复杂逻辑推理和辅助线构造等重大挑战。
Lean 4
DeepSeek最新推出Prover-V2模型，专为形式化定理证明而设计
DeepSeek发布新模型DeepSeek-Prover-V2，专为形式化定理证明设计，在神经定理证明方面取得领先性能，并提出多项创新实验提升模型能力。
DeepSeek Prover-V2，这才是探索AGI 的正确姿势！
DeepSeek 推出新模型 DeepSeek-Prover-V2-671B，专为数学定理证明打造。该模型参数量大（671亿），架构使用MoE技术，隐藏维度高达7168，支持超长上下文窗口（约80万汉字）。通过Lean 4生态训练，并结合生成自然语言讲解与强化学习提升性能。