AI 大模型
大模型数学、逻辑、规划、多步推理和测试时计算能力。
$\max$@$k$强化学习的理论基础
机构 * Bocconi University（博科尼大学）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.LG
AI总结 研究有限 horizon 强化学习中$\max$@$k$学习问题，指出其与标准预期回报最大化不同，证明马尔可夫策略不足，识别状态增强，表征策略性能差距，表明学习更难，给出高效算法实现最优样本复杂度率。
验证者即评判者：来自Ada/SPARK中AI编码代理的经过验证的安全软件
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 研究人工智能编码代理生成安全软件代码的情况，核心方法是在验证器驱动循环下编写验证，主要贡献是通过GNATprove完成大量证明义务，降低监督成本，同时指出其不足及得出代理受反馈强度限制的教训。
CAVA：用于智能代理人工智能系统运行时治理的规范动作验证与认证
机构 * Ond Holdings Inc（Ond控股公司）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 研究智能代理人工智能系统异构运行时带来的治理问题。提出CAVA，将异构代理活动转换为规范动作对象。通过基准参考实现研究，为部署者端人工智能治理提供动作级规范化和语义模式的系统表述。
Comments 35 pages. Working paper on canonical action verification, runtime governance, semantic pattern detection, and approval-bound action receipts
关于超博弈理论的综述：为多智能体系统建模错位感知与嵌套信念
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 本文综述了超博弈理论在多智能体系统中的应用，分析了其建模错位感知与嵌套信念的能力及现有研究中的趋势与挑战。
OpenProver：使用Lean 4进行智能且交互式的定理证明
机构 * Charles University, Faculty of Mathematics and Physics（查尔斯大学数学与物理系）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 介绍用于大语言模型驱动的自动化定理证明的开源系统OpenProver，它集成特定架构，完全开源，能自动验证证明，提供交互式界面，通过在ProofNet上评估展示自动验证在定量消融实验中的潜力。
Comments 7 pages, 2 figures. Accepted at the 19th Conference on Intelligent Computer Mathematics (CICM 2026)
Lean-QIT：迈向量子信息理论的形式化基础设施
机构 * QudeLeap Research（QudeLeap研究院） ； The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州）） ； Quantum Science Center of Guangdong-Hong Kong-Macao Greater Bay Area（粤港澳大湾区量子科学中心） ； The University of Hong Kong（香港大学）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 研究旨在为量子信息理论构建形式化基础设施，通过Lean 4库LeanQIT提供相关接口，将多个重要定理形式化，分离操作定义与解析表征，为形式化QIT及相关推理提供基础和知识底物。
Comments 24+5 pages, 3 figures
LLMlambda 计算：人工智能代理、对话与信息流
机构 * University of Nottingham, UK（诺丁汉大学） ； University of Edinburgh, UK（爱丁堡大学） ； Chalmers University of Technology（查尔姆斯理工大学） ； The University of Gothenburg, Sweden（哥德堡大学）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 本文提出了一种无类型的lambda计算模型，用于形式化描述和验证人工智能代理中对话和信息流的安全性。
设计和评估一种增强人工智能的沉浸式跨学科模拟（AIMS）用于多专业教育
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 AIMS通过整合AI和虚拟环境，为多专业教育提供沉浸式模拟，提升学生协作能力和临床推理能力。
Comments 15 pages. Immersive Learning Research-Academic (2026)
执行证明：受治理人工智能代理行动的运行时验证
机构 * AlphaBitCore, Inc.（AlphaBitCore公司）
专题命中 代码与定理证明 ：planning(abstract)；分类 cs.AI
AI总结 研究人工智能代理行动正确性验证问题，提出运行时证明（PoE）方法构建执行三元组及相关谓词和保证，证明其合理性，通过原型测试验证效果，能将多方面绑定到可检查对象，使受治理执行可证。
Comments 14 pages, 1 figure, 4 tables, 1 algorithm; includes formal soundness and replay theorems with witness constructions in appendix
人工智能在科学发现中的三层框架
机构 * Department of Mathematics, University of Texas at Arlington（德克萨斯大学阿灵顿分校数学系）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出AI在科学发现中的三层框架，核心创新是第二层：通过定性推理进行模型形成，识别框架结构不足并寻找缺失概念，通过三个案例说明其重要性。
编码智能体中的潜在编程视界
机构 * KTH Royal Institute of Technology（瑞典皇家理工学院）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.LG
AI总结 该研究探究编码智能体底层语言模型的程序内部表征，通过逻辑回归探针发现其残差流可线性编码程序属性，还能提前约25步预测后续编辑结果，为编码智能体的机制可解释性研究提供新方向。
临床记录的多大型语言模型编排严重程度评估（MOSAIC）
机构 * Department of Drug Design and Pharmacology, University of Copenhagen（哥本哈根大学药物设计与药理学系） ； GSK（葛兰素史克） ； School of Pharmacy, University of Rhode Island（罗德岛大学药学院）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.CL
AI总结 研究用MOSAIC这一两阶段智能语言模型框架对2型糖尿病严重程度进行表型分析，以合成队列评估其与多种算法真值对比情况及全因死亡率等，结果显示该框架有优势，智能分类与固定规则执行不同。
使用中间形式规范训练代码语言模型进行推理
机构 * FPT Software AI Center（FPT软件人工智能中心） ； University of Texas at Dallas（德克萨斯大学达拉斯分校） ； Hanoi Univ. of Science and Tech.（河内科学技术大学） ； Texas, USA（得克萨斯州，美国） ； Hanoi, Vietnam（河内，越南）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.CL
AI总结 研究可执行检查点规范生成，介绍SpecCoder框架从多种程序学习，能选正确规范拒错误执行。引入HumanExec基准测试，实验表明其提升了检查点规范质量及下游正确性推理和修复能力。
SABLE：工业 EDA 流程中用于模拟电路优化的 NDA 安全闭环 LLM 框架
机构 * University of Minnesota, Twin Cities（明尼苏达大学，双城分校）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.LG
AI总结 研究针对工业模拟流程中数据安全问题，提出 SABLE 框架，结合多种安全措施，能让 LLM 通过特定工具优化模拟电路，在实际任务中评估多个模型，验证其有效性。
将AI用作带有时序计算的可能性骰子
机构 * Department of Surgery, University of Minnesota（明尼苏达大学外科系） ； Department of Computer Science & Engineering, University of Minnesota（明尼苏达大学计算机科学与工程系）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 本文提出基于动词的范式，定义时序计算和可能性，使AI能作为实现思维语法的工具，并在乳腺癌患者数据上自动发现临床轨迹和反事实时序推断。
LLMs作为数学考试评分的助教：可靠性与实际可用性
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 评估六种LLM配置在离散数学考试评分中的表现，发现宽松评分策略降低错误率，但点校准与排名保持仍是不同目标。
Comments 12 Pages, 6 figures
Aria: 基于依赖图的检索与迭代自动形式化智能体
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出Aria系统，通过两阶段思维图过程递归分解定理陈述为依赖图并构建形式化，结合AriaScorer验证语义正确性，在ProofNet、FATE-X和同调猜想数据集上显著超越现有方法。
面向智能体RAG管道的贝叶斯不确定性传播：多跳问答的概念验证研究
机构 * University of Hull（赫尔大学）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出一种不确定性感知的智能体RAG框架，通过贝叶斯网络传播各阶段的不确定性信号，以估计系统级不确定性并定位潜在故障点，在HotpotQA上表现有效，但在StrategyQA上受限于校准问题。
Comments Submitted for 7th International Conference on Maintenance and Intelligent Asset Management (ICMIAM 2026)
AxDafny: Dafny中的智能验证代码生成
机构 * Axiomatic AI, Boston, MA, USA（Axiomatic AI，波士顿，马萨诸塞州，美国）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 提出AxDafny框架，通过验证器引导的修复迭代生成Dafny代码和证明，在LCB-Pro-Dafny和DafnyBench上显著提升验证成功率。
在 Lean 中形式化求解答案构造问题
机构 * University of Toronto（多伦多大学） ； Georgia Institute of Technology（佐治亚理工学院）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出 Enumerate-Conjecture-Prove (ECP) 框架，结合通用大语言模型和证明器大语言模型，在 Lean 中端到端地构造答案并生成形式化证明，解决数学竞赛中的答案构造问题。
言语胜于代码：探究基于LLM的代码漏洞检测中的认知启发式
机构 * BRAC University（布拉德大学） ； Purdue University（普渡大学） ； University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 本文首次系统探究认知启发式对LLM代码漏洞检测的影响，提出控制框架，发现所有评估模型均易受光环、框架和锚定效应影响，且语义推理型漏洞更易受影响。
论形式数学中的组合学习行为
机构 * University of York（约克大学）
专题命中 代码与定理证明 ：chain-of-thought(abstract)；分类 cs.CL
AI总结 本文提出 S2B-LM 基准，通过去除数值处理混淆并添加思维链框架来评估组合学习行为（CLB），发现 CLB 能力对于形式数学验证的困难部分必要但不充分。
Comments Accepted at AI4Math Workshop @ ICML2026
为价值感知多智能体系统建模人类价值观
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 本文提出一个形式化框架，用于表示人类价值观，以支持多智能体系统中的价值感知推理。通过社会心理学研究，建立价值关系和重要性模型，实现行为评估和价值感知决策机制。
Comments arXiv admin note: text overlap with arXiv:2305.02748
ToE：一种具有动态多源证据检索与聚合的分层可解释声明验证框架
机构 * School of Cyberspace Science and Technology, Beijing Institute of Technology（北京理工大学信息科学与技术学院） ； TravelSky Technology Limited（TravelSky技术有限公司） ； School of Computer Science, University of Auckland（奥克兰大学计算机科学学院）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出Tree of Evidence (ToE)框架，通过强化学习驱动的多源检索、证据评估和参数树聚合，实现可解释的自动事实核查，在多个数据集上提升4-24个百分点，尤其对抗性毒化输入效果显著。
LCAi: 基于大数据融合与检索增强生成辅助解释的生命周期评估
机构 * Institute for Chemical and Bioengineering, Department of Chemistry and Applied Biosciences, ETH Zürich（苏黎世联邦理工学院化学与应用生物科学系化学与生物工程研究所） ； NCCR Catalysis（瑞士国家研究能力中心催化研究所）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出一种视角条件检索增强生成框架，通过多视角检索与受控合成，在AI辅助生命周期评估中实现结构化解释，减少幻觉风险并保持跨领域多样性。
Comments 23 pages, 14 figures, 6 tables. Includes Supplementary Information
LLM 生成的 VeriFast 规范实证研究
机构 * Purdue University（普渡大学） ； University of Michigan（密歇根大学） ； Meta ； Ann Arbor, Michigan, USA（美国密歇根州安阿伯） ； Menlo Park, California, USA（美国加州Menlo Park） ； West Lafayette, Indiana, USA（美国印第安纳州西拉法叶）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 本研究评估了大型语言模型为分离逻辑验证器 VeriFast 生成规范的能力，发现虽然功能保持良好（>91%），但验证成功率仅31.4%，主要错误源于领域知识不足。
并非所有证明都平等：超越正确性的LLM证明质量评估
机构 * 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
大语言模型在研究级数学问题上的失败模式：分类与实证刻画
机构 * Dept. of CSE (Data Science) Heritage Institute of Technology（计算机科学与工程系（数据科学）哈里特技术学院）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 本文通过分析“First Proof”基准测试中LLM的错误，识别出四种失败模式（F1-F4），并审计Gemini 2.5 Flash生成的证明，发现前提走私（F2）普遍存在且无法被引文验证检测，提出应构建推理时管道预防而非事后检测。
TheoremGraph：连接形式化与非形式化数学
机构 * University of Washington Math AI Lab（华盛顿大学数学人工智能实验室）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出TheoremGraph，构建统一语句级依赖图，连接非形式化（arXiv论文）和形式化（Lean）数学，通过嵌入自然语言标语实现跨域链接，并验证了检索性能。
Comments 31 pages, 9 figures, 21 tables
形式验证证书的循环一致性神经解释
机构 * J.P. Morgan AI Research（摩根大通人工智能研究院）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 提出循环一致性神经架构，通过前向和逆向网络结合符号验证器，生成忠实于形式验证证书的自然语言解释，在金融合规领域测试中达到90.0%的循环验证正确性，比多LLM基线高13.9个百分点。
Comments 15 pages of main text
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