大模型推理能力

Decodable but Not Faithful: Coupling Natural-Language Rationales to Programmatic Verifiers

可解码但不忠实：将自然语言理由与程序化验证器耦合

Vatsal Ananthula, Adarsh Kumarappan

机构 * AI4Math 纠错

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

AI总结 提出验证器耦合推理框架，通过一致性训练使验证器信息可从理由表示中解码，但发现可解码性不保证忠实生成，在多个任务中验证了该差距。

Comments Accepted to the ICML 2026 AI4Math Workshop as a poster

Explaining is Harder Than Predicting Alone: Evaluating Concept-based Explanations of MLLMs as ICL Visual Classifiers

解释比单独预测更难：评估基于概念的MLLM解释作为ICL视觉分类器

Carmen Quiles-Ramírez, Leticia L. Rodríguez, Nicolás Martorell, Natalia Díaz-Rodríguez

专题命中 代码与定理证明 ：reasoning(abstract)；chain-of-thought(abstract)；分类 cs.CL、cs.AI、cs.LG

AI总结 本文通过五种形式化程度递增的条件，系统评估多模态大语言模型在少样本上下文学习中的基于概念的可解释性，发现解释比预测更难，且强制生成形式化解释会降低预测准确性。

Comments Accepted to the CompLearn Workshop at ICML 2026

Shrinking the Generation-Verification Gap with Weak Verifiers

缩小生成-验证差距的弱验证器

Jon Saad-Falcon, E. Kelly Buchanan, Mayee F. Chen, Tzu-Heng Huang, Brendan McLaughlin, Tanvir Bhathal, Shang Zhu, Ben Athiwaratkun, Frederic Sala, Scott Linderman, Azalia Mirhoseini, Christopher Ré

机构 * Stanford University（斯坦福大学） ； University of Wisconsin-Madison（威斯康星大学麦迪逊分校） ； Together AI 纠错

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

AI总结 Weaver通过结合多个弱验证器，有效缩小生成-验证差距，提升验证性能至接近理想验证器水平。

Comments Annual Conference on Neural Information Processing Systems (NeurIPS) 2025

MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

MINIF2F-DAFNY: 通过自动主动验证的LLM引导数学定理证明

Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Sean B. Holden

机构 * University of Cambridge, Cambridge, UK（剑桥大学） ； Amazon Web Services, London, UK（亚马逊网络服务（伦敦）） ； Amazon Web Services, Boston, USA（亚马逊网络服务（波士顿）） 纠错

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

AI总结 提出首个将数学基准miniF2F翻译到自动主动验证器Dafny的数据集，评估8个LLM的证明生成能力，最佳模型Claude Opus 4.6达到62.7%的累积通过率，比空证明基线提升23.8个百分点。

AXE: Grey-Box Exploitability Confirmation for Localized Vulnerability Reports

AXE：针对局部漏洞报告的灰盒可利用性确认

Amirali Sajadi, Tu Nguyen, Kostadin Damevski, Preetha Chatterjee

机构 * Virginia Commonwealth University（弗吉尼亚 Commonwealth 大学） 纠错

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

AI总结 提出多智能体框架AXE，利用CWE分类和代码位置等轻量级元数据，通过解耦规划、代码探索和动态执行反馈实现Web漏洞利用，在CVE-Bench上达到30%成功率，比黑盒基线提升3倍。

A Study of Belief Revision Postulates in Multi-Agent Systems (Extended Version)

多智能体系统中信念修正公设的研究（扩展版）

Michael Thielscher, Tran Cao Son

机构 * University of New South Wales（新南威尔士大学） ； New Mexico State University（新墨西哥州立大学） 纠错

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

AI总结 研究认知规划中的信念修正问题，将经典AGM信念修正公设推广到多智能体环境，提出广义全交多智能体信念修正算子，并讨论迭代修正公设的推广及事件模型修正算子。

A Neurosymbolic Approach to Natural Language Formalization and Verification

一种用于自然语言形式化和验证的神经符号方法

Chenyang An, Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Victor Heorhiadi, Marc Hudak, Dejan Jovanović, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamarić, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, Jianan Yao

机构 * Amazon Web Services（亚马逊网络服务） ； University College London（伦敦大学学院） ； University of Toronto（多伦多大学） ； Queen Mary University of London（伦敦大学女王学院） 纠错

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

AI总结 针对大型语言模型缺乏形式正确性保证的问题，提出神经符号方法ARc，通过使用带人工指导的大型语言模型形式化自然语言政策，并在推理时验证逻辑正确性，实现高健全性和低误报率，还能产生可审计工件。

Comments 28 pages, 11 figures

TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability

TCS-BENCH：评估最先进生成式AI理论计算机科学研究能力的基准

