大模型推理能力

Towards Risk-free AI Agent Deployment

迈向无风险的AI智能体部署

Yintong Huo, Rangeet Pan, Abhik Roychoudhury

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

AI总结 针对LLM智能体部署的安全、合规等风险，本文提出以智能体轨迹为基础，将测试与调试作为系统性研究方向，提炼部署就绪检查表并指出需解决的开放性问题，推动可信智能体部署。

Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs

证明是否以其应有的方式被证明？《几何原本》元素证明的忠实形式化

Tadd Mao, Tianjun Zhong, Dhruva Arekar, Yuming Feng, One An, Jiani Huang, Xujie Si, Ziyang Li

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

AI总结 本研究提出满足五项必要条件的Pistis智能体式证明搜索方法，通过OrderDecompose分治搜索生成欧几里得《几何原本》前三卷的忠实形式化Lean证明，其性能优于基线方法，可作为证明检查工具。

Comments Preprint. 18 pages, 14 figures, 7 tables

Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement

面向安全的大语言模型智能体：规范、验证与执行的综述

Pierre Dantas, Lucas Cordeiro, Ehsan Nowroozi, Tihanyi Norbert

机构 * The University of Manchester（曼彻斯特大学） ； The University of Greenwich（格林威治大学） ； Technology Innovation Institute（技术创新研究院） 纠错

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

AI总结 该综述针对LLM智能体缺乏形式化任务级安全保障的问题，通过系统分析38项研究，揭示规范瓶颈等四项关键发现，提出三级分类体系与十大问题研究议程，为可信智能体AI研究提供方向。

Comments 28 pages

MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving

Mechanic：基于遗憾的正式分解工作流用于自动定理证明

Ruichen Qiu, Yichuan Cao, Junqi Liu, Dakai Guo, Xiao-Shan Gao, Lihong Zhi, Ruyong Feng

机构 * Academy of Mathematics and Systems Science, CAS（数学与系统科学研究院，中国科学院） ； School of Advanced Interdisciplinary Sciences, UCAS（交叉科学学院，中国科学院大学） ； School of Mathematical Science, UCAS（数学科学学院，中国科学院大学） 纠错

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

AI总结 Mechanic通过基于遗憾的正式分解策略提升自动定理证明效率，有效解决传统方法在处理失败尝试时的效率与上下文过长问题。

Comments Published as a conference paper at COLM 2026

Vision Language Models Cannot Plan, but Can They Formalize?

视觉语言模型（VLMs）无法规划，但它们能进行形式化吗？

Muyu He, Yuxi Zheng, Yuchen Liu, Zijian An, Bill Cai, Jiani Huang, Lifeng Zhou, Feng Liu, Ziyang Li, Li Zhang

机构 * Drexel University（德雷塞尔大学） ； University of Pennsylvania（宾夕法尼亚大学） ； Johns Hopkins University（约翰霍普金斯大学） 纠错

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

AI总结 本研究提出5种VLM作为形式化器的流水线，评估后发现其表现优于端到端规划生成，较弱VLMs的瓶颈为物体关系视觉grounding，较强模型已克服该限制。

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分析模型，编码人类技能与人工智能能力的经济不对称，推导多因素对人机替代的影响，得出替代原则，揭示其引发的组织变化及中层管理与高技能工人的脆弱性，统一相关理论。

Determinization in Structure Theories: A Unified Framework via Closure, Comparability, and Joint Admissibility

结构理论中的确定化：基于闭包、可比性与联合可容许性的统一框架

Hai Hai Fu

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

AI总结 该研究提出了基于闭包、可比性与联合可容许性的统一框架，用于从多结构理论构造典范解释，区分非确定性类型并给出对应确定化机制，还可应用于LLM辅助推理以分析幻觉问题。

Comments Formal framework paper on canonicalization and determinization in structure theories; version v2.16.4; 29 pages

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

Towards Assurance Closure in AI-Native Large-Scale Agile Software Development

面向AI原生大规模敏捷软件开发中的保证闭合

Ricardo Britto

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

AI总结 针对AI原生大规模敏捷软件开发中保证推理机器可操作的缺口，提出基于共享语义保证层的高层架构及六项对应能力，以实现保证闭合。

NiyamAI - An Intent-Bound AI Agent with Cryptographically Verifiable Guardrails using Zero-Knowledge Proofs

NiyamAI——一种使用零知识证明实现密码学可验证护栏的意图绑定AI智能体

Aditya Katkar, Om Karkele, Kartik Mandhane, Manisha More, Yash Kashid

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

AI总结 Niyam-AI是一种基于零知识证明的意图绑定AI智能体框架，通过SHA-256承诺意图合约、Judge模型验证和zk-SNARK确保证明，在Agent-SafetyBench评估中较多款基线护栏实现显著安全性能提升。

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

Privacy-Preserving AI Verification via Minimal Information Disclosure

通过最小信息披露实现隐私保护的AI验证

Sleem Abdelghafar, Gabriel Kulp

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

AI总结 该研究提出最小信息披露（MID）方法，通过条件互信息衡量AI验证中的附带泄露，在多项验证任务中实现完美验证且零附带泄露，并支持基于Groth16 zk-SNARK的ZKP认证发布。

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

MechGeo：在Lean 4中自动形式化与证明欧几里得几何

Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi

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

AI总结 MechGeo是基于Mathlib的智能体框架，可在Lean 4中自动形式化欧几里得几何问题并构造认证证明，在43道IMO几何题及Lean-IMO-Bbench上取得显著成果，为可信形式几何提供实用基础。

Comments 43 pages

Judging Is Not Enumerating: Silent Omissions in LLM-Authored Acceptable Sets

判断并非枚举：大语言模型生成的可接受集合中的隐性遗漏

