大模型推理能力

Analyzing the Narration Gap in LLM-Solver Loops

分析大语言模型-求解器循环中的叙述差距

Zunchen Huang, Songgaojun Deng

机构 * Eindhoven University of Technology（埃因霍温理工大学） 纠错

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

AI总结 研究LLM与SAT/SMT求解器混合推理中，将求解器输出转化为用户答案的叙述步骤存在的安全漏洞，通过形式化建模和实验评估发现证书门控可保证求解结果正确，但对抗攻击可反转结论。

What Must Generalist Agents Remember?

通用型智能体必须记住什么？

Khurram Yamin, Namrata Deka, Maitreyi Swaroop, Albert Ting, Jeff Schneider, Bryan Wilder

机构 * Carnegie Mellon University（卡内基梅隆大学） ； Georgia Institute of Technology（佐治亚理工学院） 纠错

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

AI总结 本文形式化论证了通用型智能体为在多个环境和目标下近似最优行动，必须存储领域相关信息以区分观察瓶颈处的不兼容最优动作，并证明记忆可用于重构局部转移动态。

Extracting Semantics: LLM-Guided Automatic Population of Robot Ontology from URDF

提取语义：从URDF自动构建机器人本体的LLM引导方法

Bastien Dussard, Guillaume Sarthou

机构 * LAAS-CNRS, Department of Robotics, Toulouse, France（法国图卢兹机器人系CNRS实验室） 纠错

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

AI总结 提出利用大语言模型从URDF文件自动生成机器人语义本体，通过多数投票和语法验证确保与现有本体对齐，初步实验表明该方法能有效桥接低层描述与高层知识表示。

Journal ref 18th International Conference on Social Robotics (ICSR 2026), University of London, Jul 2026, Londres, United Kingdom

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

Mask-Proof: 一种基于LLM的数学证明自动数据整理流水线

Jierui Zhang, Siyuan Tan, Xinhang Li, Longzhuangzhi Lin, Dailin Li, Chengfeng Gu, Xinping Li, Yaxian Hao, Shengjia Liang, Yuxiang Ren, Wenhao Liu

机构 * School of Computer Science, Beijing University of Posts and Telecommunications（北京邮电大学计算机学院） ； Graduate College for Engineers, Beijing University of Posts and Telecommunications（北京邮电大学研究生院工程师学院） ； School of Mathematical Sciences, Fudan University（复旦大学数学科学学院） ； School of Cyberspace Security, Beijing University of Posts and Telecommunications（北京邮电大学网络空间安全学院） ； School of Computer Science and Technology, Dalian University of Technology（大连理工大学计算机科学与技术学院） ； Chu Kochen Honors College, Zhejiang University（浙江大学竺可桢学院） ； Department of Psychological and Cognitive Sciences, Tsinghua University（清华大学心理学与认知科学系） ； State Key Laboratory of Virtual Reality Technology and Systems, Beihang University（北京航空航天大学虚拟现实技术与系统国家重点实验室） ； School of Intelligence Science and Technology, Nanjing University（南京大学智能科学与技术学院） 纠错

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

AI总结 提出Mask-Proof流水线，将真实证明转化为可自动检查的掩码步骤任务，通过LLM等价性判断器评估模型推理，构建包含292个问题的基准，推理增强模型性能提升12%-27%。

VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization

VGPT-RSI 用于 RH 邻近形式化进展：边界证书、已验证的有限 Lagarias 不等式和显式故障定位

Zhixin Hu, Tao Xu, Xiaodian Sun, Li Jin, Momiao Xiong

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

AI总结 提出 VGPT-RSI 系统，通过构造并验证有限 RH 边界证书和 Lagarias 准则的有限形式化，实现 Riemann 假设邻近问题的部分形式化进展，并明确识别剩余数学障碍。

Comments 31 pages, 3 figures

Cognitive Debt: AI as Intellectual Leverage and the Dynamics of Systemic Fragility

认知债务：作为智力杠杆的AI与系统性脆弱性的动态机制

Shuchen Meng

机构 * New York University（纽约大学） 纠错

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

AI总结 本文提出认知债务的形式化理论，通过建立包含认知资本和认知债务的状态变量模型，证明理性代理人会积累认知债务，并导致认知明斯基时刻和系统性脆弱性。

Comments 46 pages, 3 figures. Preliminary version; comments welcome

Measuring Epistemic Resilience of LLMs Under Misleading Medical Context

测量大语言模型在误导性医疗上下文下的认知韧性

