使用 Opus 4.6 和 Rocq-MCP 在 Putnam 2025 中求解问题
机器学习
2026-05-22 v2 计算与语言
计算机科学中的逻辑
摘要
我们报告了一项实验，其中Claude Opus 4.6配备了为Rocq证明助手设计的模型上下文协议（MCP）工具套件，自主地证明了2025年Putnam数学竞赛的10道问题。MCP工具的设计是基于对miniF2F-Rocq先前实验日志的分析，编码了“编译-交互式后备”策略。该代理在无互联网访问的隔离虚拟机上部署，激活计算时间为17.7小时（51.6小时墙钟时间），消耗约19亿个token。所有证明均公开可用。
引用
@article{arxiv.2603.20405,
title = {Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP},
author = {Guillaume Baudart and Marc Lelarge and Tristan Stérin and Jules Viennot},
journal= {arXiv preprint arXiv:2603.20405},
year = {2026}
}