Vincent Cohen-Addad, Dimitris Paparas, Ernest van Wijland, Max Springer, Julien Canitrot-Paradis, Honghao Lin, David Woodruff, Adarsh Kumarappan, Rajesh Jayaram, Rudrajit Das, Lalit Jain, Ola Svensson, Silvio Lattanzi, Mislav Balunovic, Theophane Weber, Vahab Mirrokni

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

AI总结 研究人员推出TCS-Bench基准，基于STOC、FOCS、SODA论文的定理证明任务评估LLMs，结合验证智能体，参考验证器在专家标注集准确率超90%，为评估生成式AI的TCS研究能力提供工具

OS-Sentinel: Towards Safety-Enhanced Mobile GUI Agents via Hybrid Validation in Realistic Workflows

OS-Sentinel: 通过现实工作流中的混合验证实现安全增强的移动GUI代理

Qiushi Sun, Mukai Li, Zhoumianze Liu, Zhihui Xie, Fangzhi Xu, Zhangyue Yin, Kanzhi Cheng, Zehao Li, Zichen Ding, Qi Liu, Zhiyong Wu, Zhuosheng Zhang, Ben Kao, Lingpeng Kong

机构 * The University of Hong Kong（香港大学） ； Fudan University（复旦大学） ； Shanghai AI Laboratory（上海人工智能实验室） ； Nanyang Technological University（南洋理工大学） ； Nanjing University（南京大学） ； Shanghai Jiao Tong University（上海交通大学） 纠错

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

AI总结 OS-Sentinel通过结合形式验证器和VLM上下文判断者，提升移动GUI代理的安全性，实验显示在多个指标上优于现有方法。

Comments ACL 2026 (Oral) & Best Paper at AIWILD @ ICLR 2026

Left-right asymmetry in predicting brain activity from LLMs' representations emerges with their formal linguistic competence

在LLM表示中预测脑活动的左右不对称性随着其正式语言能力的出现而出现

Laurent Bonnasse-Gahot, Christophe Pallier

机构 * Centre d’Analyse et de Mathématique Sociales CNRS, EHESS, Paris, France（分析与数学社会中心 CNRS，EHESS，巴黎，法国） ； Cognitive Neuroimaging Unit CNRS, INSERM, CEA, Neurospin Center, 91191 Gif-sur-Yvette, France（认知神经成像单元 CNRS，INSERM，CEA，Neurospin中心，法国91191 Gif-sur-Yvette） 纠错

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

AI总结 研究发现LLM的正式语言能力与大脑预测活动的左右不对称性同步发展，且与算术或世界知识任务无关。

Journal ref Neurobiology of Language 2026

Agentic AI for Commercial Insurance Underwriting with Adversarial Self-Critique

用于商业保险承保的具有对抗性自我批评的智能体人工智能

Joyjit Roy, Samaresh Kumar Singh

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

AI总结 研究针对商业保险承保中AI可靠性问题，提出含对抗性自我批评机制的人在回路智能体系统，开发故障模式分类法。实验表明该机制降低幻觉率、提高准确率，还确保人类权威，为受监管领域安全部署AI提供模型。

Comments 9 pages, 8 figuers, 6 tables, Presented at 9th International Conference on Modern Computing, Networking and Applications (MCNA2026)

Journal ref 2026 International Conference on Modern Computing, Networking and Applications (MCNA)

Guidelines for the Annotation and Visualization of Legal Argumentation Structures in Chinese Judicial Decisions

中国司法判决中法律论证结构的标注与可视化指南

Kun Chen, Xianglei Liao, Kaixue Fei, Yi Xing, Xinrui Li

机构 * Law School, Nanjing University（南京大学法学院） 纠错

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

AI总结 提出一个系统化、可操作的标注框架，用于表示司法判决中的法律论证结构，支持大规模司法推理分析和法律论证挖掘。

Comments This Guideline has been developed through revision and refinement based on the first edition. The element label system has been adjusted, and the annotation granularity and annotation workflow have been further optimized

The Human-AI Substitution Principle: When will you be replaced by AI in your organization?

人类-人工智能替代原则：在你的组织中，你何时会被人工智能取代？

Bonny Banerjee, Shreya Singh

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

AI总结 研究人类员工何时被人工智能取代，提出HAT分析模型，编码人类技能与人工智能能力的经济不对称，推导多因素对人机替代的影响，得出替代原则，揭示其引发的组织变化及中层管理与高技能工人的脆弱性，统一相关理论。

Human agency in initial human-AI proof formalization workflows

表征初始人机交互的证明形式化工作流

Katherine M. Collins, Simon Frieder, Jonas Bayer, Jacob Loader, Jeck Lim, Peiyang Song, Fabian Zaiser, Lexin Zhou, Shanda Li, Sam Looi, Joshua B. Tenenbaum, Umang Bhatt, Adrian Weller, Jose Hernandez-Orallo, Cameron E. Freer, Valerie Chen, Ilia Sucholutsky

