大模型推理能力

Code-QA-Bench: Separating Code Reasoning from Documentation Memorization in Repository-Level QA

Code-QA-Bench：在仓库级问答中分离代码推理与文档记忆

Jun Zhang, JianYing Qu, Hanwen Du, Zhongkai Sun, Yehua Yang, Qiao Zhao

机构 * Baidu Inc（百度公司） 纠错

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.AI

AI总结 提出Code-QA-Bench框架，通过答案优先生成和三条件实验设计，自动构建仓库级代码理解基准，以区分代码推理、文档回忆和预训练记忆的影响。

Taint-Style Vulnerability Detection and Confirmation for Node.js Packages Using LLM Agent Reasoning

基于LLM代理推理的Node.js包污点式漏洞检测与验证

Ronghao Ni, Mihai Christodorescu, Limin Jia

机构 * Carnegie Mellon University（卡内基梅隆大学） ； Google（谷歌） 纠错

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.AI

AI总结 本文提出LLMVD.js，通过LLM代理实现Node.js包的污点式漏洞检测与验证，有效率达84%，优于传统方法，无需注解或报告。

Comments 19 pages, 6 figures

Designing Adaptive Digital Nudging Systems with LLM-Driven Reasoning

基于LLM驱动推理的自适应数字引导系统设计

Tiziano Santilli, Mina Alipour, Mahyar Tourchi Moghaddam

机构 * Syddansk Universitet（南丹麦大学） 纠错

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.AI

AI总结 本文提出一种将行为科学与软件设计结合的自适应数字引导系统架构，通过整合多维用户建模与伦理合规，验证了其在住宅能源可持续性中的可行性。

Reliable Use of Lemmas via Eligibility Reasoning and Section$-$Aware Reinforcement Learning

通过资格推理和面向节段的强化学习可靠地使用引理

Zhikun Xu, Xiaodong Yu, Ben Zhou, Jiang Liu, Jialian Wu, Ze Wang, Ximeng Sun, Hao Chen, Zicheng Liu

机构 * Arizona State University（亚利桑那州立大学） ； Advanced Micro Devices, Inc.（先进微器件公司） 纠错

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.CL

AI总结 通过资格推理和面向节段的强化学习提升LLM在数学引理应用的可靠性与鲁棒性

Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification

连接大语言模型规划代理与形式方法：计划验证的案例研究

Keshav Ramani, Vali Tawosi, Salwa Alamir, Daniel Borrajo

机构 * J.P. Morgan AI Research（摩根大通人工智能研究） 纠错

专题命中 代码与定理证明 ：planning(title)；分类 cs.AI

AI总结 本文提出一种利用大语言模型将自然语言计划转换为形式化逻辑并进行验证的框架，展示了GPT-5在计划验证中的高准确率及形式化表示的生成能力。

Comments Accepted to AgenticSE Workshop at ASE 2025

Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification

Jacqueline Mitchell, Yasser Shaaban

机构 * University of Southern California（南加州大学） 纠错

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.LG

Comments 7 pages, 3 figures, In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL'25), October 12-18, 2025, Singapore, Singapore. ACM, New York, NY, USA

Mind the Gap: Evaluating the Representativeness of Quantitative Medical Language Reasoning LLM Benchmarks for African Disease Burdens

Fred Mutisya, Shikoh Gitau, Christine Syovata, Diana Oigara, Ibrahim Matende, Muna Aden, Munira Ali, Ryan Nyotu, Diana Marion, Job Nyangena, Nasubo Ongoma, Keith Mbae, Elizabeth Wamicha, Eric Mibuari, Jean Philbert Nsengemana, Talkmore Chidede

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.AI

Comments Preprint. 26 pages, includes appendix and tables

A Formal Framework for Reasoning about Agents' Independence in Self-organizing Multi-agent Systems

Jieting Luo, Beishui Liao, John-Jules Meyer

专题命中 代码与定理证明 ：reasoning(title)；分类 cs.AI

LAMP: Lean-based Agentic framework with MCP and Proof Repair

LAMP: 基于 Lean 的 MCP 与证明修复智能体框架

