日期: 2025 年 5 月 7 日

挑战AI数学推理极限！大规模形式化数学基准FormalMATH发布，最强模型成功率仅16%

作者

香港中文大学等机构联合推出FormalMATH基准测试，包含5560道经过验证的数学题。尽管大语言模型在自然语言处理和代码生成领域表现优异，但在数学定理证明任务中成功率仅为16.46%。研究提出了一套三阶段过滤框架用于自动形式化和语义一致性检测，并分析了现有LLM证明器的表现，发现代数较强而微积分较弱，存在滥用自动化策略的问题。

ICML 2025 视频生成模型无损加速两倍，秘诀竟然是「抓住attention的时空稀疏性」

作者

Sparse VideoGen 提出了一种无需重新训练模型的方法来加速视频生成过程。通过挖掘注意力机制中的空间与时间稀疏性，该方法成功将推理时间减半，并保持了接近原模型的视觉质量。