大模型推理能力

Automated Proof Generation for Rust Code via Self-Evolution

通过自我进化实现Rust代码的自动证明生成

Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, Lidong Zhou

机构 * Peking University（北京大学） ； Microsoft Research（微软研究院） ； University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） ； Columbia University（哥伦比亚大学） ； University of California Irvine（加州大学 Irvine 分校） 纠错

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

AI总结 SAFE框架通过自我进化循环和自我调试机制，提升开源模型自动编写Rust代码证明的能力，准确率达52.52%

TensorCommitments: A Lightweight Verifiable Inference for Language Models

张量承诺：一种轻量级可验证的语言模型推断

Oguzhan Baser, Elahe Sadeghi, Eric Wang, David Ribeiro Alves, Sam Kazemian, Hong Kang, Sandeep P. Chinchali, Sriram Vishwanath

机构 * The University of Texas at Austin（德克萨斯大学） ； Georgia Institute of Technology（佐治亚理工学院） ； Theseus AI Labs（Theseus AI实验室） ； McGill University（麦吉尔大学） 纠错

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

AI总结 张量承诺通过轻量级的证明方案实现可验证的语言模型推断，提高对抗性攻击的鲁棒性。

Comments 23 pages, 8 figures, under review

SKATE, a Scalable Tournament Eval: Weaker LLMs differentiate between stronger ones using verifiable challenges

SKATE，一种可扩展的锦标赛评估：较弱的LLM通过可验证的挑战区分更强的LLM

Dewi S. W. Gould, Bruno Mlodozeniec, Samuel F. Brown

机构 * The Alan Turing Institute（阿尔文·图灵研究所） ； University of Cambridge（剑桥大学） ； Max Planck Institute for Intelligent Systems（马克斯·普朗克智能系统研究所） ； Independent（独立研究者） 纠错

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

AI总结 SKATE通过让LLM相互生成和解决可验证任务，实现可扩展的评估框架，揭示模型间的细微能力差异。

Comments 7 pages and appendices

Protecting Context and Prompts: Deterministic Security for Non-Deterministic AI

保护上下文和提示：非确定性AI的确定性安全

Mohan Rajagopalan, Vinay Rao

机构 * MACAW Security, Inc.（MACAW安全公司） 纠错

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

AI总结 本研究提出认证提示和上下文技术，通过加密验证和策略代数实现LLM的预防性安全，有效防止提示注入和上下文操纵攻击。

A Small-Scale System for Autoregressive Program Synthesis Enabling Controlled Experimentation

一个小型系统用于自回归程序合成，以实现受控实验

Russ Webb, Jason Ramapuram

机构 * Apple（苹果公司） 纠错

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

AI总结 Cadmus系统通过低成本模型实现复杂程序合成任务，展示其在整数算术任务中的优越性能并揭示大模型的局限性。

Agentifying Agentic AI

使AI具备代理性

Virginia Dignum, Frank Dignum

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

AI总结 本文提出通过整合BDI架构与制度建模，构建具备透明性和合作性的代理系统，实现自主性与责任感的统一。

Comments 10 pages; 1 figure

Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis

通过类型引导的程序合成学习保证类型正确性

Zhechong Huang, Zhao Zhang, Ruyi Ji, Tingxuan Xia, Qihao Zhu, Qinxiang Cao, Zeyu Sun, Wiggin Zhou, Yingfei Xiong

机构 * Peking University（北京大学） ； University of Michigan（密歇根大学） ； Shanghai Jiao Tong University（上海交通大学） ； Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所） ； Tencent（腾讯） 纠错

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

AI总结 TyFlow 通过内部化类型推理，提升代码生成的类型正确性与功能正确性。

Evaluating Large Language Models on Solved and Unsolved Problems in Graph Theory: Implications for Computing Education

在图论中解决和未解决的问题上评估大语言模型：对计算教育的启示

Adithya Kulkarni, Mohna Chakraborty, Jay Bagga

机构 * Department of Computer Science（计算机科学系） ； Ball State University（巴尔的摩州立大学） ； School of Artificial Intelligence and Data Science（人工智能与数据科学学院） ； Jio Institute（乔研究所） 纠错

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

