AI 大模型
大模型数学、逻辑、规划、多步推理和测试时计算能力。
临床记录的多大型语言模型编排严重程度评估（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
闭环：形式化验证的法律作为自我改进法律AI的奖励信号
机构 * Harvard University（哈佛大学） ； Columbia University（哥伦比亚大学）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.LG
AI总结 提出一种架构，通过LLM驱动的形式化转换和验证内核，为法律AI提供可验证的奖励信号，实现闭环强化学习，并在多个法律领域展示其优势。
Comments 14 pages, no figures
可信AI的密码学有效性证书
机构 * Heriot-Watt University（赫瑞思-瓦特大学）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 提出为智能AI系统生成密码学有效性证书，通过将正确性条件编译为多项式约束的见证检查问题，并使用简洁密码学证明系统（可选零知识）来证明条件成立，平衡了源代码形式验证与密码学认证。
机器人安全的可验证基础模型
机构 * University of California, Irvine（加州大学尔湾分校）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.LG
AI总结 提出FEARL框架，将策略分解为大控制器和小安全模块，使形式化验证仅应用于安全模块，从而在保持控制器表达能力的同时实现可验证的机器人安全控制。
GIF: 局部几何信息流控制用于大语言模型
机构 * Columbia University（哥伦比亚大学）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 提出GIF框架，利用LLM雅可比矩阵和局部输出几何上界香农互信息，实现可扩展的信息流追踪，在提示注入和隐私泄露任务中达到近完美召回，且计算成本低。
Grounded Scaling: 为什么代理型AI需要确定性环境
机构 * Alibaba Group（阿里巴巴集团）
专题命中 代码与定理证明 ：verifier(abstract)；分类 cs.AI
AI总结 本文论证环境确定性是影响长链代理任务成功的关键因素，提出确定性-效率界限、验证者-古德哈特下限等理论，并构建供应确定性指数和确定性成熟度模型。
由AI编写，由AI管理：跨越391个连续会话的语义空间控制与索引病消除
机构 * Shenzhen Yunxi Technology Co., Ltd.（深圳云曦科技有限公司） ； Information Technology Center, Tsinghua University（清华大学信息科学技术中心）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.CL
AI总结 本文通过真实软件项目中的行动研究，发现长期LLM协作中增加形式约束反而导致“索引病”，提出“基线-日志物理分离”机制，有效消除该问题。
Comments 22 pages, 2 tables, 1 figure. Action research. Bilingual submission (Chinese companion version included as supplementary). Submitted to ICSE 2027 IOR track
评估基于大语言模型的议会辩论总结的论证内容
机构 * 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
分析大语言模型-求解器循环中的叙述差距
机构 * Eindhoven University of Technology（埃因霍温理工大学）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 研究LLM与SAT/SMT求解器混合推理中，将求解器输出转化为用户答案的叙述步骤存在的安全漏洞，通过形式化建模和实验评估发现证书门控可保证求解结果正确，但对抗攻击可反转结论。
伪形式化用于自动证明验证
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.LG
AI总结 本文提出了一种名为伪形式化的证明格式，该格式在保持自然语言灵活性的同时，保留了形式证明的模块性和精确性，通过块验证算法实现了对自然语言证明的高效验证，其在错误发现的精度和召回率上优于现有基线方法。
Comments 31 pages, code available at https://github.com/Slim205/pseudo-formalization
通用型智能体必须记住什么？
机构 * Carnegie Mellon University（卡内基梅隆大学） ； Georgia Institute of Technology（佐治亚理工学院）
专题命中 代码与定理证明 ：planning(abstract)；分类 cs.AI
AI总结 本文形式化论证了通用型智能体为在多个环境和目标下近似最优行动，必须存储领域相关信息以区分观察瓶颈处的不兼容最优动作，并证明记忆可用于重构局部转移动态。
热力学中的超级学生智能
机构 * Laboratory of Engineering Thermodynamics (LTD)（工程热力学实验室） ； Visual Information Analysis Research Group (VIA)（视觉信息分析研究组） ； Machine Learning Research Group (ML)（机器学习研究组）
专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI
AI总结 研究展示OpenAI的o3模型在热力学考试中超越所有学生，证明机器在复杂任务中的能力，影响工程教育与实践。
Comments This document is the unedited Author's version of a yet to be Submitted Work to Physical Review Physics Education Research. 15 pages, 2 figures, Graphical Abstract, Highlights and SI available (12 pages)
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