論文の概要: Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
- arxiv url: http://arxiv.org/abs/2603.20405v1
- Date: Fri, 20 Mar 2026 18:25:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-24 19:11:38.893467
- Title: Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
- Title（参考訳）: Opus 4.6とRocq-MCPを用いたRocqのPutnam 2025問題
- Authors: Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot,
- Abstract要約: 筆者らは,Rocq証明アシスタントのためのモデルコンテキストプロトコル(MCP)ツールセットを備えたClaude Opus4.6が,2025年パットナム数学コンペティション(Putnam Mathematical Competition)において,12の問題の内10を自律的に証明した実験について報告する。
インターネットアクセスのない隔離されたVM上で実行されるエージェントは、17.7時間にわたって141個のサブエージェントをデプロイし、約19億のトークンを消費した。
- 参考スコア（独自算出の注目度）: 6.089774484591286
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We report on an experiment in which Claude Opus~4.6, equipped with a suite of Model Context Protocol (MCP) tools for the Rocq proof assistant, autonomously proved 10 of 12 problems from the 2025 Putnam Mathematical Competition. The MCP tools, designed with Claude by analyzing logs from a prior experiment on miniF2F-Rocq, encode a "compile-first, interactive-fallback" strategy. Running on an isolated VM with no internet access, the agent deployed 141 subagents over 17.7 hours of active compute (51.6h wall-clock), consuming approximately 1.9 billion tokens. All proofs are publicly available.
- Abstract（参考訳）: 筆者らは,Rocq証明アシスタントのためのモデルコンテキストプロトコル(MCP)ツールセットを備えたClaude Opus~4.6を用いて,2025年のパットナム数学コンペティションにおいて,12の課題のうち10を自律的に証明した実験について報告する。
MCPツールは、miniF2F-Rocqの以前の実験からログを分析してClaudeで設計され、"コンパイルファーストでインタラクティブなフォールバック"戦略をエンコードしている。
エージェントは、インターネットアクセスのない隔離されたVM上で実行し、141個のサブエージェントを17.7時間のアクティブな計算時間 (51.6h Wall-clock) にデプロイし、約190億のトークンを消費した。
すべての証明が公開されている。
関連論文リスト
- ResearchGym: Evaluating Language Model Agents on Real-World AI Research [48.46915933681714]
我々は、エンドツーエンドの研究においてAIエージェントを評価するためのベンチマークおよび実行環境であるResearchGymを紹介する。
これを実現するために,ICML,ICLR,ACLの5つの口頭およびスポットライト論文を再利用した。
GPT-5を動力とするエージェントの制御評価において、我々は鋭い能力-信頼性ギャップを観察する。
論文 参考訳（メタデータ） (2026-02-16T19:00:03Z) - Model Context Protocol (MCP) at First Glance: Studying the Security and Maintainability of MCP Servers [16.794115541448758]
Anthropicは2024年後半にこのツールエコシステムを標準化するためにModel Context Protocol (MCP)を導入した。
採用にもかかわらず、MPPのAI駆動の非決定論的制御フローは、持続可能性、セキュリティ、保守性に対する新たなリスクをもたらす。
我々は1,899のオープンソースMPPサーバを評価し,その健全性,セキュリティ,保守性を評価した。
論文 参考訳（メタデータ） (2025-06-16T14:26:37Z) - Seed1.5-Thinking: Advancing Superb Reasoning Models with Reinforcement Learning [231.11339402237903]
反応前に思考を通して推論できるSeed1.5-Thinkingを紹介した。
Seed1.5-ThinkingはAIME 2024で86.7、Codeforcesで55.0、GPQAで77.3を達成した。
これは、STEMとコーディングにおいて優れた推論能力を示す。
論文 参考訳（メタデータ） (2025-04-10T17:10:51Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search [65.05674971652776]
代表的な証明法は、証明手法を戦術によって反復的に構築することであり、典型的には最優先の探索スキームに従う。
本稿では,評価モデルを用いて選好情報を抽出する直感的かつ効果的な手法を提案する。
2万日以上のCPUを持つ大規模なエキスパートイテレーションが、証明者と批判者をさらに微調整するために適用される。
論文 参考訳（メタデータ） (2024-10-21T07:18:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。