Fugu-MT 論文翻訳(概要): Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP

論文の概要: 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問題
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億のトークンを消費した。すべての証明が公開されている。

関連論文リスト

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。 Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
論文参考訳（メタデータ） (2026-06-04T17:54:44Z)
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文参考訳（メタデータ） (2026-06-03T20:09:39Z)
How Reliable Are AI Attackers Against a Fixed Vulnerable Target? A 400-Run Empirical Study of LLM Penetration Testing Consistency [0.0]
大規模言語モデル(LLM)は、多段階のサイバー攻撃を自律的に行うことができるが、その攻撃行動の一貫性は調査されていない。この研究は、Juice Shopをホストする同一のハニーポットに対して400ラン(4モデル、100台)の攻撃一貫性を実証した最初の大規模な実験的な測定結果を示す。オーケストレータのワンショットの承認が0-1で再発効したコンテントの拒絶は、モデルでは発生しなかった。
論文参考訳（メタデータ） (2026-05-28T15:39:43Z)
The Range Shrinks, the Threat Remains: Re-evaluating LLM Package Hallucinations on the 2026 Frontier-Model Cohort [51.56484100374058]
Spracklenらは、コード生成された大きな言語モデルは、PyPIやnpmに存在しないパッケージ名を幻覚させることを示した。 199,845対のPythonとJavaScriptプロンプトの幻覚率を測定し、PyPIとnpmマスターリストに対して検証した。 127個のパッケージ名(PyPIは109個,npmは18個)を5つの評価モデルで同一に作成する。
論文参考訳（メタデータ） (2026-05-16T16:08:52Z)
ZAYA1-8B Technical Report [14.894881882111605]
700Mのアクティブパラメータと8Bの合計パラメータを混合したMoEモデルであるZAYA1-8Bを提案する。 ZAYA1-8BはDeepSeek-R1-0528といくつかの挑戦的な数学とコーディングのベンチマークで一致または超える。ポストトレーニングでは、数学とパズルのウォームアップを推論する4段階のRLカスケード、400タスクのRLVE-Gymカリキュラム、テストタイムの計算トレースと合成コード環境を備えた数学とコードRLを使用する。
論文参考訳（メタデータ） (2026-05-06T18:44:08Z)
MCP Pitfall Lab: Exposing Developer Pitfalls in MCP Tool Server Security under Multi-Vector Attacks [0.7305019142196584]
MCP Pitfall Labは,開発者の落とし穴を再現可能なシナリオとして運用するプロトコル対応のセキュリティテストフレームワークである。 Pitfall Labは,現実的なマルチベクタ条件下でのMPPツールサーバの実用的,エンドツーエンド評価と強化を可能にする。
論文参考訳（メタデータ） (2026-04-23T09:39:15Z)
Assessing REST API Test Generation Strategies with Log Coverage [18.116037423912257]
我々は、Light-OAuth2認証マイクロサービスシステム上で、3つのREST APIテスト生成戦略、進化型コンピューティング(EvoMaster v5.0.2)、LSM(Claude Opus 4.6およびGPT-5.2-Codex)、人手によるローカスト負荷テストを経験的に評価した。平均して、Claude Opus 4.6テストでは、人間によるテストよりも28.4%、EvoMasterとGPT-5.2-Codexは26.1%、38.6%減少している。
論文参考訳（メタデータ） (2026-04-08T13:26:04Z)
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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。