大模型推理能力

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)

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到可靠模拟设计方法奠定基础。

The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK

验证者即评判者：来自Ada/SPARK中AI编码代理的经过验证的安全软件

Tobias Philipp

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

AI总结 研究人工智能编码代理生成安全软件代码的情况，核心方法是在验证器驱动循环下编写验证，主要贡献是通过GNATprove完成大量证明义务，降低监督成本，同时指出其不足及得出代理受反馈强度限制的教训。

Correctness, confidence, and context: Framing software assurance in the AI age

正确性、置信度与上下文：在人工智能时代构建软件保障

Mary Shaw

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

AI总结 探讨软件工程中正确性相关挑战，指出传统方法与生成式人工智能在软件保障上的差异，呼吁系统思考保障技术，做出明智选择。

Comments 12 pages, 10 figures, text for invited keynote at FSE 2026 in Montreal. Revised after the conference to reflect discussions at the conference

Thermodynamic Limits of Proof

物理计数的计算复杂性

Tristan Simas

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

AI总结 研究物理计数的计算复杂性，提出决策商 Q 作为最小抽象，并证明多个复杂性理论结果。

Comments Main PDF: 35 pages, 4 tables. Supplementary: 26 pages, 2 tables. Lean 4 release artifact available at https://doi.org/10.5281/zenodo.18140965