Santhana Srinivasan R, Maithilee Patawar

机构 * Indian Institute of Information Technology, Design and Manufacturing, Kancheepuram（印度信息与设计制造理工学院，卡纳切普拉姆） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；verifier(abstract)；分类 cs.CL、cs.AI

AI总结 提出 LAMP 多智能体框架，通过推理时提供结构化领域知识（本体）而非微调，在 Lean 4 中合成内核验证的证明，在组合学词领域定理上达到 96.7% 的验证率。

Why We Need World Models for AGI: Where LLMs Fail and How World Models May Outperform

为什么我们需要世界模型来实现通用人工智能：大语言模型失败之处以及世界模型如何可能超越

Feisal Alaswad, Batoul Aljaddouh, Maher Alrahhal, Poovammal E, Talal Bonny

机构 * Department of Computing Technologies（计算技术系） ； SRM Institute of Science and Technology（SRM科学与技术学院） ； Bio-Sensing and Bio-Sensors Group（生物传感与生物传感器组） ； Smart Automation and Communication Technologies Research Institute of Sciences and Engineering（科学与工程智能自动化与通信技术研究所） ； University of Sharjah, UAE（阿联酋沙迦大学） ； Department of Computer Engineering（计算机工程系） ； College of Computing and Informatics（计算与信息学院） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.CL、cs.AI

AI总结 本文通过提出潜在动态推理（LDI）概念和Flux环境案例研究，论证了大语言模型在因果推理、状态跟踪和长程规划上的局限性，并展示基于显式状态空间的强化学习智能体在长程游戏中显著优于纯文本LLM。

Comments 19 pages, 5 figures

AgentSOC: A Multi-Layer Agentic AI Framework for Security Operations Automation

AgentSOC: 一种多层代理AI框架用于安全运营自动化

Joyjit Roy, Samaresh Kumar Singh

机构 * IEEE 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.CL、cs.AI

AI总结 AgentSOC通过整合感知、前瞻性推理和基于风险的行动规划，提升安全运营中心自动化水平，实现警报标准化、上下文丰富化及安全响应合规性。

Comments 7 pages, 6 figures, 2 tables. Peer-reviewed paper published in IEEE ICAIC 2026 (IEEE Xplore)

Journal ref 2026 IEEE 5th International Conference on AI in Cybersecurity (ICAIC), Houston, TX, USA, 2026

TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving

TrustGeoGen: 用于可信多模态几何问题求解的正式验证数据引擎

Daocheng Fu, Jianlong Chen, Renqiu Xia, Zijun Chen, Qi Liu, Yuan Feng, Hongbin Zhou, Renrui Zhang, Shiyang Feng, Peng Gao, Hongyuan Zha, Junchi Yan, Botian Shi, Yu Qiao, Bo Zhang

机构 * College of Computer Science and Artificial Intelligence, Fudan University（复旦大学计算机科学与人工智能学院） ； Shanghai Artificial Intelligence Laboratory（上海人工智能实验室） ； The Chinese University of Hong Kong, Shenzhen（香港中文大学（深圳）） ； School of Artificial Intelligence, Shanghai Jiao Tong University（上海交通大学人工智能学院） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；logical reasoning(abstract)；分类 cs.CL、cs.AI

AI总结 本文提出TrustGeoGen，通过正式验证生成多模态几何数据，提升模型深度几何推理能力，在GeoQA等基准测试中取得显著成效。

Multimodal DeepResearcher: Generating Text-Chart Interleaved Reports From Scratch with Agentic Framework

多模态深度研究员：从零开始生成文本-图表交织报告的代理框架

Zhaorui Yang, Bo Pan, Han Wang, Yiyao Wang, Xingyu Liu, Luoxuan Weng, Yingchaojie Feng, Haozhe Feng, Minfeng Zhu, Bo Zhang, Wei Chen

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.CL、cs.AI

AI总结 多模态深度研究员通过代理框架实现从零开始生成文本-图表交织报告，利用FDV结构化文本表示提升可视化生成质量。

Comments AAAI 2026 Oral

