大模型推理能力

Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

形式化迪斯科：可扩展的形式化验证程序的开放式生成

Gabriel Poesia, Simon Henniger, Tzu-Han Hsu, Yilun Du, Nada Amin

机构 * Kempner Institute, Harvard University（坎普纳研究所，哈佛大学） ； School of Engineering and Applied Sciences, Harvard University（工程与应用科学学院，哈佛大学） 纠错

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

AI总结 针对生成程序质量保证落后及形式验证数据稀缺问题，提出Formal Disco分布式系统，协调三类工人，记录痕迹用于改进，提出最大熵原则，发布数据集并微调模型，为形式推理领域大规模创建合成数据。

Comments Code: https://github.com/metareflection/formal-disco Datasets: https://huggingface.co/collections/metareflection/formal-disco

Beyond the Autoregressive Horizon: A Comprehensive Survey of Diffusion Models, World Modelling, and State Space Models for Code

超越自回归视野：扩散模型、世界模型和状态空间模型在代码领域的综合综述

Kishan Maharaj, Ashita Saxena, Srikanth Tamilselvam

机构 * IBM 纠错

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

AI总结 综述扩散模型、代码世界模型和状态空间模型在代码生成中的潜力，以克服自回归模型在全局规划、长程依赖和执行语义方面的局限，并展望“系统2”代码生成智能体。

Comments 14 Pages, 1 Table, 1 Figure

Process-Verified Reinforcement Learning for Theorem Proving via Lean

基于Lean的过程验证强化学习用于定理证明

Minsu Kim, Se-Young Yun

机构 * KAIST AI（韩国科学技术院人工智能系） 纠错

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

AI总结 提出利用Lean证明助手提供过程级验证信号，结合GRPO风格强化学习目标，通过策略级监督提升定理证明性能。

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

Diffusion-Proof：超越自回归生成的正式定理证明配方

Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

机构 * University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） ； NVIDIA（英伟达） 纠错

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

AI总结 提出Diffusion-Proof框架，首次将扩散语言模型应用于形式定理证明，通过全证明生成和局部校正方法，在ProofNet和MiniF2F上分别提升1.61%和6.14%，并解决了一个DeepSeek-Prover-V2-7B无法解决的IMO问题。

No Accidental Software Agent First Canonical Code for Human Code Entropy Reduction and 30 to 500 times Lower Frontier Model Requirements

无意外软件智能体：首个用于人类代码熵降低的正则代码，以及30到500倍的前沿模型需求降低

Jepson Taylor

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

AI总结 提出智能体优先的正则代码方法，通过行为等价商化人类代码中的意外熵，实现30-500倍的前沿模型需求降低，核心是行为等价商化和证明携带变更。

Comments 36 pages

Modular Cognitive Architecture Emerges in Large Language Models

大型语言模型中出现的模块化认知架构

Pengrui Han, Jacob Andreas, Evelina Fedorenko, Andrea Gregor de Varda

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

AI总结 该研究探究大型语言模型是否会出现类似人类大脑的模块化认知架构，经对4个认知领域46项任务的回路分析，发现其会形成相似模块化架构，表明模块化可能是智能系统的基本属性。

