ScholarPulse 日报 2026-07-15

2026-07-15 学术简报：2 篇。MCPEvol-Bench揭示了LLM代理在动态工具环境中的适应性缺陷，为评估代理适应性提供了新基准。

今日速览

序号	标题	来源	日期	主题	推荐等级
1	MCPEvol-Bench: Benchmarking LLM Agent Performance Across Dynamic Evolutions of MCP Servers	arXiv	2026-07-16	MCP	高
2	MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research	arXiv	2026-07-16	AI-Agent	高

重点论文与技术动态

1. MCPEvol-Bench: Benchmarking LLM Agent Performance Across Dynamic Evolutions of MCP Servers

来源：arXiv
日期：2026-07-16
作者/机构：Huanxi Liu, Kun Hu, Jiaqi Liao, Qiang Wang, Pengfei Qian, YuanZhao Zhai
主题标签：MCP, arXiv
推荐等级：高
分类：cs.AI, cs.SE

一句话结论

MCPEvol-Bench揭示了LLM代理在动态工具环境中的适应性缺陷，为评估代理适应性提供了新基准。

一段话：该基准通过11个突变算子模拟123个MCP服务器的工具演变，测试12个先进LLM，发现GPT-5.4和Claude-Sonnet-4-6性能分别下降13.7%和14.4%，伴随规划和推理错误显著增加，凸显LLM工作流的脆弱性。

核心内容

现有基准忽略MCP服务器工具接口和功能的持续演变，导致评估无法捕捉代理在变化工具环境中的适应能力。
MCPEvol-Bench基于大规模实证研究，提出11个突变算子模拟真实工具演变，用于评估LLM代理任务解决能力。
实验显示，前沿模型如GPT-5.4和Claude-Sonnet-4-6在演变工具下性能大幅下降，规划和推理错误增加。

方法与数据

提出11个突变算子模拟工具演变。
基准测试覆盖123个MCP服务器和12个状态领先LLM。

价值判断

值得关注：LLM驱动工作流在动态工具环境中的适应性缺陷。
可复用点：MCPEvol-Bench可作为标准基准评估代理适应性。
局限/待核查：摘要未明确。

摘要

As Model Context Protocol (MCP) servers emerge as the core infrastructure for connecting LLMs with external tools, existing benchmarks leverage real-world MCP servers to evaluate LLM agents' tool-using capabilities. However, these benchmarks overlook the continuous evolution of tool interfaces and functionalities within MCP servers, resulting in flawed assessments that fail to capture the agent's adaptability in changing tool landscapes. To bridge this gap, we introduce \textbf{MCPEvol-Bench}, a novel benchmark for evaluating the task-solving capabilities of LLM agents under dynamic toolset evolution. Inspired by large-scale empirical study, we propose 11 mutation operators to simulate realistic tool evolution within 123 MCP servers. We benchmark 12 state-of-the-art LLMs on multiple versions of MCP servers, revealing that even frontier models struggle to adapt to evolving tools. For instance, GPT-5.4 and Claude-Sonnet-4-6 exhibit performance declines of 13.7\% and 14.4\% in evolved MCP servers, respectively, accompanied by substantial increases in planning and reasoning errors. These findings highlight the vulnerability of LLM-driven workflows, establishing MCPEvol-Bench as a standard for evaluating agent adaptability in dynamic tool environments.

2. MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research

来源：arXiv
日期：2026-07-16
作者/机构：Junjie Zhang, Jiayu Liu, Wenbin Liu, Zhenya Huang, Doudou Wang, Yan Jiang
主题标签：AI-Agent, arXiv
推荐等级：高
分类：cs.AI

一句话结论

MathCoPilot实现了人-AI共生的数学研究新范式，但当前大型语言模型在领域特定定理上仍面临挑战。

一段话：该系统通过交互式工作台使数学家能直接指导AI进行形式化证明，实验表明模型在本科级问题上成功率高，但在需深度数学理解的PDE定理上表现不足。

核心内容

交互式工作台支持数学家通过可导航证明蓝图实时检查、指导和优化证明步骤。
自动化证明技能编排整合自适应知识库搜索和Lean集成的迭代验证机制。
主题驱动论文检索系统能自动将论文形式化到验证的Lean知识库。

方法与数据

系统性比较了Gemini 3.1 Pro、GPT-5.4和Claude Opus 4.7等四个SOTA LLMs。
在FormalMATH子集和两个真实PDE定理上评估了生成验证Lean 4证明及识别错误证明的能力。

价值判断

值得关注：人-AI共生范式为数学研究提供了新方向。
可复用点：交互式工作台和自动化证明框架可推广至其他形式化任务。
局限/待核查：当前模型在需深度数学理解的领域特定定理上成功率低。

摘要

Existing LLM-based theorem provers have achieved impressive results on formal mathematics benchmarks, yet they remain confined to acting as autonomous agents that prove a stated proposition. In this paper, we propose MathCoPilot, a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research, in which the mathematician steers the high-level mathematical direction while AI agents carry out the detailed formalization and proof work under continuous human guidance. MathCoPilot unifies three core capabilities: (1) an interactive workbench where the mathematician and AI agents collaborate through a living proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; (2) automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and (3) topic-driven paper retrieval and automated formalization into a verified Lean knowledge base. Using MathCoPilot, we systematically compare four state-of-the-art LLMs, including Gemini~3.1~Pro, GPT-5.4, and Claude~Opus~4.7, on a FormalMATH subset and on two real PDE theorems requiring deep domain expertise, evaluating their ability to produce verified Lean~4 proofs and to identify errors in deliberately incorrect proofs. Our results show that while current models can handle undergraduate-level problems with high success rates under favorable autoformalization conditions, substantial challenges remain for domain-specific theorems requiring genuine mathematical understanding.