大模型推理能力

Can LLMs Perform Synthesis?

LLMs能否进行合成？

Derek Egolf, Yuhao Zhou, Stavros Tripakis

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

AI总结 本文比较了LLMs与符号工具在程序合成任务中的表现，发现符号工具在多个领域均优于Qwen和GPT-5，且执行时间更短。

Leveraging Large Language Models for Generalizing Peephole Optimizations

利用大型语言模型进行通用窥视优化

Chunhao Liao, Hongxu Xu, Xintong Zhou, Zhenyang Xu, Chengnian Sun

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

AI总结 本文提出LPG框架，利用大型语言模型进行窥视优化泛化，通过闭环工作流整合符号常量泛化、结构泛化、约束放松和位宽/精度泛化，提升优化规则的正确性和通用性。

R3R: Decentralized Multi-Agent Collision Avoidance with Infinite-Horizon Safety

R3R：具有无限时间安全性的去中心化多智能体避障

Thomas Marshall Vielmetti, Devansh R. Agrawal, Dimitra Panagou

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

AI总结 R3R是首个在通信受限条件下提供无限时间安全保证的去中心化多智能体运动规划框架，通过结合安全框架与几何约束实现轨迹的可证明安全。

Comments 8 pages, LaTeX; submitted to the American Control Conference (ACC) 2026

LPO: Discovering Missed Peephole Optimizations with Large Language Models

LPO：利用大语言模型发现遗漏的窥视优化

Zhenyang Xu, Hongxu Xu, Yongqiang Tian, Xintong Zhou, Chengnian Sun

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

AI总结 本文提出LPO框架，结合大语言模型与形式验证技术，发现此前遗漏的窥视优化，实验显示其在LLVM中发现大量有效优化。

Comments Accepted at ASPLOS 2026

Journal ref Proc. 31st ACM Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2026)

A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

1001行代码的故事：潜在运行时错误引导的规范合成用于验证大规模程序

Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Haokun Li, Mingqi Yang, Xiao Yi, Shengchao Qin, Yixing Luo, Xiaofeng Li, Bin Gu, Liqiang Lu, Jianwei Yin

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

AI总结 Preguss通过结合静态分析与演绎验证，实现大规模程序的自动化形式化验证，显著提升验证效率。

Comments Accepted at OOPSLA 2026. Publication date: April 2026

Dial E for Ethical Enforcement: institutional VETO power as a governance primitive

为伦理执行而 Dial E：作为治理原语的机构 veto 权力

Subramanyam Sahoo, Vinija Jain, Aman Chadha, Divya Chaudhary

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

AI总结 本文提出机构 veto 权力作为治理原语，旨在通过正式权威阻止潜在武器化风险，推动模型去武装和伦理执行。

Comments Accepted at the AI for Peace Workshop at ICLR 2026.32 Pages and 2 Figures

Generalised Möbius Categories and Convolution Kleene Algebras

广义莫比乌斯范畴与卷积克里勒代数

James Cranch, Georg Struth, Jana Wagemaker

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

AI总结 本文提出广义莫比乌斯范畴与经典星定义的结合，用于构建卷积克里勒代数，应用于程序验证和高维重写中的代数推理。

Comments 40 pages

A2H: Agent-to-Human Protocol for AI Agent

A2H：AI代理的代理到人类协议

Zhiyuan Liang, Enfang Cui, Qian Wei, Rui She, Tianzheng Li, Minxin Guo, Yujun Cheng

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

AI总结 A2H协议通过统一机制使人类成为可发现的可解析实体，推动AI代理向人类连接的智能基础设施发展。

UAVGENT: A Language-Guided Distributed Control Framework

UAVGENT: 一种语言引导的分布式控制框架

Ziyi Zhang, Xiyu Deng, Guannan Qu, Yorie Nakahira

机构 * Department of Electrical and Computer Engineering（电气与计算机工程系） ； Carnegie Mellon University（卡内基梅隆大学） 纠错

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

AI总结 UAVGENT通过结合语言引导的任务推理与分布式反馈控制，实现了多无人机系统在复杂任务中的鲁棒性和稳定性。

Self-Supervised JEPA-based World Models for LiDAR Occupancy Completion and Forecasting

基于JEPA的世界模型的自监督LiDAR占用完成与预测

Haoran Zhu, Anna Choromanska

机构 * Department of Electrical and Computer Engineering（电气与计算机工程系） 纠错

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

AI总结 本文提出AD-LiST-JEPA，一种基于JEPA框架的自监督世界模型，用于自动驾驶中通过LiDAR数据预测未来时空演变，并在占用完成与预测任务中验证其有效性。