Hongjian Zhou, Xinyu Zou, Jinge Wu, Sean Wu, Junchi Yu, Bradley Max Segal, Tobias Erich Niebuhr, Sara Amro, Michael Petrus, Sheikh Momin, Alexandra M. Cardoso Pinto, Rachel Niesen, Laura Sophie Wegner, Dhruv Darji, Jung Moses Koo, Joshua Fieggen, Kapil Narain, Mingde Zeng, Lei Clifton, Linda Shapiro, Fenglin Liu, David A. Clifton

机构 * University of Oxford（牛津大学） ； University of Washington（华盛顿大学） ； University College London（伦敦大学学院） ； University of Waterloo（滑铁卢大学） 纠错

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

AI总结 本研究提出MedMisBench基准，通过注入误导性上下文测试大语言模型在医疗场景中的认知韧性，发现模型准确率从71.1%降至38.0%，权威性虚假信息攻击成功率达69.5%。

MiniMax Sparse Attention

MiniMax 稀疏注意力

Xunhao Lai, Weiqi Xu, Yufeng Yang, Qiaorui Chen, Yang Xu, Lunbin Zeng, Xiaolong Li, Haohai Sun, Haichao Zhu, Vito Zhang, Jinkai Hu, Jiayao Li, Rui Gao, Zekun Li, Songquan Zhu, Jingkai Zhou, Pengyu Zhao

机构 * MiniMax ； Peking University（北京大学） ； NVIDIA（英伟达） ； Zhejiang University（浙江大学） ； Huazhong University of Science and Technology（华中科技大学） 纠错

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

AI总结 提出 MiniMax 稀疏注意力（MSA），一种基于分组查询注意力的块级稀疏注意力机制，通过轻量索引分支选择 Top-k 键值块，实现高效长上下文处理，在 109B 模型上以 1M 上下文减少 28.4 倍注意力计算，并带来 14.2 倍预填充和 7.6 倍解码加速。

Comments 30 pages, 14 figures

ERTS: Adversarial Robustness Testing of Ethical AI via Semantic Perturbation in a Bounded Consequence Space

ERTS: 通过有界后果空间中的语义扰动进行伦理AI的对抗鲁棒性测试

Pratyush Chaudhari

机构 * Pratyush Chaudhari（普拉蒂什·查德哈里） 纠错

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

AI总结 提出伦理鲁棒性测试系统(ERTS)，通过有界伦理后果空间、语义扰动和领域自适应评估，测试AI在伦理推理中的对抗鲁棒性，实验表明仅33%模型通过测试。

Comments 8 pages, 10 tables

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Pythagoras-Prover: 通过增强型Lean形式化推进高效形式化证明

Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

机构 * Imperial College London（伦敦帝国学院） ； University of Edinburgh（爱丁堡大学） ； Nanyang Technological University（南洋理工大学） ； MBZUAI（穆罕默德·本·扎耶德人工智能大学） 纠错

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

AI总结 提出Pythagoras-Prover系列，包括自回归和扩散模型，通过课程SFT、动态过滤和增强型Lean形式化（ALF）扩展验证数据，在MiniF2F-Test上以更少参数超越DeepSeek-Prover-V2。

Comments Pythagoras-Prover: Technical Report

Bridging the Agent-World Gap: Text World Models for LLM-based Agents

弥合智能体-世界鸿沟：面向基于LLM的智能体的文本世界模型

Yixia Li, Hongru Wang, Peng Lai, Zhiwen Ruan, He Zhu, Youxin Zhu, Ganlong Zhao, Minda Hu, Yun Chen, Sibei Yang, Peng Li, Jeff Z. Pan, Jia Pan, Guanhua Chen, Yang Liu, Guanbin Li

机构 * Southern University of Science and Technology（南方科技大学） ； University of Edinburgh（爱丁堡大学） ； Peking University（北京大学） ； Sun Yat-sen University（中山大学） ； The Chinese University of Hong Kong（香港中文大学） ； Shanghai University of Finance and Economics（上海财经大学） ； Tsinghua University（清华大学） ； The University of Hong Kong（香港大学） 纠错

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

AI总结 本文系统综述了面向基于LLM的智能体的文本世界模型，围绕形式化框架和智能体生命周期，涵盖基础定义、构建范式、应用（训练时经验合成与推理时规划、验证、适应）及评估，旨在整合该领域并明确设计空间与开放挑战。

Comments Code: https://github.com/sustech-nlp/awesome-text-world-models

Traxia: A Framework for Verifiable, Agent-Native Scientific Publishing

Traxia：一个可验证的、智能体原生的科学出版框架

Wisdom Dogah

机构 * Faculty of Computing and Mathematical Sciences, University of Mines and Technology (UMaT), Tarkwa, Ghana（加纳塔夸矿业与技术大学计算与数学科学学院） ； BlackMatrix AI Research, Accra, Ghana（加纳阿克拉BlackMatrix AI研究院） 纠错

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

