标签
AdvancedMathBench是一个新的基准套件，用于评估大语言模型在高级数学证明生成与验证方面的性能。它包含用于生成的ProverBench和用于验证的VerifierBench，表明当前模型如GPT-5.5-xhigh仅取得了有限的性能。
来自牛津、剑桥、MIT、CMU等机构的研究人员开展了一项混合方法研究，考察人们如何将AI工具融入数学证明形式化工作流程。研究发现，借助AI辅助时，参与者的形式化准确率普遍更高，同时他们倾向于在证明发现过程中保持人类对高层决策的主导权。
Research Math Agents (RMA) 是一个用于研究级数学问题自动推理的智能体框架，在 First Proof 基准测试中取得最先进结果，解决了10个问题中的8个，优于 GPT-5.2R 和 Aletheia 等强基线。
ProofGrid是一个基准测试套件，通过使用极小形式化符号的机器可验证证明来评估LLM推理，包含证明编写、检查与补全任务，揭示了进展与尚存局限，包括认知不稳定性。