大模型推理能力

PAVE: Premise-Aware Validation and Editing for Retrieval-Augmented LLMs

PAVE：基于前提的验证与编辑用于检索增强的大语言模型

Tianyi Huang, Caden Yang, Emily Yin, Eric Wang, Michael Zhang

机构 * Ryquo ； App-In Club 纠错

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

AI总结 PAVE通过在推理阶段验证和编辑检索到的证据，提高检索增强大语言模型的回答一致性。在两个证据基础问答任务中，PAVE在跨度基础基准上提升了32.7个准确率点。

Comments Accepted at the ICLR 2026 Workshop on Logical Reasoning of Large Language Models

Auditing and Decomposing Feedback-Driven Evolution in LLM Test Generation under the Oracle Problem

在神谕问题下对LLM测试生成中反馈驱动演化的审计与分解

Yunhao Liang, Chengguang Gan, Ruixuan Ying, Hanjun Wei, Zhe Cui, Shiwen Ni

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

AI总结 该研究针对LLM测试生成中反馈驱动演化的神谕问题，通过多任务实验发现单一神谕会膨胀演化增益，提出审计-安慰剂协议以分离验证器人工制品等，为相关评估提供改进方案。

A Nonmonotone Real-Rootedness Set for Symmetric Imaginary Shifts

Vasily Stodolsky

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

Comments 7 pages, 1 table. AI Research Artifact with material AI use and author accountability disclosed in the paper. Corresponds to Zenodo v0.1.3, DOI: 10.5281/zenodo.21922629

Formal Safety Verification for Nonlinear Systems with Generative Barrier Certificate

基于生成式障碍证书的非线性系统形式化安全验证

Mengxin Ren, Hanrui Zhao

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

AI总结 该研究针对非线性系统安全验证中障碍证书推导计算成本高的问题，提出基于大语言模型的生成式框架，将BMI问题转化为LMI测试，实现了远超传统方法的速度与性能提升。

KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

KBSpec：基于演化领域知识库的LLM驱动形式化规约生成

Wenhan Wang, Zeyu Sun

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

AI总结 提出KBSpec方法，利用外部官方文档和内部验证器反馈的双源知识增强LLM，通过自演化知识库持续更新成功轨迹，无需调参或标注数据，在JML规约生成上验证通过率提升10-25%。

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实现智能体与处理程序模块，自动合成跨域确定性网络的静态、动态契约，经实验验证其动态契约性能优于静态配置，且分工模式可保障模型可靠性。

CognixShield: PoV-Guided Vulnerable API Usage Detection in Large Codebases via LLMs

CognixShield：基于LLM的、面向大型代码库的PoV引导式漏洞API使用检测

Quanzhi Fu, Wang Lingxiang, Wenjia Song, Gelei Deng, Yi Liu, Dan Williams, Ying Zhang

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

AI总结 CognixShield是一款LLM驱动的框架，通过保留语义的AST碎片化、感知漏洞的多智能体RAG、PoV引导的语义推理三个核心组件，在57个Java应用上实现了优于现有工具的漏洞API使用检测性能。

Comments accepted in ESEM 2026

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法律能力的范围与边界。

Introducing Large Language Models into the Design Flow of Time-Sensitive Networking

将大语言模型引入时间敏感网络的设计流程

Rubi Debnath, Luxi Zhao, Mohammadreza Barzegaran, Paul Pop, Sebastian Steinhorst

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

AI总结 针对配置优化TSN网络的挑战，通过跨模型案例研究评估现有大语言模型能力，提出LLM辅助编排框架，介绍构建模块与管道，分析实际部署机会与局限，为评估LLM辅助TSN编排可行性提供路线图。

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项基准证明，比普通智能体更高效。

On Some Problems from the Kourovka Notebook

关于《库罗夫卡笔记本》中的一些问题

Wouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison

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

AI总结 本文解决《库罗夫卡笔记本》中八个群论问题，包括构建特定群、证明元素乘积取值情况、说明群阶与统计量不能确定单性、构造算子，还涉及确定生成群、证明幂图性质、探讨子群格情况及反驳秩不等式，且由形式推理主体在Lean中完成。

Comments 21 pages. Lean 4 formalisation: https://github.com/pitmonticone/Kourovka. v2: Expands the appendix with an account on problem selection and adds the MathOverflow provenance of Problem 18.50

FlexNGIA 2.0: Redesigning the Internet with Agentic AI -- Protocols, Services, and Traffic Engineering Designed, Deployed, and Managed by AI

FlexNGIA 2.0：利用智能AI重新设计互联网——由AI设计、部署和管理的协议、服务和流量工程

Mohamed Faten Zhani, Younes Korbi, Yamen Mkadem

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

AI总结 面对沉浸式通信需求等带来的契机，FlexNGIA 2.0利用基于大语言模型的AI智能体自主编排、配置和演进网络，可动态调整多种网络方案。通过初步实验证明其能力，为新型智能AI驱动网络奠基，也指出了相关关键研究挑战。

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

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