AI总结 提出Traxia框架，通过智能体身份、可验证出版、四层同行评审、声誉机制和知识图谱，解决科学出版中可验证性、归属和可重复性问题。

Comments 22 pages, 3 figures, 3 tables. Preprint. Under active development. Comments welcome

Beyond Post-hoc Explanation: Toward Glassbox AI via Probabilistic Mediation

超越事后解释：通过概率中介迈向玻璃箱AI

Manuele Leonelli

机构 * Manuele Leonelli（曼努埃尔·莱奥内利） 纠错

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

AI总结 针对大语言模型在关键领域的不透明性，提出玻璃箱框架，利用贝叶斯网络作为事前中介层，实现可审计推理、不确定性量化和可争议输出。

CARVE-Q: Quantum-Proposed, Classically Certified Interactive Driving Repair

CARVE-Q：量子提议、经典认证的交互式驾驶修复

Yifan Wang

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

AI总结 针对被否决的驾驶操作，提出CARVE-Q架构，通过量子最小搜索加速修复格搜索，同时保持安全认证的经典性，实现可审计的交互修复。

Comments 9 pages, 3 figures

How Powerful are LLMs in Generating Formal Program Specifications?

大型语言模型在生成形式化程序规约方面的能力有多强？

Fanpeng Yang, Xing Li, Shuling Wang, Jie An, Zeyu Sun, Shenghua Feng, Wenhan Wang, Weiyi Wang, Naijun Zhan, Fanjiang Xu

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

AI总结 该研究引入基于Rocq的Coins评估框架，在HumanEval数据集上开展大规模研究，发现LLMs生成形式化程序规约仍具挑战，准确的规约评估是理解其能力的核心。

GraphAlignCoder: Aligning Program and Proof Graphs for Code Generation

GraphAlignCoder：对齐程序与证明图的代码生成框架

Yueke Zhang, Zihan Fang, Kevin Leach, Yu Huang

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

AI总结 GraphAlignCoder是将显式正确性结构迁移至代码生成的训练框架，通过对齐程序与证明图提升性能，在多个基准测试中优于现有方法，验证图注入与验证到代码的整合是关键。

Comments 9 pages, 3 figures

Automated Synthesis of Deterministic Cross-Domain Interfaces

确定性跨域接口的自动合成

Konstantinos Christodoulopoulos, Antonis Selentis-Boulntadakis

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

AI总结 该研究提出框架，利用LLM实现智能体与处理程序模块，自动合成跨域确定性网络的静态、动态契约，经实验验证其动态契约性能优于静态配置，且分工模式可保障模型可靠性。

What out-of-the-box LLMs can(t) do in law? A Turing test in Italian exams for lawyers, judges and notaries

开箱即用的大语言模型（LLM）在法律领域能（不能）做什么？针对意大利律师、法官和公证人考试的图灵测试

Germana Bertoli, Ilaria Amelia Caggiano, Francesca Lagioia, Riccardo Rovatti, Giovanni Sartor, Emiliano Troisi

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

AI总结 本研究通过意大利律师、法官、公证人考试的盲法图灵测试，评估开箱即用的主流LLM的法律能力，发现其在部分法律任务表现接近人类但公证人考试全部失败，明确了LLM法律能力的范围与边界。

D-MUTRA: DLT-based MUTual Remote Attestation for Multi-Agent Systems

D-MUTRA：面向多智能体系统的基于分布式账本（DLT）的相互远程证明

Adam Zahir, Vincent Lefebvre, Mark Angoustures, Milan Groshev, Carlos J. Bernardos

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

AI总结 针对多智能体系统传统远程证明的局限，本文提出基于区块链的D-MUTRA框架，实现智能体间的持续相互证明，可检测恶意软件修改，且扩展时开销可忽略。

CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification

CircuitProver：基于可复用电路证明库的智能体Lean 4定理证明框架，用于硬件验证

Ziyi Yang, Wenji Fang, Chen Chen, Zhiyao Xie, Hongce Zhang

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

AI总结 CircuitProver是基于Lean 4的智能体硬件验证框架，可自动转换硬件设计为Lean模型，通过积累可复用证明知识完成63项基准证明，比普通智能体更高效。

Formal Verification of an Out-of-Order Multiprocessor against an In-Order Weak-Memory ISA

针对顺序弱内存ISA的乱序多处理器形式验证

Janggun Lee, Jeehoon Kang

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

AI总结 研究针对顺序弱内存ISA的乱序多处理器验证问题，核心方法是设计核心规范并分两步证明，主要贡献是首次实现此类形式验证，借助核心规范简化证明，且利用LLM代理自动编写证明。

Mapping the Narrow Corridor with Large Language Models

用大语言模型绘制狭窄走廊

Ebrahim M Songhori