AI总结 本研究评估了大语言模型在图论已解决和未解决问题上的表现，发现其在已有知识探索上有效，但在需要创新数学洞察的任务中存在局限，对计算教育有重要启示。

Formal Semantic Control over Language Models

语言模型的正式语义控制

Yingji Zhang

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

AI总结 本研究通过VAE框架，探索了在潜在空间中解构语义特征以提升语言模型的可解释性和可控性。

Should I Have Expressed a Different Intent? Counterfactual Generation for LLM-Based Autonomous Control

我本应表达不同的意图？基于LLM的自主控制的反事实生成

Amirmohammad Farzaneh, Salvatore D'Oro, Osvaldo Simeone

机构 * Department of Engineering, King's College London, London, UK（伦敦大学金史密斯学院工程系） ； Intelligent Networked Systems Institute (INSI), Northeastern University, Boston, MA, USA（东北大学智能网络系统研究所） ； Intelligent Networked Systems Institute (INSI), Northeastern University, London, UK（伦敦大学东北大学智能网络系统研究所） 纠错

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

AI总结 本文提出一种基于结构因果模型的反事实生成方法，通过概率性反事实生成和离线校准，为LLM驱动的自主控制提供可靠反事实推理，展示了在无线网络控制中的显著优势。

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

为验证条件进行神经定理证明：一个现实世界的基准测试

Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang, Peixin Wang, Haonan Li, Wenda Li, Conrad Watt

机构 * Nanyang Technological University（南洋理工大学） ； Peking University（北京大学） ； MBZUAI ； Imperial College London（帝国理工学院） ； East China Normal University（华东师范大学） ； University of Edinburgh（爱丁堡大学） 纠错

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

AI总结 本研究提出NTP4VC，首个现实世界多语言基准测试，评估LLMs在自动验证条件证明中的表现，揭示程序验证中的挑战与未来研究方向。

Comments Accepted in ICLR'26

Decompose-and-Formalise: Recursively Verifiable Natural Language Inference

分解与形式化：可递归验证的自然语言推理

Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas

机构 * Department of Computer Science, University of Manchester（曼彻斯特大学计算机科学系） ； School of Computer Science, University of Sheffield（谢菲尔德大学计算机科学学院） ； Idiap Research Institute（Idiap研究 institute） ； National Biomarker Centre, CRUK-MI, University of Manchester（曼彻斯特大学国家生物标记中心） 纠错

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

AI总结 本文提出分解与形式化框架，通过自底向上的验证和局部诊断引导细化，提升自然语言推理的解释验证效率和准确性。

LLM Agents for Knowledge Discovery in Atomic Layer Processing

用于原子层处理中知识发现的LLM代理

Andreas Werbrouck, Marshall B. Lindsay, Matthew Maschmann, Matthias J. Young

机构 * University of Missouri Columbia（密苏里大学哥伦比亚分校） 纠错

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

AI总结 本研究利用LLM代理在原子层处理中探索化学相互作用，通过试错和持续探索实现知识发现。

Comments Accepted submission to the AI4MAT workshop@NEURIPS 2025. As submitted, except author names added

Evolution of AI in Education: Agentic Workflows

人工智能在教育中的演变：代理工作流

Firuz Kamalov, David Santandreu Calonge, Linda Smail, Dilshod Azizov, Dimple R. Thadani, Theresa Kwong, Amara Atif

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

AI总结 本研究探讨了AI代理在教育中的应用，提出多代理框架用于自动评分，并指出其在一致性上的优势及需进一步研究的可解释性问题。

Comments made the abstract more succinct, revised the methodology, added PRISMA flow chart, updated references

Designing AI-Resilient Assessments Using Interconnected Problems: A Theoretically Grounded and Empirically Validated Framework

利用互联问题设计AI鲁棒评估：一种理论严谨且经验证实的框架

Kaihua Ding

机构 * University of Pennsylvania（宾夕法尼亚大学） 纠错

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

AI总结 本文提出了一种理论严谨且经验证实的框架，通过设计互联问题来提高评估的AI鲁棒性，挑战了开放性评估的鲁棒性假设，并提供了实证支持和实用设计方法。