Self-Improving AI Agents through Self-Play

通过自play实现自我改进的AI代理

Przemyslaw Chojecki

专题命中 代码与定理证明 ：verifier(abstract)；self-correction(abstract)；分类 cs.AI、cs.LG

AI总结 本文提出了一种通过自play实现自我改进的AI代理框架，通过GVU算子和方差不等式理论，统一了语言自play、自我修正和合成数据 bootstrap 的研究。

Automating Structural Engineering Workflows with Large Language Model Agents

Haoran Liang, Yufa Zhou, Mohammad Talebi Kalaleh, Qipei Mei

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.CL、cs.AI

Comments Code: https://github.com/DelosLiang/masse

Factorio Learning Environment

Jack Hopkins, Mart Bakler, Akbir Khan

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.CL、cs.LG

A Stochastic Dynamical Theory of LLM Self-Adversariality: Modeling Severity Drift as a Critical Process

Jack David Carson

专题命中 代码与定理证明 ：reasoning(abstract)；chain-of-thought(abstract)；分类 cs.CL、cs.AI

Comments Experimental verification and more formal argument for Markov approximation of bias propagation to be released soon. Primarily pushed now to establish novelty and ease of sharing. Please do not cite this work until the forthcoming experimental validation and updated mathematical model are provided

Formally Explaining Neural Networks within Reactive Systems

Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, Guy Katz

专题命中 代码与定理证明 ：reasoning(abstract)；verifier(abstract)；分类 cs.AI、cs.LG

Comments To appear in Proc. 23rd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD)

Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation

Wenqing Zheng, S P Sharan, Ajay Kumar Jaiswal, Kevin Wang, Yihan Xi, Dejia Xu, Zhangyang Wang

专题命中 代码与定理证明 ：reasoning(abstract)；chain-of-thought(abstract)；分类 cs.AI、cs.LG

Comments Accepted in ICML 2023

String Tightening as a Self-Organizing Phenomenon: Computation of Shortest Homotopic Path, Smooth Path, and Convex Hull

Bonny Banerjee

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.AI、cs.LG

Journal ref in IEEE Transactions on Neural Networks, vol. 18, no. 5, pp. 1463-1471, Sept. 2007

Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean

物理推理公理：在Lean中编码塞伯格 - 维滕解

Michael R. Douglas

专题命中 代码与定理证明 ：reasoning(title)

AI总结 研究利用交互式定理证明器验证物理论证，通过假定物理假设清单，经机器可验证证明得出结果，以Lean 4形式化${N}=2$ $SU(2)$超杨 - 米尔斯的塞伯格 - 维滕解，为验证理论物理中AI生成结果提供合理标准。

Comments 18 pages; companion github repo mrdouglasny/seiberg-witten

PROMISE: Proof Automation as Structural Imitation of Human Reasoning

PROMISE：证明自动化作为人类推理的结构模仿

Youngjoo Ahn, Sangyeop Yeo, Gijung Im, Jongmin Lee, Jinyoung Yeo, Jieung Kim

专题命中 代码与定理证明 ：reasoning(title)

AI总结 PROMISE通过结构化嵌入框架实现证明生成自动化，通过挖掘证明状态的结构模式提升大规模定理证明的可扩展性。

Reasoning about quantum knowledge

Ellie D'Hondt, Prakash Panangaden

专题命中 代码与定理证明 ：reasoning(title)

Comments 12 pages, 2 figures. Revised version based on referee reports

Journal ref Proceedings of FSTTCS05, LNCS vol. 3821, 0544c, 2005

Shrinking the Generation-Verification Gap with Weak Verifiers

缩小生成-验证差距的弱验证器

Jon Saad-Falcon, E. Kelly Buchanan, Mayee F. Chen, Tzu-Heng Huang, Brendan McLaughlin, Tanvir Bhathal, Shang Zhu, Ben Athiwaratkun, Frederic Sala, Scott Linderman, Azalia Mirhoseini, Christopher Ré

机构 * Stanford University（斯坦福大学） ； University of Wisconsin-Madison（威斯康星大学麦迪逊分校） ； Together AI 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；verifier(abstract)；分类 cs.CL