专题命中 代码与定理证明 ：chain-of-thought(abstract)

AI总结 研究探讨大语言模型能否将国家历史在二维空间路径的框架付诸实践，引入可重现流程，制作12国轨迹图集并比较四个模型，评估与专家指数的一致性及模型间一致性，还讨论了大语言模型注释器和人类专家偏差差异。

Show Me The Money: An Exercise in Proof-Driven Software Understanding

给我看钱：一个关于证明驱动软件理解的实践

Joseph Tafese, Karthik Nukala, Hassen Saïdi, Natarajan Shankar, Arie Gurfinkel, Giuliano Losa

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

AI总结 该研究对成熟工业C++代码库进行证明驱动软件理解，结合大语言模型、PVS和SeaHorn，对恒星区块链SDEX订单簿核心算法形式化分析，发现文档不一致，生成便于检查代码更改的工件，展示了定理证明与模型检查组合为遗留系统提供保证的途径。

Comments CAV 2026

Beyond Detection: Agentic Attack Synthesis and Simulation for Smart Contracts

超越检测：智能合约的代理攻击合成与模拟

Xianhao Zhang, Jing Sun, Zijian Zhang, Ye Liu, Zhe Hou, Jiaqi Gao, Yuqiang Sun

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

AI总结 研究智能合约漏洞利用验证问题，提出KASS多智能体框架，将自动利用生成分解为多阶段并集成多种机制，在多类智能合约上评估，能成功生成可执行利用及结构化攻击计划，验证效果优于其他工具。

WebDesignIter: Co-Evolving Design Knowledge for Repository-Level Front-End Code Generation

WebDesignIter：用于仓库级前端代码生成的协同进化设计知识

Zheng Pei, Mingwei Liu, Zhenxi Chen, Zihao Wang, Yanlin Wang

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

AI总结 研究针对前端开发仓库级代码生成问题，提出WebDesignIter框架，通过持久知识图谱融合设计知识与仓库结构，分两阶段工作，实验证明其相比基线和通用编码代理有优势，凸显设计知识对仓库级代码生成的重要性。

Collective Cognition in Hybrid Groups: A Network Science Synthesis

混合群体中的集体认知：网络科学综合研究

Babak Hemmatian, Razan Baltaji, Lav R. Varshney

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

AI总结 研究人工智能代理融入人类团队后混合系统中集体智能的产生，综合网络科学等多学科，通过注意力等视角分析不同网络中集体结果的塑造因素及扩展到混合环境的情况，确定鲁棒效应与需修正之处，得出对相关方面的启示。

Comments Non-authoritative author's version of forthcoming chapter in the Springer Nature Handbook of Hybrid Intelligence

VLM-CASE: Vision-Language Model Enabled Context-Adaptive Safety Envelopes for Anticipatory Safe Autonomous Driving

VLM-CASE：面向前瞻安全自动驾驶的视觉语言模型赋能上下文自适应安全包络

Tianjia Yang, Ke Li, Ruwen Qin, Xianbiao Hu

机构 * Department of Civil and Environmental Engineering, The Pennsylvania State University（宾夕法尼亚州立大学土木与环境工程系） ； Department of Civil Engineering, Stony Brook University（石溪大学土木工程系） 纠错

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

AI总结 针对恶劣工况下自动驾驶感知与性能退化、仅能事后响应的问题，提出基于微调VLM的上下文自适应安全包络框架，实现前瞻安全控制，在多场景仿真中性能优于基线方法。

A Comprehensive Study of Implementation Bugs in Multi-modal Agents

多模态智能体中实现错误的综合研究

Suwan Li, Lei Bu, Shangqing Liu, Yile Wang, Guangdong Bai, Fuman Xie, Kai Chen, Chang Yue

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

AI总结 针对多模态智能体实现错误缺乏系统研究的问题，收集34个智能体，从1268个问题报告中识别出158个错误，开发分类法，实现MATester工具，为多模态智能体错误分类、预防和修复提供参考。

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

CrypFormBench：评估大型语言模型在密码方案形式化分析中的能力基准

Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

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

AI总结 提出CrypFormBench基准，涵盖符号与计算安全，评估LLM在密码方案形式化分析中的五项核心能力，发现模型在生成、转换和修正方面表现有限。

Comments 23 pages, 17 figures, FSE 2026

Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language

使用宽松自然形式语言的可验证数学自动形式化

Zhicheng Hui, Lihan Xie, Xingzhi Qi, Zhehao Li, Yingjun Lan, Qinxiang Cao

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

AI总结 提出一种宽松自然形式语言作为中间目标，通过分阶段精化实现可验证的数学自动形式化，结合规则转换与LLM启发式方法，并利用领域特定策略语言生成验证条件。