The Dawn of Agentic EDA: A Survey of Autonomous Digital Chip Design

代理EDA的黎明：自主数字芯片设计的综述

Zelin Zang, Yuhang Song, Aili Wang, Bingo Wing-Kuen Ling, Qi Sun, Zhen Lei, Fuji Yang, Cheng Zhuo, Jiebo Luo

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

AI总结 本文提出代理EDA的系统框架，通过认知堆栈分析前端和后端设计流程，强调神经符号优化和可信度提升的重要性。

CSLib: The Lean Computer Science Library

CSLib: 用于证明计算机科学定理和编写形式验证代码的轻量级框架

Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai

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

AI总结 CSLib是一个旨在提升Lean在计算机科学领域应用的开源框架，通过增强形式验证能力促进教育与研究。

Patterns for a New Generation: AI and Agents

新一代的模式：人工智能与代理

Joseph Corneli, Charles J. Danoff, Raymond S. Puzio, Sridevi Ayloo, Sergio Belich, Andre Wilkinson, Mary Tedeschi, Pauline Mosley

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

AI总结 本文提出利用设计模式指导代理行为，展示基于LLM的系统能读取生成模式，并探讨其在软件开发、教育等领域的应用潜力。

Comments 10 pages with 4 page appendix; to appear in Proceedings of Pattern Languages of Programs 2025

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

构造-验证：Lean 4中的应用数学基准

Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

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

AI总结 本文提出Lean 4中的构造-验证框架，通过AMBER基准评估应用数学领域中显式解决方案合成与验证能力，揭示通用模型在复杂构造任务中的优势。

Agentic Fog: A Policy-driven Framework for Distributed Intelligence in Fog Computing

代理雾：一种基于策略的雾计算分布式智能框架

Saeed Akbar, Muhammad Waqas, Rahmat Ullah

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

AI总结 本文提出了一种基于策略的雾计算框架，通过将雾节点建模为自主代理并利用势博弈理论，实现了动态环境下的高效资源管理和稳定系统收敛。

Comments 09 Pages

Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles

利用LLMs和测试或acles自动生成形式规范和验证注解

João Pascoal Faria, Emanuel Trigo, Vinicius Honorato, Rui Abreu

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

AI总结 本文利用LLMs和测试或acles自动为Dafny程序生成形式规范和验证注解，实验表明该方法在多数情况下有效，并展示了IDE集成的可行性。

Augmented Knowledge Graph Querying leveraging LLMs

增强知识图谱查询利用大语言模型

Marco Arazzi, Davide Ligari, Serena Nicolazzo, Antonino Nocera

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

AI总结 SparqLLM通过结合RAG和LLM技术，实现高效的知识图谱查询与可视化，提升非专家用户的数据交互能力。

Journal ref 2025 International Joint Conference on Neural Networks (IJCNN)

Test Case Specification Techniques and System Testing Tools in the Automotive Industry: A Review

汽车行业中测试用例规范技术与系统测试工具：综述

Denesa Zyberaj, Pascal Hirmer, Marco Aiello, Stefan Wagner

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

AI总结 本文通过系统文献综述和行业经验，综述了汽车行业测试用例规范技术与系统测试工具的挑战与需求，提出了优先级标准目录，支持技术选择和未来测试框架改进。

Comments This is the author accepted manuscript (AAM) of a paper accepted for publication in The Journal of Systems and Software (Elsevier). The final published version will be available via the journal

Human Challenge Oracle: Designing AI-Resistant, Identity-Bound, Time-Limited Tasks for Sybil-Resistant Consensus

人类挑战Oracle：设计抗AI、身份绑定、时间限制的任务以实现抗Sybil共识

Homayoun Maleki, Nekane Sainz, Jon Legarda

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

AI总结 本文提出HCO，一种通过时间限制、身份绑定挑战来对抗Sybil攻击的新型安全机制，旨在提升共识系统的抗AI能力。

Comments 21 pages, 4 tables. Initial preprint

Agentic Proof Automation: A Case Study

代理证明自动化：一个案例研究

Yichen Xu, Martin Odersky

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

AI总结 本研究提出代理证明自动化方案，利用LLM代理高效完成证明工程任务，通过案例研究展示其在形式化系统中的应用与成效。

FICO: Finite-Horizon Closed-Loop Factorization for Unified Multi-Agent Path Finding

FICO：有限时间闭环因子分解用于统一多智能体路径寻找

Jiarui Li, Alessandro Zanardi, Federico Pecora, Runyu Zhang, Gioele Zardini

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

AI总结 FICO通过系统级建模和闭环设计，实现了多智能体路径寻找问题的高效解决，显著提升了计算效率和适应性。