Comments 8 pages, 3 figures and 3 tables, under submission to IEEE FIE

Large Language Model for OWL Proofs

面向OWL证明的大型语言模型

Hui Yang, Jiaoyan Chen, Uli Sattler

机构 * The University of Manchester（曼彻斯特大学） 纠错

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

AI总结 本文提出面向OWL本体论证明生成的LLM方法，通过构建评估框架验证了逻辑复杂性对LLM性能的影响，并发现输入数据质量对证明生成至关重要。

AI Co-Scientist for Knowledge Synthesis in Medical Contexts: A Proof of Concept

医疗领域知识综合的AI合作者：概念验证

Arya Rahgozar, Pouria Mortezaagha

机构 * Methodological Implementation Research, Ottawa Hospital Research Institute（方法实施研究，渥太华医院研究所） ； School of Engineering Design and Teaching Innovation, University of Ottawa（工程设计与教学创新学院，渥太华大学） 纠错

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

AI总结 本研究提出了一种基于PICOS的AI合作者，通过整合知识图谱和自然语言处理技术，提升医疗领域证据综合的可扩展性、透明性和效率。

LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

LeanProgress: 通过证明进度预测引导神经定理证明的搜索

Robert Joseph George, Suozhi Huang, Peiyang Song, Anima Anandkumar

机构 * Computing + Mathematical Sciences Department（计算与数学科学系） ； California Institute of Technology（加利福尼亚理工学院） ； Computer Science Department（计算机科学系） ； Princeton University（普林斯顿大学） 纠错

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

AI总结 LeanProgress通过预测证明进度提升神经定理证明效率，实现Mathlib4证明效率提升3.8%

Comments Published in TMLR (Transactions on Machine Learning Research)

Theorem Prover as a Judge for Synthetic Data Generation

定理推理解释器作为合成数据生成的裁判

Joshua Ong Jun Leang, Giwon Hong, Wenda Li, Shay B. Cohen

机构 * School of Informatics, The University of Edinburgh（信息学院，爱丁堡大学） 纠错

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

AI总结 本研究提出TP-as-a-Judge和RLTPF方法，通过定理推理解释器提升LLM的合成数据生成与推理准确性。

Journal ref Proc. ACL 2025, pp. 29941-29977

Recursive Knowledge Synthesis for Multi-LLM Systems: Stability Analysis and Tri-Agent Audit Framework

多LLM系统的递归知识合成：稳定性分析与三代理审计框架

Toshiyuki Shigemura

机构 * Independent Researcher（独立研究者） 纠错

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

AI总结 本文提出三代理框架用于多LLM系统稳定性分析，通过递归知识合成实现安全可靠的知识生成。

Comments 25 pages, 9 figures. Pilot feasibility study using public-access large language models without API-level orchestration

AI Agent Smart Contract Exploit Generation

AI代理智能合约漏洞生成

Arthur Gervais, Liyi Zhou

机构 * University College London（伦敦大学学院） ； The University of Sydney（悉尼大学） ； Decentralized Intelligence AG（去中心化智能有限公司） ； UC Berkeley RDI（伯克利大学RDI） 纠错

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

AI总结 A1通过代理系统结合大语言模型，实现智能合约漏洞的高效生成与验证，成功率达63%，并揭示了攻击与防御在经济上的不对称性。

Vibe Coding an LLM-powered Theorem Prover

Vibe 编码一个基于 LLM 的定理推理论证系统

Zhe Hou

机构 * Griffith University（格里菲斯大学） 纠错

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

AI总结 Isabellm是一个基于LLM的定理推理论证系统，通过结合分步推证器和证明计划器，实现自动证明合成，并展示了LLM在复杂证明任务中的潜力与挑战。

Automated Post-Incident Policy Gap Analysis via Threat-Informed Evidence Mapping using Large Language Models

通过大语言模型进行威胁感知证据映射的自动事后政策差距分析

Huan Lin Oh, Jay Yong Jun Jie, Mandy Lee Ling Siu, Jonathan Pan

