大模型推理能力

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

Cycle-Consistent Neural Explanation of Formal Verification Certificates

形式验证证书的循环一致性神经解释

Andoni Rodriguez, Alberto Pozanco, Daniel Borrajo

机构 * J.P. Morgan AI Research（摩根大通人工智能研究院） 纠错

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

AI总结 提出循环一致性神经架构，通过前向和逆向网络结合符号验证器，生成忠实于形式验证证书的自然语言解释，在金融合规领域测试中达到90.0%的循环验证正确性，比多LLM基线高13.9个百分点。

Comments 15 pages of main text

Closing the Loop: Formally Verified Law as a Reward Signal for Self-Improving Legal AI

闭环：形式化验证的法律作为自我改进法律AI的奖励信号

Armin Heydari, Torben Leowald

机构 * Harvard University（哈佛大学） ； Columbia University（哥伦比亚大学） 纠错

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

AI总结 提出一种架构，通过LLM驱动的形式化转换和验证内核，为法律AI提供可验证的奖励信号，实现闭环强化学习，并在多个法律领域展示其优势。

Comments 14 pages, no figures

Cryptographic certificates of validity for trustworthy AI

可信AI的密码学有效性证书

Murdoch J. Gabbay

机构 * Heriot-Watt University（赫瑞思-瓦特大学） 纠错

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

AI总结 提出为智能AI系统生成密码学有效性证书，通过将正确性条件编译为多项式约束的见证检查问题，并使用简洁密码学证明系统（可选零知识）来证明条件成立，平衡了源代码形式验证与密码学认证。

Verifiable Foundation Models for Robot Safety

机器人安全的可验证基础模型

Davide Corsi, Kyungmin Kim, Roy Fox

机构 * University of California, Irvine（加州大学尔湾分校） 纠错

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

AI总结 提出FEARL框架，将策略分解为大控制器和小安全模块，使形式化验证仅应用于安全模块，从而在保持控制器表达能力的同时实现可验证的机器人安全控制。

Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language

使用宽松自然形式语言的可验证数学自动形式化

Zhicheng Hui, Lihan Xie, Xingzhi Qi, Zhehao Li, Yingjun Lan, Qinxiang Cao

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

AI总结 提出一种宽松自然形式语言作为中间目标，通过分阶段精化实现可验证的数学自动形式化，结合规则转换与LLM启发式方法，并利用领域特定策略语言生成验证条件。

Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering

形式化方法引导的Vibe编码：通过模型驱动工程关闭AI生成安全关键软件的验证循环

Ran Wei, Le Zhu, Haochi Wang, Jim Woodcock, Fang Yan, Simon Foster, Xiangyang Ji

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

AI总结 提出Forge管道，结合Vibe编码与模型驱动工程，通过多种形式化验证（Dafny、CSP、Isabelle）迭代修正LLM生成的Java代码，生成符合安全标准的验证证据。