机构 * Massachusetts Institute of Technology（麻省理工学院） ； University of Cambridge（剑桥大学） ； Princeton University（普林斯顿大学） ； University of Oxford（牛津大学） ； Caltech（加州理工学院） ； Carnegie Mellon University（卡内基梅隆大学） ； Universitat Politècnica de València（瓦伦西亚理工大学） ； New York University（纽约大学） 纠错

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

AI总结 通过混合方法分析，研究人们在形式化证明过程中对AI工具的需求、障碍及实际使用模式，发现AI辅助能提高形式化准确率且用户偏好多样但普遍希望保持人类对证明发现过程的高层控制。

Comments Updated working paper

Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Goedel-Code-Prover：面向开放状态的最新代码验证的分层证明搜索

Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin

机构 * ETH Zürich（苏黎世联邦理工学院） ； Princeton Language and Intelligence（普林斯顿语言与智能实验室） ； Department of Computer Science, Princeton University（普林斯顿大学计算机科学系） ； MiroMind 纠错

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

AI总结 本文提出Goedel-Code-Prover框架，通过分层证明搜索提升Lean4中代码验证的自动化水平，实现62%的成功率，优于现有基线方法。

Comments Published as a COLM paper

Screenshots or Tools? Eliciting Tool Use and Managing Multimodal Context in Hybrid GUI-MCP Computer-Use Agents

截图还是工具？在混合GUI-MCP计算机使用智能体中引出工具使用并管理多模态上下文

Siqi Fan, Minghao Li, Xiaoqian Ma, Wenhui Tan, Xiusheng Huang, Juntong Wu, Liujie Zhang, Shuo Shang, Weihang Chen

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

AI总结 该研究针对混合GUI-MCP计算机使用智能体，发现工具使用存在采用缺口，通过调整工具奖励与上下文压缩优化，提升了智能体性能并降低输入成本。

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

超越图书馆：用于自动形式化研究数学的智能体框架

Arshia Soltani Moakhar, Iman Gholami, Max Springer, Mahdi JafariRaviz, MohammadTaghi Hajiaghayi

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

AI总结 提出一种基于通用编码大语言模型的智能体自动形式化框架，通过多智能体管道和辅助引理技术，成功形式化了PutnamBench和STOC论文中的主要定理，其中两个证明无需额外公理。

Comments preprint

An Autonomous Scientific Knowledge Generation Framework for AI-Driven Scientific Discovery

一种用于人工智能驱动科学发现的自主科学知识生成框架

Dibakar Datta

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

AI总结 该研究提出自主科学知识生成框架，整合多种技术将科学出版物转化为适用于人工智能的知识库，以电光材料为例进行验证，实现从文献到知识库的转变，为人工智能驱动的科学发现提供了可扩展、领域独立的基础。

Comments 32 pages, 6 figures

Conformal Cascade: Distribution-Free Accuracy Guarantees for Multi-Tier LLM Inference

共形级联：多层大语言模型推理的无分布精度保证

Yifan Dou, Shikan Lian, Shibo Li

机构 * Department of Computer Science, Florida State University（佛罗里达州立大学计算机科学系） 纠错

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

AI总结 研究针对LLM级联推理成本高、置信分数校准不当等问题，提出共形级联框架，以共形预测集大小为推迟规则，提供无分布精度保证，在多基准测试中表现优于启发式级联，且无需模型训练，仅需黑盒API访问。

Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

迈向可验证的Transformer：求解器可检查的电路解释

Neel Somani

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

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

AI总结 提出Verifiable Transformers框架，通过将任务局部Transformer电路转化为有界、求解器可检查的声明，实现电路属性的形式化验证。

Comments 23 pages. v2: adds GPT-2-scale verified distillation (three-edge verified quote circuit), LayerNorm removal for sparsemax models, and gated localization protocols

Guardians and Offenders: A Survey on Harmful Content Generation and Safety Mitigation of LLM

守护者与违规者：大语言模型有害内容生成与安全缓解研究综述

Chi Zhang, Changjia Zhu, Junjie Xiong, Xiaoran Xu, Lingyao Li, Yao Liu, Zhuo Lu

机构 * University of South Florida（佛罗里达州立大学） ； Missouri University of Science and Technology（密苏里科技大学） 纠错

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

AI总结 综述大语言模型在内容创作中带来的风险与挑战，系统回顾相关研究，提出危害与防御统一分类法，分析越狱策略，评估缓解措施，指出评估局限，明确未来研究方向以推动语言技术稳健且符合伦理发展。

The Lattice Representation Hypothesis of Large Language Models

大语言模型的晶格表示假说