机构 * Nanyang Technological University, Singapore（南洋理工大学） 纠错

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

AI总结 本文提出利用大语言模型进行威胁感知证据映射，实现自动事后政策差距分析，提升网络安全事件审查的效率与可审计性。

Comments 5 pages, 1 figure. Preprint

Causal-Enhanced AI Agents for Medical Research Screening

因果增强的医疗研究筛查AI代理

Duc Ngo, Arya Rahgoza

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

AI总结 本文提出一种因果图增强的AI代理，用于医疗研究筛选，通过显式因果推理和双层知识图谱提升系统综述的准确性和可解释性。

Comments for submission to The 39th Canadian Conference on Artificial Intelligence

Enforcing Temporal Constraints for LLM Agents

为LLM代理强制执行时间约束

Adharsh Kamath, Sishen Zhang, Calvin Xu, Shubham Ugare, Gagandeep Singh, Sasa Misailovic

机构 * University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） ； University of Illinois at Urbana-Champaign, USA（伊利诺伊大学厄巴纳-香槟分校，美国） ； Meta 纠错

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

AI总结 Agent-C通过运行时保证确保LLM代理遵守时间安全属性，提高任务实用性并实现完美安全性。

zkFL-Health: Blockchain-Enabled Zero-Knowledge Federated Learning for Medical AI Privacy

zkFL-Health: 区块链赋能的零知识联邦学习用于医疗AI隐私

Savvy Sharma, George Petrovic, Sarthak Kaushik

机构 * School of Arts And Technology（艺术与技术学院） ； George Brown Polytechnic（乔治布朗理工学院） 纠错

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

AI总结 zkFL-Health通过结合联邦学习、零知识证明和可信执行环境，实现医疗AI的隐私保护和可验证协作训练。

Comments 10 pages, 1 figure, 5 tables

The Silent Scholar Problem: A Probabilistic Framework for Breaking Epistemic Asymmetry in LLM Agents

沉默学者问题：一种基于概率的框架，用于在LLM代理中打破知识不对称性

Zan-Kai Chong, Hiroyuki Ohsaki, Bryan Ng

机构 * School of Science and Technology（科学与技术学院） ； Kwansei Gakuin University（冈山大学） ； School of Engineering & Computer Science（工程与计算机科学学院） ； Victoria University of Wellington（惠灵顿维多利亚大学） 纠错

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

AI总结 本文提出了一种基于概率的框架，用于在LLM代理中打破知识不对称性，通过双向知识交流和不确定性驱动的主动学习策略提升代理的适应性和信息获取能力。

Dual Computational Horizons: Incompleteness and Unpredictability in Intelligent Systems

双重计算 horizon：智能系统中的不完全性与不可预测性

Abhisek Ganguly

机构 * Engineering Mechanics Unit, Jawaharlal Nehru Centre for Advanced Scientific Research, Bangalore 560064, India（奈尔中心先进科学研究所工程力学单元，班加罗尔560064，印度） 纠错

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

AI总结 本文研究了智能系统中由于形式不完全性和动态不可预测性导致的计算限制，并探讨了推理、预测与自我分析之间的权衡。

Comments 8 Pages, 0 figures

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification

MSC-180：一个用于从数学学科分类自动形式定理证明的基准

Sirui Li, Wangyue Lu, Xiaorui Shi, Ke Weng, Haozhe Sun, Minghe Yu, Tiancheng Zhang, Ge Yu, Hengyu Liu, Lun Du

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

AI总结 MSC-180是一个用于评估自动形式定理证明的基准，揭示了当前基于LLM的定理证明者在数学领域覆盖和泛化能力上的不足。

Instruction-Level Weight Shaping: A Framework for Self-Improving AI Agents

指令级权重塑造：一种自我改进的AI代理框架

Rimom Costa

机构 * Adobe Commerce Cloud Support Engineering - EMEA Division（Adobe 商业云支持工程 - EMEA部门） 纠错

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

AI总结 指令级权重塑造通过外部可审计伪参数提升AI代理的自我改进能力，实现低延迟部署和减少幻觉，适用于动态领域。

Comments 12 pages, 1 figure, 2 tables