Trust in LLM-controlled Robotics: a Survey of Security Threats, Defenses and Challenges

对LLM控制的机器人信任：安全威胁、防御和挑战的综述

Xinyu Huang, Shyam Karthick V B, Taozhao Chen, Mitch Bryson, Thomas Chaffey, Huaming Chen, Kim-Kwang Raymond Choo, Ian R. Manchester

机构 * School of Electrical and Computer Engineering, The University of Sydney（悉尼大学电气与计算机工程学院） ； Australian Centre for Robotics and School of Aerospace, Mechanical and Mechatronic Engineering, The University of Sydney（悉尼大学机器人中心及航空航天、机械与机电工程学院） ； Department of Information Systems and Cybersecurity, University of Texas at San Antonio（德克萨斯大学圣安东尼奥分校信息系统与网络安全系） ； School of Engineering and Natural Sciences, University of Iceland（冰岛大学工程与自然科学学院） 纠错

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

AI总结 本文综述了LLM控制机器人面临的安全威胁和防御策略，强调了具身系统中恶意输出的物理风险，并提出了安全规范和多LLM监督等防御方法。

Modelling cultural evolution

文化进化建模

Fredrik Jansson

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

AI总结 本文提出了一种文化进化建模的通用模板，通过动态循环连接系统状态、认知过程、行为和宏观结果，以理解文化变化的多元但一致的机制。

Comments Chapter in Johan Lind and Anna Jon-And, eds.: Cultural Evolution from Minimal Principles, Cambridge University Press

Counterfactual Harm: A Counter-argument

反事实伤害：一种反论点

Amit N. Sawant, Mats J. Stensrud

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

AI总结 本文指出基于反事实的伤害定义在多治疗选项场景下会产生不一致性，提出基于预期效用的干预定义以确保治疗排名的传递性。

When Natural Strategies Meet Fuzziness and Resource-Bounded Actions (Extended Version)

当自然策略与模糊性及资源受限行动相遇（扩展版本）

Marco Aruta, Francesco Improta, Vadim Malvone, Aniello Murano

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

AI总结 本文提出HumanATLF逻辑，结合模糊语义和资源受限行动，解决自然策略中成本和不确定性的问题，并证明模型检查的复杂性。

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL

为Isabelle/HOL上的神经定理证明设计的最小化证明语言

Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li, Conrad Watt

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

AI总结 本文提出Minilang，一种简洁的证明语言，用于提升神经定理证明在形式证明中的性能。

Comments Accepted in OOPSLA'26

Reconsidering Conversational Norms in LLM Chatbots for Sustainable AI

重新审视LLM聊天机器人中的会话规范以实现可持续AI

Ronnie de Souza Santos, Cleyton Magalhães, Italo Santos

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

AI总结 本文探讨了LLM聊天机器人中会话规范对可持续性的影响，指出交互行为、对话模式、用户习惯及上下文积累是影响系统能耗的关键因素，需重新设计交互方式以实现可持续发展。

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification

Kimina Lean Server: 一种高性能的大型验证用Lean服务器

Marco Dos Santos, Hugues de Saxcé, Haiming Wang, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu, Jia Li

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

AI总结 Kimina Lean Server通过高效的并行处理和缓存机制，提升了大规模验证和数据提取的效率，适用于强化学习管道中的高性能验证任务。

Comments Accepted to the 5th MATH-AI Workshop at NeurIPS 2025

Beyond the Hype: Critical Analysis of Student Motivations and Ethical Boundaries in Educational AI Use in Higher Education

超越 hype：批判性分析高等教育中教育 AI 使用的学生动机与伦理边界

Adeleh Mazaherian, Erfan Nourbakhsh

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

AI总结 本文探讨高等教育中学生使用 AI 的动机与伦理问题，指出学生普遍依赖 AI 工具但缺乏指导，女性更关注 AI 滥用风险，提出通过 AI 文化课程和评估改革促进负责任的 AI 采用。

Comments 14 pages, 3 figures

From Show Programmes to Data: Designing a Workflow to Make Performing Arts Ephemera Accessible Through Language Models

从节目到数据：设计一种工作流，通过语言模型使表演艺术的临时性资料可访问

Clarisse Bardiot, Pierre-Carl Langlais, Bernard Jacquemin, Jacob Hart, Antonios Lagarias, Nicolas Foucault, Aurélie Lemaître-Legargeant, Jeanne Fras

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

AI总结 本文提出利用多模态语言模型和本体推理模型，将戏剧节目转化为结构化数据，以提升文化遗产资料的可访问性和分析能力。

Comments 19 pages, 8 figures, 5 tables, 17 references