Bo Xiong

机构 * Stanford University（斯坦福大学） 纠错

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

AI总结 本文提出大语言模型的晶格表示假说，通过嵌入几何将概念层次和逻辑运算统一到线性表示中，实验表明LLM嵌入编码概念晶格及其逻辑结构。

Comments Published at ICLR 2026

A Survey on Hypergame Theory: Modelling Misaligned Perceptions and Nested Beliefs for Multi-Agent Systems

关于超博弈理论的综述：为多智能体系统建模错位感知与嵌套信念

Vince Trencsenyi, Agnieszka Mensfelt, Kostas Stathis

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

AI总结 本文综述了超博弈理论在多智能体系统中的应用，分析了其建模错位感知与嵌套信念的能力及现有研究中的趋势与挑战。

The LLMbda Calculus: AI Agents, Conversations, and Information Flow

LLMlambda 计算：人工智能代理、对话与信息流

Zac Garby, Andrew D. Gordon, David Sands

机构 * University of Nottingham, UK（诺丁汉大学） ； University of Edinburgh, UK（爱丁堡大学） ； Chalmers University of Technology（查尔姆斯理工大学） ； The University of Gothenburg, Sweden（哥德堡大学） 纠错

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

AI总结 本文提出了一种无类型的lambda计算模型，用于形式化描述和验证人工智能代理中对话和信息流的安全性。

To Use AI as Dice of Possibilities with Timing Computation

将AI用作带有时序计算的可能性骰子

Jia Li, Vipin Kumar, Rui Zhang

机构 * Department of Surgery, University of Minnesota（明尼苏达大学外科系） ； Department of Computer Science & Engineering, University of Minnesota（明尼苏达大学计算机科学与工程系） 纠错

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

AI总结 本文提出基于动词的范式，定义时序计算和可能性，使AI能作为实现思维语法的工具，并在乳腺癌患者数据上自动发现临床轨迹和反事实时序推断。

Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

Aria: 基于依赖图的检索与迭代自动形式化智能体

Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, Bin Dong

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

AI总结 提出Aria系统，通过两阶段思维图过程递归分解定理陈述为依赖图并构建形式化，结合AriaScorer验证语义正确性，在ProofNet、FATE-X和同调猜想数据集上显著超越现有方法。

Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

并非所有证明都平等：超越正确性的LLM证明质量评估

Ivo Petrov, Jasper Dekoninck, Dimitar I. Dimitrov, Martin Vechev

机构 * INSAIT（INSAIT研究所） ； Sofia University "St. Kliment Ohridski"（索菲亚大学"圣克莱孟·奥赫里迪斯基"） ； ETH Zurich（苏黎世联邦理工学院） 纠错

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

AI总结 本文提出ProofRank基准，评估证明的简洁性、计算便捷性、认知简单性、多样性及适应性，揭示正确性之外的证明质量差异及优劣权衡。

Comments 9 main text pages, 36 total pages, Accepted at ICML 2026 AI for Math workshop

Evaluating LLM-Driven Summarisation of Parliamentary Debates with Computational Argumentation

评估基于大语言模型的议会辩论总结的论证内容

Eoghan Cunningham, Derek Greene, James Cross, Antonio Rago

机构 * School of Computer Science, University College Dublin（都柏林大学计算机科学学院） ； School of Politics and International Relations, University College Dublin（都柏林大学政治与国际关系学院） ； Department of Informatics, King’s College London（伦敦国王学院信息学院） 纠错

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

AI总结 本文提出一种评估议会辩论总结的框架，通过计算论证方法评估总结对辩论论证内容的忠实性，以欧洲议会辩论为例验证方法有效性。

Comments Accepted at KR'26 In The Wild Track. Camera Ready with additional supplementary materials

Pseudo-Formalization for Automatic Proof Verification

伪形式化用于自动证明验证

Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma

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

AI总结 本文提出了一种名为伪形式化的证明格式，该格式在保持自然语言灵活性的同时，保留了形式证明的模块性和精确性，通过块验证算法实现了对自然语言证明的高效验证，其在错误发现的精度和召回率上优于现有基线方法。

Comments 31 pages, code available at https://github.com/Slim205/pseudo-formalization

Intelligence as Managed Autonomy: Failure, Escalation, and Governance for Agentic AI Systems

智能作为受管自主：代理型AI系统的失败、升级与治理

Srini Ramaswamy

机构 * DNRS.ai USA（DNRS.ai美国公司） 纠错

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

AI总结 本文提出SMARt模型，通过形式化能力检测认知漂移、暂停推理、尝试恢复并在可靠性下降时放弃控制，以解决自主AI系统中的幻觉和持续不合理行为问题。

Comments This peer-reviewed paper is to appear in the Journal of Intelligent and Robotic Systems