Wenhui Chen, Jianlin Chen, Ziyao Lin, Peiji Long, Chi Man Vong

机构 * University of Macau（澳门大学） ； South China University of Technology（华南理工大学） 纠错

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

AI总结 该研究发现大语言模型作为评估者时，生成可接受集合的表现远差于判断表现，核心问题是隐性遗漏，通过重写错误预期值可大幅提升修复后的套件产量。

Comments 53 pages, 14 figures, 26 tables

Auditing Discovery Claims: A Two-Sided Criterion for Agentic Science, with the Negative Side Decidable

审计发现主张：面向智能体科学的双边准则，其负面侧可判定

Wenhui Chen, Jianlin Chen, Ziyao Lin, Chi Man Vong

机构 * University of Macau（澳门大学） ； South China University of Technology（华南理工大学） 纠错

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

AI总结 该研究提出面向智能体科学的双边审计准则，通过实验揭示AI科学系统能力主张的夸大问题，证实智能体编写的程序在低计算量下可击败人类程序，但未明确可迁移的机制。

Comments 51 pages, 10 figures, 10 tables

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

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

Dibakar Datta

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

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

Comments 32 pages, 6 figures

Persistent Convolution: A Topological Framework for AI Alignment Testing and Semantic Space Characterization

持久卷积：用于AI对齐测试和语义空间表征的拓扑框架

Tyler Ashoff, Jordan Rodu

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

AI总结 本研究开发了一种基于拓扑的多模态对齐测试，以提升不透明AI模型部署、选择与比较的可解释性，助力AI对齐测试与语义空间表征。

Comments Code available at github.com/tylerashoff/persiscope (PyPI: persiscope)

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访问。

FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs

FAVA：基于证据支持的权限图的经验证智能体的形式化授权

Yifan Zhang, Xinkui Zhao, Sai Liu, Hengxuan Lou, Guanjie Cheng, Chang Liu

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

AI总结 FAVA是一种用于智能体执行的带权限授权框架，通过LLM引导的权限IR、证据支持的权限图和SMT授权器保障安全，在多场景评估中达90.5%决策合规率，可拦截动态违规迹。

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

"Amazing, They All Lean Left" -- Analyzing the Political Temperaments of Current LLMs

W. Russell Neuman, Chad Coleman, Ali Dasdan, Safinah Ali, Manan Shah, Kund Meghani

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

Context Assembly as the Controlled Variable: A Control-Theoretic View of Harness Policies for Frozen LLM Agents

作为受控变量的上下文组装：冻结大语言模型智能体利用策略的控制理论视角

Debjyoti Paul

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

AI总结 研究聚焦大语言模型智能体，以往控制工具选择等，本文将上下文组装视为受控变量，通过上下文博弈或强化学习策略在线学习，进行形式分解、稳定性论证及不确定性校准分析，给出控制理论视角的相关证据。

Comments 6 pages, 2 figures, 1 table. Code and companion paper's data: https://github.com/dpaul0501/context-optimization-rl

Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations

不可信作者，可信答案：保真度分级翻译演算

Christoph Kirsch

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

AI总结 研究翻译问题，提出保真度分级翻译演算，该演算可按程序检查、通过粘贴组合，核心在Lean 4中机械化，在hurdy - gurdy平台实现，报告了多项实验结果，其增长模型通过任何人贡献语言对扩展语言支持。

Comments 29 pages. v2: rewritten on the two-plane principle; directional squares primary (exactness = the identity-embedding case, mechanized incl. the lax telescope); the answerability loop and its economy (demand books, recommended-then-registered); post-snapshot exhibits. Code, evidence, Lean mechanization: https://github.com/cksystemsgroup/hurdy-gurdy (tag arxiv.2)

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

Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro

使用GPT-5.5 Pro对实数上的和积猜想进行自主反证

Yichen Huang

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

AI总结 本文借助GPT-5.5 Pro构建智能体，通过三阶段提示管道，对实数上的和积猜想进行自主反证，8次试验中7次成功生成正确证明，每次试验平均用132.4k推理令牌，还发布相关内容供重现研究。

Agree on the Model, Verify the Inference: GKR Protocols for HND-Based Transformer Inference

就模型达成一致，验证推理：基于同态-非同态分解变压器的HND的GKR协议

Xiaolong Liang, Juanjuan Li, Rui Qin, Yisheng Lv

机构 * Institute of Automation, Chinese Academy of Sciences（中国科学院自动化研究所） ； State Key Laboratory of Multimodal Artificial Intelligence Systems（多模态人工智能系统国家重点实验室） 纠错

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

AI总结 研究外包变压器推理问题，提出GKR-HND协议验证同态-非同态分解变压器多项式主干，保留验证器检查记录与开口，委托公共评估给计算工作者，实验验证了证明路径与委托计算，无需密集矩阵重放。

Comments 24 pages, including 4 pages of supporting information; 2 figures

From Intent to Infrastructure: LLM-Driven Agent Compilers for ISAC Networks

从意图到基础设施：用于ISAC网络的基于大语言模型的智能体编译器

Lijie Zheng, Xudong Zhong, Baoquan Ren, Xiangwu Gong, Xinghui Zhu, Ji He

机构 * School of Computer Science and Technology, Xidian University（西安电子科技大学计算机科学与技术学院） ； Institute of Systems General, Academy of Systems Engineering, Academy of Military Sciences（系统工程院系统一般研究所） 纠错

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

AI总结 研究ISAC网络从概念验证到系统级部署的设计难题，提出基于大语言模型的智能体编译器，经四个阶段工作产生ISAC策略图，运行时引擎支持闭环自适应，以无人机救援为例展示编译过程并讨论开放问题。