ScholarPulse 日报 2026-11-09

2026-11-09 学术简报：2 篇。本文提出结合 Lean 证明器与大模型智能体团队的框架，实现了超越经典模拟尺度、经形式化验证的量子算法自动化发现。

今日速览

序号	标题	来源	日期	主题	推荐等级
1	Discovering formally verified quantum programs with AI	arXiv	2026-11-06	AI-Agent	高
2	Knowing When to Intervene: Causal Evaluation of AI Agents	arXiv	2026-11-06	RAG	高

重点论文与技术动态

1. Discovering formally verified quantum programs with AI

来源：arXiv
日期：2026-11-06
作者/机构：Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser
主题标签：AI-Agent, arXiv
推荐等级：高
分类：quant-ph, cs.AI, cs.PL

一句话结论

本文提出结合 Lean 证明器与大模型智能体团队的框架，实现了超越经典模拟尺度、经形式化验证的量子算法自动化发现。

核心内容

在 Lean 中构建程序库，由 LLM 智能体依据规范合成量子程序，并自动验证正确性与成本。
智能体团队通过 Wiki 沉淀知识并模拟学术会议，实现规模化人机协同。
性能超越基线：量子算术提升 290 倍，聚变、光化学与药物代谢模拟分别提升 11、8 与 2.5 倍，并行搜索提升达 1.4 倍。

方法与数据

基于 Lean 定理证明器与多智能体协同机制；具体测试数据集细节摘要未明确。

价值判断

值得关注：摆脱经典计算难以评估大规模量子程序的困境，在多项科学应用中实现数量级优化。
可复用点：定理证明器严谨约束下的多智能体“Wiki+研讨会”知识发现机制。
局限/待核查：合成效率、计算成本及对更广泛量子问题的泛化能力摘要未明确。

摘要

The timeline by which quantum computers can solve breakthrough problems in science depends on improved quantum algorithms as much as on better hardware. Such algorithmic advances are typically achieved through many years of expert human collaboration. In mathematics and computer science, large language models have accelerated progress through automated discovery loops. However, quantum algorithms can only be evaluated by classical computers on restricted or small instances. Here we demonstrate automated discovery of quantum programs beyond these regimes including order-of-magnitude improvements on scientific applications. To achieve this, we build a quantum program library in the Lean theorem prover in which large language model agents synthesize novel programs against formal problem specifications and verify their correctness and cost. Agent teams collaborate, sharing results and knowledge through wikis and discussing ideas at organized conferences. Our results improve on prior baselines for parallel search (up to 1.4x), quantum arithmetic (290x), and simulations relevant to fusion, photochemistry and drug-metabolism by 11x, 8x and 2.5x respectively. Combining human and artificial intelligence at scale, under the rigor of mathematical proof, lets researchers design algorithms that today's classical and quantum computers cannot test, shortening the path to practical quantum computation.

2. Knowing When to Intervene: Causal Evaluation of AI Agents

来源：arXiv
日期：2026-11-06
作者/机构：Ayush Sawarni, Wenqian Xing, Tijana Zrnic, Ramesh Johari, Vasilis Syrgkanis
主题标签：RAG, arXiv
推荐等级：高
分类：cs.AI, cs.LG, econ.EM, stat.ME

一句话结论

该研究提出了首个评估智能体轨迹中干预因果效应的理论框架，解决了部署期何时进行验证或纠偏等审计干预的决策难题。

核心内容

部署期决定何时介入干预本质是动态因果推断问题，其效果取决于当前上下文、环境及智能体未来行为。
该框架仅需少量包含随机干预的轨迹数据，即可有效估计丰富的上下文干预策略的动态因果效应。
实证发现干预效果在智能体动作与状态间差异显著；所估结构参数可构建安全排行榜，指导审计优先级。

方法与数据

基于包含验证或筛选等随机干预的小规模轨迹数据，在 tau-bench Retail、ToolSandbox 和 ImpossibleBench 上完成了评估验证。

价值判断

值得关注：开辟了因果推断与智能体评估相结合的新方向，为安全可靠部署提供了量化工具。
可复用点：基于干预因果效应构建智能体动作风险与审计优先级排行榜的方法。
局限/待核查：摘要未明确所需小规模数据集的具体样本量下限及因果估计的计算开销。

摘要

Current evaluations of agentic AI systems primarily rely on benchmarks. However, the static nature of benchmarks makes them uninformative about the value of auditing interventions at deployment time. For reliable deployment, we often need to determine within an agent's trajectory whether or not to intervene, e.g., by verifying the agent's current output or steering it toward different behavior, using either human review or more costly models or time-consuming agentic supervision. The value of such interventions is fundamentally a causal inference question, asking whether the causal effect of such an intervention is beneficial for the final outcome. Estimating this causal effect is particularly challenging due to the dynamic nature of the problem: the impact of an intervention depends on the current context and environment, as well as the agent's future behavior. We develop the first methodologically grounded framework for evaluating the causal effects of randomized interventions within agent trajectories. By leveraging a relatively small dataset of agent trajectories collected under randomized interventions such as verification or screening, we can estimate the dynamic causal effect of a rich class of (contextual) intervention policies. The structural parameters that we estimate can also be used to construct safety leaderboards that capture the risk of various agentic actions, which can be used by practitioners for audit prioritization. Applying our methods to tau-bench Retail, ToolSandbox, and ImpossibleBench, we find that intervention effects vary substantially across agent actions and states. More broadly, our work suggests a rich research agenda at the intersection of causal inference and agentic evaluation, which we believe is essential for the reliable and safe deployment of AI agents in the real world.