大模型推理能力

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多智能体框架，将自动利用生成分解为多阶段并集成多种机制，在多类智能合约上评估，能成功生成可执行利用及结构化攻击计划，验证效果优于其他工具。

Correctness, confidence, and context: Framing software assurance in the AI age

正确性、置信度与上下文：在人工智能时代构建软件保障

Mary Shaw

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

AI总结 探讨软件工程中正确性相关挑战，指出传统方法与生成式人工智能在软件保障上的差异，呼吁系统思考保障技术，做出明智选择。

Comments 12 pages, 10 figures, text for invited keynote at FSE 2026 in Montreal. Revised after the conference to reflect discussions at the conference

Thermodynamic Limits of Proof

物理计数的计算复杂性

Tristan Simas

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

AI总结 研究物理计数的计算复杂性，提出决策商 Q 作为最小抽象，并证明多个复杂性理论结果。

Comments Main PDF: 35 pages, 4 tables. Supplementary: 26 pages, 2 tables. Lean 4 release artifact available at https://doi.org/10.5281/zenodo.18140965

SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis

通过负测试作为完整性信号的强化学习用于形式规范综合

Zhechong Huang, Zhao Zhang, Zeyu Sun, Huifeng Sun, Yingfei Xiong

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

AI总结 本文提出SpecRL框架，利用负测试比例作为规范完整性的信号，提升规范强度和验证成功率，实验显示其在不同模型规模上表现优异。

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工具，为多模态智能体错误分类、预防和修复提供参考。

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

Evolving Quantum Error-Correcting Encodings for Molecular Simulation

面向分子模拟的量子纠错编码演化

Kenny Heitritter, James Brown, Tarini Hardikar

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

AI总结 利用LLM驱动的演化程序合成，发现分子模拟中距离5和6的广义超快编码，并进一步通过压缩导向搜索获得结构化循环构造器。

Comments 16 pages including appendices, 4 figures, 8 tables

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启发式方法，并利用领域特定策略语言生成验证条件。

Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering

形式化方法引导的Vibe编码：通过模型驱动工程关闭AI生成安全关键软件的验证循环

Ran Wei, Le Zhu, Haochi Wang, Jim Woodcock, Fang Yan, Simon Foster, Xiangyang Ji

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

AI总结 提出Forge管道，结合Vibe编码与模型驱动工程，通过多种形式化验证（Dafny、CSP、Isabelle）迭代修正LLM生成的Java代码，生成符合安全标准的验证证据。

Statistical Proof as a Window into Human-AI Collaboration: Practical Insights and a Community Agenda

统计证明作为人机协作的窗口：实践见解与社区议程

Xiaojing Sun, Huayu Tang, Buxin Su, Mateo Matijasevick, Chong Wu, Fei Xue, Bingxin Zhao

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

AI总结 通过统计证明任务，发现当前通用大语言模型在精确定义问题下可执行技术组件，但在开放或长链推理中不可靠，提出人机协作中人类专业知识应聚焦于问题构建与验证。

SHACR: A Graph-Augmented Semi-Autonomous Framework for Multi-Class Conflict Resolution in Smart Home IoT Automation

SHACR：一种用于智能家居物联网自动化中多类冲突解决的图增强半自主框架

Leena Marghalani, Walid Aljoby, Suayb S. Arslan

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

AI总结 提出SHACR框架，通过有向知识图谱将冲突检测从文本推理转化为确定性多跳图遍历，统一逻辑、语义和物理冲突，结合LLM实现闭环工作流，在203条规则测试中F1从0.59提升至0.95。

From Production SIEM to Reusable Cybersecurity Artifacts

从生产SIEM到可复用的网络安全工件

Sidnei Barbieri, Leonardo Vaz de Meneses, Ágney Lopes Roth Ferraz, Wagner Comin Sonaglio, Lourenço Alves Pereira Júnior

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

AI总结 提出一种从生产金融安全运营中心提取、匿名化、结构化并验证SIEM数据的方法，生成可复用的研究工件，并通过训练和测量实验验证其隐私-效用边界。

ARENA: An Architecture for Measuring the Transferability of Autonomous Cyber Defense

ARENA: 一种衡量自主网络防御可迁移性的架构

Sidnei Barbieri, Ágney Lopes Roth Ferraz, Wagner Comin Sonaglio, Gioliano de Oliveira Braga, Henrique Curi de Miranda, Lourenço Alves Pereira Júnior

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

AI总结 针对生产环境安全运营中心数据难以公开的问题，提出一种从私有生产数据中提取、匿名化、结构化并验证SIEM数据的方法，在保护隐私的同时保留任务相关结构，并通过两个应用案例验证了隐私-效用边界。

The Hitchhiker's Guide to Program Analysis, Part III: Mostly Harmless LLMs

程序分析漫游指南，第三部分：基本无害的LLMs