Comments this https URL (https://pengrui-han.github.io/LLM_Modularity_Page/)

A Frozen 12B Beats Frontier Models on Verified Work: 100% Accuracy, 0 Tokens, Bit-Exact, Forever

一个冻结的12B模型在经过验证的任务上超越前沿模型：100%准确率、零token、位精确、永远如此

Sietse Schelpe

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

AI总结 研究提出一种让模型冻结，通过增长持久内存来解决问题的方法。在多个问题族实例上，四种架构得分优异，执行与参数扩展解耦。该方法在开放式推理中也有效，内存选择快，存储规模大，在已验证任务上超越前沿模型。

Comments Industry experience report. 14 pages, 8 figures. Public testbench: https://corbenic-galahad-bench.hf.space; companion repository with SHA-256 provenance manifest: https://github.com/corbenicai/galahad-bench

RECEIPT: Deterministic, Reward-Hacking-Resistant Verification for White-Box Agentic XSS Discovery

RECEIPT：用于白盒代理式XSS发现的确定性、抗奖励攻击验证

Muxi Lyu, Karen Shieh, Yiwei Hou, Hao Wang, Koushik Sen, David Wagner

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

AI总结 研究针对白盒代理式XSS发现中编码代理声明不可信的问题，提出RECEIPT验证框架，通过环境隔离等手段使发现可信，经实验评估，在预算内发现多个未知漏洞，相比其他方式能确认更多真实利用且无假阳性。

Interpretable Language Model for Closed-Loop Type 1 Diabetes Control

用于闭环1型糖尿病控制的可解释语言模型

Maya Sarkar

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

AI总结 研究针对1型糖尿病控制中人工胰腺系统“黑箱”问题，提出LLM-T1D方法，结合强化学习与大语言模型，训练专家RL系统并提炼知识到模型，开发出可解释且性能优的胰岛素泵控制器，在模拟器测试中血糖控制良好且能防幻觉。

Comments Accepted at the 2026 IEEE 22nd International Conference on Automation Science and Engineering conference (IEEE CASE 2026)

CARVE: Content-Aware Recurrent with Value Efficiency for Chunk-Parallel Linear Attention

CARVE: 内容感知循环与值效率的分块并行线性注意力

Sayak Dutta

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

AI总结 提出CARVE模型，通过仅在键轴上擦除解决delta规则架构的三个耦合缺陷，实现WY形式分块求解器，在1.3B参数上取得WikiText困惑度15.72，优于GDN-2。

Comments 33 pages, 3 figures, 11 tables, 5 algorithms (incl. appendices with full proofs and Triton kernel pseudocode). Single-author preprint

Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit

洪流与收获：通过极限语言生成视角证明琐碎知识对于生成有价值数学的必要性

Xiaoyu Li, Andi Han, Dai Shi, Zheng Gao, Jiaojiao Jiang, Junbin Gao

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

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

AI总结 本文通过极限语言生成模型证明，在形式化数学生成中，验证器无法替代品味：覆盖未记录的有价值数学必须产生无限但渐近可忽略的琐碎语句，这是理论上的必然。

Interpretable Unsupervised Community Detection with LLM-Symbolized Structured Processes

基于LLM符号化结构化过程的可解释无监督社区检测

Aoting Zeng, Kai Wang, Jianwei Wang, Yuxiang Sun, Yizhang He, Wenjie Zhang

机构 * Shanghai Jiao Tong University（上海交通大学） ； University of New South Wales（新南威尔士大学） 纠错

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

AI总结 本研究提出LLM引导的无监督社区检测方法LUCID，通过四阶段流程结合LLM生成规则实现可解释性，在真实数据集上性能优于主流无监督与半监督基线。

Invariant Discovery for Networked Systems

网络系统的不变量发现

Hongyu Hè, Alexander Krentsel, Sylvia Ratnasamy, Maria Apostolaki

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

AI总结 研究网络系统不变量发现问题，核心方法是将其分为人工智能驱动的语法“发现”与统计驱动的“搜索”问题，设计实现Autogram系统，贡献是能在多种数据上高覆盖率、低误报地恢复专家不变量并讨论开放问题。

Comments 8 pages, 4 figures, 1 table

LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

LeanFlow：工作流驱动的精益自动形式化案例研究

Lazar Milikic, Simon Guilloud, Khanh Nguyen, Viktor Kuncak

机构 * Moonshot AI（月球计划人工智能公司） ； epfl-lara（洛桑联邦理工学院拉腊实验室） 纠错

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

AI总结 研究通过对两篇数学论文案例研究，探讨文档到项目形式化中运行时机制对相关指标的影响，使用Kimi2.6和GPT5.5进行消融实验，报告多项数据，展示LeanFlow在特定任务上的表现及校准成果。

Comments 14 pages, 3 figures, ICML 2026: AI for Math Workshop

ETAS: An Effect-Typed Language for Agent Systems

ETAS：一种用于智能体系统的效果类型化语言

Huiri Tan, Yikun Wang, Puyang Zhang, Shangyu Li, Jiasi Shen

机构 * The Hong Kong University of Science and Technology（香港科学与技术大学） 纠错

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

AI总结 研究针对智能体系统设计ETAS语言，核心方法是通过规范一致性分配类型并用行为索引跟踪计算，主要贡献是为智能体执行相关推理提供编程语言基础，涵盖授权、非确定性等方面，还实现了该语言并形式化相关性质。

Towards Reliable AI-Assisted Analog Design: Template-Constrained LLM Agents for SAR ADC Generation

迈向可靠的人工智能辅助模拟设计：用于逐次逼近寄存器型模数转换器生成的模板约束大语言模型智能体

Dimple Vijay Kochar, Hae-Seung Lee, Anantha P. Chandrakasan

机构 * Massachusetts Institute of Technology（麻省理工学院） 纠错

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

AI总结 研究针对大语言模型在模拟电子设计自动化应用的瓶颈，提出端到端多步骤的ATLAS框架，利用专家知识结合模板约束生成，能生成成功通过仿真验证的SAR ADC，为集成LLMs到可靠模拟设计方法奠定基础。

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

从求解器到研究：前沿研究中的大语言模型驱动形式数学

Eric Jiang, Xiao Liang, Yikai Zhang, Yingjia Wan, Mengting Li, Haikang Deng, Alexander K. Taylor, Justin Baker, Rushil Raghavan, Junyi Zhang, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang

机构 * University of California, Los Angeles（加利福尼亚大学洛杉矶分校） ； Lawrence Livermore National Laboratory（劳伦斯利弗莫尔国家实验室） 纠错

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

AI总结 探讨AI4Math领域进展，指出当前系统处理前沿数学问题有局限。主张从预定义求解器转向研究代理，对该领域进行系统综述，识别现有系统局限性，为AI4Math未来发展规划战略路线图。

Plans Don't Persist: Why Context Management Is Load Bearing for LLM Agents

计划不会持久：为什么上下文管理对LLM代理至关重要

Aman Mehta, Anupam Datta

机构 * Snowflake AI Research（Snowflake AI研究） 纠错

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

AI总结 本文通过重放配对诊断和压缩压力测试，证明标准LLM代理不将计划作为持久状态携带，而是依赖上下文中的计划，并揭示了推理模型的推理痕迹混淆问题。

Comments 17 pages, 8 figures

VeriBound: PAC-Bayesian Generalization Bounds for Process Reward Models Trained with Formal Verification Tools

VeriBound: 使用形式验证工具训练的过程奖励模型的PAC-Bayesian泛化界

Amirul Rahman, Mohammed Sabih Alsharari

机构 * University of Malaya（马来亚大学） 纠错

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

AI总结 针对形式验证工具标注的过程奖励模型（PRM）缺乏理论解释的问题，提出VeriBound框架，给出PAC-Bayesian泛化界、样本复杂度、收敛速率及下游Best-of-K性能的误差传播界。

Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory

假设约束的多智能体自动形式化渐近统计理论

Tingzhou Wei, Zeyu Zheng, Ethan X. Fang, Junwei Lu

机构 * Department of Biostatistics & Bioinformatics, Duke University（杜克大学生物统计与生物信息学系） ； Department of Mathematical Sciences, Carnegie Mellon University（卡内基梅隆大学数学科学系） ； Department of Biostatistics, Harvard T.H. Chan School of Public Health（哈佛大学陈曾熙公共卫生学院生物统计系） 纠错

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

AI总结 提出一种假设约束的多智能体Lean 4形式化流程，通过七个专业角色协调工作，实现渐近统计理论中参数和半参数模型的形式化，确保公理干净且忠实于原文。

CAF-Gen: A Multi-Agent System for Enriching Argumentation Structures

CAF-Gen: 一种用于丰富论证结构的多智能体系统

Jakub Bąba, Jarosław A. Chudziak

机构 * Faculty of Electronics and Information Technology, Warsaw University of Technology（电子与信息技术学院，华沙技术大学） 纠错

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

AI总结 提出CAF-Gen多智能体框架，通过迭代创建-评审流程将浅层论证结构自动转换为符合Carneades论证框架的丰富模型，克服单次生成的结构不稳定性。

Comments Accepted for publication in the proceedings of ICCCI 2026

One Polluted Page Is Enough: Evaluating Web Content Pollution in Generative Recommenders

一个被污染的页面就够了：评估生成式推荐系统中的网页内容污染

Minghao Luo, Liang Chen

机构 * The Chinese University of Hong Kong（香港中文大学） 纠错

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

AI总结 本研究提出FORGE基准，评估搜索增强LLM在检索结果被污染时推荐虚假产品的脆弱性，发现单个污染页面即可导致高达27%的推荐错误率，且推理能力无法缓解此问题。

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

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评估中较多款基线护栏实现显著安全性能提升。

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

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)