AI总结 Weaver通过结合多个弱验证器，有效缩小生成-验证差距，提升验证性能至接近理想验证器水平。

Comments Annual Conference on Neural Information Processing Systems (NeurIPS) 2025

Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization

多智能体证明自动形式化的高效测试时优化

Tian-Shuo Liu, Shiyuan Zhang, Zijie Geng, Haoyu Liu, Runjie Xu, Pengyuan Wang, Lei Yuan, Yang Yu

机构 * Polixir Technologies（波利希瑞技术公司） ； University of Science and Technology of China（中国科学技术大学） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；test-time compute(abstract)；分类 cs.AI

AI总结 研究多智能体证明自动形式化，提出ToMap框架，将其构建为分解器-形式化器-证明器管道，经瓶颈分析聚焦于分解器优化，通过特定循环和标准指导更新，实验显示该方法提升了性能且降低测试成本。

Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

形式化迪斯科：可扩展的形式化验证程序的开放式生成

Gabriel Poesia, Simon Henniger, Tzu-Han Hsu, Yilun Du, Nada Amin

机构 * Kempner Institute, Harvard University（坎普纳研究所，哈佛大学） ； School of Engineering and Applied Sciences, Harvard University（工程与应用科学学院，哈佛大学） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；verifier(abstract)；分类 cs.AI

AI总结 针对生成程序质量保证落后及形式验证数据稀缺问题，提出Formal Disco分布式系统，协调三类工人，记录痕迹用于改进，提出最大熵原则，发布数据集并微调模型，为形式推理领域大规模创建合成数据。

Comments Code: https://github.com/metareflection/formal-disco Datasets: https://huggingface.co/collections/metareflection/formal-disco

MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

MINIF2F-DAFNY: 通过自动主动验证的LLM引导数学定理证明

Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Sean B. Holden

机构 * University of Cambridge, Cambridge, UK（剑桥大学） ； Amazon Web Services, London, UK（亚马逊网络服务（伦敦）） ； Amazon Web Services, Boston, USA（亚马逊网络服务（波士顿）） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；verifier(abstract)；分类 cs.LG

AI总结 提出首个将数学基准miniF2F翻译到自动主动验证器Dafny的数据集，评估8个LLM的证明生成能力，最佳模型Claude Opus 4.6达到62.7%的累积通过率，比空证明基线提升23.8个百分点。

Beyond the Autoregressive Horizon: A Comprehensive Survey of Diffusion Models, World Modelling, and State Space Models for Code

超越自回归视野：扩散模型、世界模型和状态空间模型在代码领域的综合综述

Kishan Maharaj, Ashita Saxena, Srikanth Tamilselvam

机构 * IBM 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.AI

AI总结 综述扩散模型、代码世界模型和状态空间模型在代码生成中的潜力，以克服自回归模型在全局规划、长程依赖和执行语义方面的局限，并展望“系统2”代码生成智能体。

Comments 14 Pages, 1 Table, 1 Figure

AXE: Grey-Box Exploitability Confirmation for Localized Vulnerability Reports

AXE：针对局部漏洞报告的灰盒可利用性确认

Amirali Sajadi, Tu Nguyen, Kostadin Damevski, Preetha Chatterjee

机构 * Virginia Commonwealth University（弗吉尼亚 Commonwealth 大学） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；planning(abstract)；分类 cs.AI

AI总结 提出多智能体框架AXE，利用CWE分类和代码位置等轻量级元数据，通过解耦规划、代码探索和动态执行反馈实现Web漏洞利用，在CVE-Bench上达到30%成功率，比黑盒基线提升3倍。

Process-Verified Reinforcement Learning for Theorem Proving via Lean

基于Lean的过程验证强化学习用于定理证明

Minsu Kim, Se-Young Yun

机构 * KAIST AI（韩国科学技术院人工智能系） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；verifier(abstract)；分类 cs.AI

AI总结 提出利用Lean证明助手提供过程级验证信号，结合GRPO风格强化学习目标，通过策略级监督提升定理证明性能。