大模型推理能力

Code Reasoning for Software Engineering Tasks: A Survey and A Call to Action

代码推理用于软件工程任务：调查与呼吁行动

Saurabh Pujar, Ira Ceka, Irene Manotas, Gail Kaiser, Baishakhi Ray, Shyam Ramji

机构 * IBM ； Columbia University（哥伦比亚大学） 纠错

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

AI总结 本文调查代码推理技术，探讨其在软件工程任务中的影响，提出未来研究方向。

Comments Published in Transactions on Machine Learning Research (06/2026) 40 pages, 8 figures, 11 tables

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% 的验证率。

A Machine-Verified Proof of a Quantum-Optimization Conjecture

一个量子优化猜想的机器验证证明

Uri Kol, Maor Ben-Shahar, Kfir Sulimany, Dirk Englund

机构 * Center of Mathematical Sciences and Applications, Harvard University（哈佛大学数学科学中心） ； MIT Center for Theoretical Physics - a Leinweber Institute（麻省理工学院理论物理中心 - 莱因韦伯研究所） ； Research Laboratory of Electronics, Massachusetts Institute of Technology（麻省理工学院电子研究实验室） 纠错

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

AI总结 利用大语言模型Claude Fable 5发现证明，并通过Lean 4证明助手端到端验证了Farhi-Goldstone-Gutmann猜想，即深度p的量子近似优化算法在环上的近似比恰好为(2p+1)/(2p+2)。

Statistically Indistinguishable, Operationally Distinct: A Formal Barrier for Tabular Foundation Models

统计不可区分，操作上截然不同：表格基础模型的形式化障碍

Tassilo Klein, Johannes Hoffart

机构 * SAP SE（SAP公司） 纠错

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

AI总结 本文提出操作图灵测试，证明仅基于值的表格模型无法区分合法与违规数据库状态，而操作审计特征可突破该障碍，揭示可识别性而非模型容量是根本限制。

Comments Accepted at the 2nd ICML Workshop on Foundation Models for Structured Data, 2026

Self-Supervised Theorem Discovery in a Formal Axiomatic System

形式化公理系统中的自监督定理发现

Kazuki Ota, Takayuki Osa, Tatsuya Harada

机构 * The University of Tokyo, Japan（东京大学，日本） ； RIKEN AIP, Japan（日本RIKEN AIP） 纠错

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

AI总结 提出一种自监督定理发现算法，通过交替进行证明搜索和有用定理提取，从公理和推理规则出发逐步构建定理库，实验表明发现的定理具有人类数学意义且能提升大语言模型证明性能。

Comments AI for Math Workshop @ ICML 2026

Words Speak Louder Than Code: Investigating Cognitive Heuristics in LLM-Based Code Vulnerability Detection

言语胜于代码：探究基于LLM的代码漏洞检测中的认知启发式

Asif Shahriar, Hongyu Cai, Hadjer Benkraouda, Gang Wang, Z. Berkay Celik

机构 * BRAC University（布拉德大学） ； Purdue University（普渡大学） ； University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） 纠错

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

AI总结 本文首次系统探究认知启发式对LLM代码漏洞检测的影响，提出控制框架，发现所有评估模型均易受光环、框架和锚定效应影响，且语义推理型漏洞更易受影响。

On Compositional Learning Behaviours in Formal Mathematics

论形式数学中的组合学习行为

Kevin Yandoka Denamganaï

机构 * University of York（约克大学） 纠错

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

AI总结 本文提出 S2B-LM 基准，通过去除数值处理混淆并添加思维链框架来评估组合学习行为（CLB），发现 CLB 能力对于形式数学验证的困难部分必要但不充分。

Comments Accepted at AI4Math Workshop @ ICML2026

Modelling Human Values for Value-Aware Multi-Agent Systems

为价值感知多智能体系统建模人类价值观

Nardine Osman, Mark d'Inverno

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

AI总结 本文提出一个形式化框架，用于表示人类价值观，以支持多智能体系统中的价值感知推理。通过社会心理学研究，建立价值关系和重要性模型，实现行为评估和价值感知决策机制。

Comments arXiv admin note: text overlap with arXiv:2305.02748

PBFuzz: Agentic Directed Fuzzing for PoV Generation

PBFuzz：面向漏洞证明的代理引导模糊测试

Haochen Zeng, Andrew Bao, Jiajun Cheng, Chengyu Song

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

AI总结 PBFuzz通过模拟人类专家流程，自动提取语义约束并高效生成漏洞证明输入，实验表明其在效率和漏洞触发性能上优于现有方法。

Comments 24 pages, 8 figures

Adaptive Shielding via Parametric Safety Proofs

基于参数安全证明的自适应防护

Yao Feng, Jun Zhu, André Platzer, Jonathan Laurent

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

AI总结 本文提出一种编程语言框架，允许专家静态指定自适应防护，以确保学习代理的安全控制范围，并在运行时获取知识时变得更加宽松。

Journal ref Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA1, 2025