Haonan Li, Tianyang Zhou, Manu Sridharan, Hang Zhang, Zhiyun Qian

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

AI总结 提出Evident系统，将LLM用于构建分析框架，后端形式化验证错误状态不可达，在151个真实警告中正确分类，未漏报任何确认漏洞。

DIG: Oracle-Guided Directed Input Generation for One-Day Vulnerabilities

DIG：面向单日漏洞的Oracle引导定向输入生成

Andrew Bao, Haochen Zeng, Peng Chen, Stephen McCamant, Pen-Chung Yew

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

AI总结 针对补丁延迟或未完全部署导致的单日漏洞风险，提出Oracle引导的定向输入生成方法DIG，利用补丁揭示触发条件，通过LLM合成Oracle并引导生成器进化与定向模糊测试，在138个真实CVE上触发80个漏洞，超过现有技术。

IDDMBSE: Integrating Data-Driven and Model-Based Systems Engineering for Trusted Autonomous Cyber-Physical Systems

IDDMBSE：集成数据驱动和基于模型的系统工程用于可信自主网络物理系统

John S. Baras, Sai Sandeep Damera, Ryan Matheu, Clinton Enwerem, Praveen M. S. Kumar

机构 * Institute for Systems Research, University of Maryland, College Park（系统研究所，马里兰大学，College Park） 纠错

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

AI总结 提出IDDMBSE方法，将MBSE V流程与数据驱动循环结合，通过开源工具链PERFECT、TRADES-X和VERITAS实现，在自主地面机器人全生命周期验证其有效性。

Comments 9 pages, 11 figures. This work has been submitted to the IEEE for possible publication

GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation

GCD: 乱码、修正、证明——修复并验证Go语言的扩展GCD实现

Linard Arquint

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

AI总结 本文修复了Go标准库中extendedGCD实现的两个偏差，并使用Gobra和Lean进行了形式化验证，证明了正确性和终止性，同时发现AI代理可辅助验证过程。

NeuroSymbolic Robustness Analysis for Discrete Systems with Respect to Transition Deviations

针对转移偏差的离散系统神经符号鲁棒性分析

Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

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

AI总结 提出一种神经符号计算框架，利用大语言模型推断可行偏差转移集，再通过符号层计算离散鲁棒性保证，以解决传统方法可扩展性差和保守性问题。

Neuroforger: certified violation witnesses for smart contracts verification via LLMs

Neuroforger: 通过大语言模型为智能合约验证生成认证违规见证

Massimo Bartoletti, Enrico Lipparini

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

AI总结 针对自然语言属性歧义和LLM回答无正确性保证的问题，提出一种结合LLM、类型检查和具体执行的工作流，通过引入扩展Solidity的抽象类型形式规范语言，生成并验证违规见证（反例）。

On some open problems in commutative algebra resolved by Rethlas

关于由Rethlas解决的交换代数中一些开放问题

Jiedong Jiang, Yixiao Li, Zeming Sun, Yuefeng Wang, Liang Xiao, Jiahong Yu

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

AI总结 本文报告了使用Rethlas自然语言自动推理系统解决（证明或反驳）的交换代数及相关领域的一系列开放问题，并给出了精确陈述和自包含证明。

Comments 13 pages. AI-generated, human verified

Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust

Heimdall: 形式化验证的遗留 eBPF 程序到 Rust 的自动迁移

Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari, Gang Tan

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

AI总结 本文提出 Heimdall，一个利用大语言模型将遗留 libbpf C 程序自动翻译为 Aya Rust 的管道，通过静态分析和符号执行确保迁移后程序行为等价，并修复了 eBPF 程序中六类源级漏洞，包括未报告的信息泄露。

Tacit Signal Infrastructure: Towards AI Systems that Model Expert Sensing Over Time

隐性信号基础设施：迈向随时间建模专家感知的AI系统

Annie Yuan

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

AI总结 本文提出隐性信号基础设施，通过长期认知操作和认知运营管理器，使AI系统能够建模专家随时间变化的隐性感知，从而超越显性知识处理。

Comments 17 pages, 2 figures

QwenSafe: Multimodal Content Rating Description Identification via Preference-Aligned VLMs

QwenSafe: 通过偏好对齐的视觉语言模型实现多模态内容评级描述识别

Dishanika Denipitiyage, Aruna Seneviratne, Suranga Seneviratne

机构 * University of Sydney（悉尼大学） ； University of New South Wales（新南威尔士大学） 纠错

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

AI总结 本文提出QwenSafe，一种通过联合推理应用元数据和截图来自动识别苹果定义的内容评级描述（CRDs）的视觉语言模型，通过引入metadata2CRD数据构建管道和直接偏好优化（DPO）提升模型预测准确性，实验结果显示QwenSafe在二元CRD分类中显著优于现有模型。