大模型推理能力

The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

4/δ 界：设计具有形式方法保证的可预测 LLM-验证器系统

Pierre Dantas, Lucas Cordeiro, Youcheng Sun, Waldir Junior

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

AI总结 提出 LLM-验证器收敛定理，将多阶段验证建模为顺序吸收马尔可夫链，证明成功概率 δ>0 时系统几乎必然验证，并导出精确延迟上界 4/δ，经 90000+ 试验验证。

Comments 36 pages, 9 figures

MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

MINIF2F-DAFNY: 通过自动主动验证的LLM引导数学定理证明

Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Sean B. Holden

机构 * University of Cambridge, Cambridge, UK（剑桥大学） ； Amazon Web Services, London, UK（亚马逊网络服务（伦敦）） ； Amazon Web Services, Boston, USA（亚马逊网络服务（波士顿）） 纠错

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

AI总结 提出首个将数学基准miniF2F翻译到自动主动验证器Dafny的数据集，评估8个LLM的证明生成能力，最佳模型Claude Opus 4.6达到62.7%的累积通过率，比空证明基线提升23.8个百分点。

Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation

大语言模型在研究级数学问题上的失败模式：分类与实证刻画

Arnesh Banerjee, Ayushi Bhattacharjee

机构 * 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: Bridging Formal and Informal Mathematics

TheoremGraph：连接形式化与非形式化数学

Simon Kurgan, Evan Wang, Eric Leonen, Sophie Szeto, Luke Alexander, Artemii Remizov, Jarod Alper, Giovanni Inchiostro, Vasily Ilin

机构 * University of Washington Math AI Lab（华盛顿大学数学人工智能实验室） 纠错

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

AI总结 提出TheoremGraph，构建统一语句级依赖图，连接非形式化（arXiv论文）和形式化（Lean）数学，通过嵌入自然语言标语实现跨域链接，并验证了检索性能。

Comments 31 pages, 9 figures, 21 tables

Evolving Quantum Error-Correcting Encodings for Molecular Simulation

面向分子模拟的量子纠错编码演化

Kenny Heitritter, James Brown, Tarini Hardikar

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

AI总结 利用LLM驱动的演化程序合成，发现分子模拟中距离5和6的广义超快编码，并进一步通过压缩导向搜索获得结构化循环构造器。

Comments 16 pages including appendices, 4 figures, 8 tables

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

CrypFormBench：评估大型语言模型在密码方案形式化分析中的能力基准

Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

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

AI总结 提出CrypFormBench基准，涵盖符号与计算安全，评估LLM在密码方案形式化分析中的五项核心能力，发现模型在生成、转换和修正方面表现有限。

Comments 23 pages, 17 figures, FSE 2026