跳到正文
研踪PaperTrail

论文库

检索计算机领域论文，按研究方向、作者或关键词筛选。

部分采集异常
正在读取账号与研究记录…

全站更新概况

+0新增论文
+0其中 AI 相关
+2已有论文修订
+100新增 AI 导读

arXiv 最近完成扫描：2026-11-15 00:32 · 全站最近入库：2026-11-14 15:09各信源进度 →

统计口径与数据新鲜度

统计 2026-11-14 01:01 — 2026-11-15 01:01（北京时间） · 点击数字查看对应简报；AI 相关包含在新增论文内。

最近完成检查：2026-11-15 00:32最近发现新增版本：2026-11-14 15:09库内论文最新更新时间：2026-11-13 02:59

每分钟刷新已保存的数据。空检查不代表采集异常；新收录可能包含历史论文。AI 导读按新增版本计数。

23,348 已收录论文19,580 AI 相关6,729 有修订112 HF 社区发现

浏览论文库

研究日报 / 周报 →按信源浏览 →

时间范围跟随排序：版本更新、本站收录或首次发表。最新收录可能包含历史论文。部分信源异常，查看状态 →

找到 4 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-15 00:30（北京时间）
版本更新 · v3arXiv:2606.03303

LEAP：用智能体框架为形式数学增强大语言模型

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart 等 13 位作者

AI 速读 基于摘要

LEAP 是一个智能体框架，让通用基础模型通过与 Lean 编译器持续交互，把非形式化推理转化为可机械验证的形式化证明，并在 2025 年 Putnam 竞赛与自建 Lean-IMO-Bench 上取得作者报告的高求解率。

cs.AI

arXiv ↗PDF ↗
查看原文摘要

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.

首次观测 · 记录 #1ACL Anthology · ACL 2026:acl:2026.acl-long.178ACL Anthology · ACL 2026

Crossing the Reward Bridge: Expanding Reinforcement Learning with Verifiable Rewards Across Diverse Domains

Yi Su, Dian Yu Tencent AI Lab, Linfeng Song Google, Juntao Li, Haitao Mi Tencent AI Lab, Zhaopeng Tu Tencent, Min Zhang Harbin Institute of Technology, Shenzhen and Harbin Institute of Technology, Dong Yu CapitalOne

原文摘要

Reinforcement learning with verifiable rewards (RLVR) has been effective on tasks with structured solutions like math and coding, but its reliance on simple, rule-based verifiers creates a fundamental bottleneck. We find their applicability is surprisingly narrow even in structured domains, a limitation that is compounded at scale: rule-based systems can paradoxically degrade in performance as multi-domain, free-form training data increases. To overcome these challenges, we propose a new RLVR framework that uses a generative verifier to provide soft, probabilistic rewards. Our key insight is that powerful LLMs show high agreement with human evaluators when judging answer correctness given a ground-truth reference, allowing us to automate reward generation without costly human annotation. Our experiments demonstrate the effectiveness of this approach. We show that a compact 7B generative reward model can guide a 7B policy model to decisively outperform models up to 10x its size, including the 72B Qwen2.5-Instruct (by a margin of +8.6%). This effectiveness is robust, holding true across diverse training datasets with answers sourced from experts, web users, and other LLMs, and generalizes strongly to seven out-of-distribution benchmarks. Our work provides a scalable and effective framework for extending RLVR beyond the limitations of pattern-based verification to complex, noisy, real-world domains.

cs.CL

Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · 2026 · 正式发表

首次观测 · 记录 #1ACL Anthology · ACL 2026:acl:2026.acl-long.2121ACL Anthology · ACL 2026

EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving

Mukai Li, Linfeng Song Google, Zhenwen Liang Tencent AI Lab, Jiahao Xu Tencent AI Lab, Shansan Gong, Qi Liu University of Hong Kong, Haitao Mi Tencent AI Lab, Dong Yu CapitalOne

原文摘要

Large Language Models (LLMs) have recently advanced the field of Automated Theorem Proving (ATP), attaining substantial performance gains through widely adopted test-time scaling strategies, notably reflective Chain-of-Thought (CoT) reasoning and increased sampling passes. However, they both introduce significant computational overhead for inference. Moreover, existing cost analyses typically regulate only the number of sampling passes, while neglecting the substantial disparities in sampling costs introduced by different scaling strategies. In this paper, we systematically compare the efficiency of different test-time scaling strategies for ATP models and demonstrate the inefficiency of the current state-of-the-art (SOTA) open-source approaches. We then investigate approaches to significantly reduce token usage and sample passes while maintaining the original performance. Specifically, we propose two complementary methods that can be integrated into a unified EconRL pipeline for amplified benefits: (1) a dynamic Chain-of-Thought (CoT) switching mechanism designed to mitigate unnecessary token consumption, and (2) Diverse parallel-scaled reinforcement learning (RL) with trainable prefixes to enhance pass rates under constrained sampling passes. Experiments on miniF2F and ProofNet demonstrate that our EconProver-GD achieves comparable performance to baseline methods with only 12% of the computational cost. This work provides actionable insights for deploying lightweight ATP models without sacrificing performance.

cs.CL

Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · 2026 · 正式发表

首次观测 · 记录 #1ACL Anthology · ACL 2026:acl:2026.acl-long.788ACL Anthology · ACL 2026

Your Reasoning Model is Secretly a Reward Model - Optimization-Free Verification from Experience

Zhenwen Liang Tencent AI Lab, Ruosen Li University of Texas at Dallas, Yujun Zhou University of Notre Dame, Linfeng Song Google, Dian Yu Tencent AI Lab, Xinya Du University of Texas at Dallas, Haitao Mi Tencent AI Lab, Dong Yu CapitalOne

原文摘要

Assessing the quality of Large Language Model (LLM) outputs becomes especially challenging in high-branching settings, where a single prompt yields many plausible candidates. Existing verifiers typically operate on the surface text (e.g., reward models, LLM judges, majority voting) or on confidence proxies derived from token probabilities, both of which can be brittle: the former can be influenced by stylistic artifacts, while the latter is often miscalibrated. In this paper, we study a third source of information—the model’s hidden states—for binary correctness verification in tasks with a reliable success/failure signal (e.g., deterministic checkers or reference-grounded answers). We find that correct and incorrect solutions exhibit measurable geometric differences in their hidden-state trajectories. To isolate this signal with minimal modeling assumptions, we introduce Clue (Clustering and Experience-based Verification), a training-free, non-parametric verifier. Clue summarizes each reasoning trace by an activation delta—the difference between hidden states at the start and end of the explicit reasoning span—and predicts correctness by comparing this delta to two class centroids computed from labeled experience. Across math (AIME 24/25), scientific QA (GPQA), and a multi-domain benchmark (WebInstruct-verified), Clue improves selection and reranking, with particularly strong gains on smaller or less-calibrated models. For example, on AIME 24 with a 1.5B model, Clue raises accuracy from 56.7% (majority@64) to 70.0% (top-maj@16).

cs.CL

Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · 2026 · 正式发表