大模型推理能力

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

VERITAS：验证器引导的零样本形式定理证明搜索

Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

机构 * Department of Computer Science, Vanderbilt University（范德堡大学计算机科学系） ； Amazon（亚马逊） 纠错

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

AI总结 提出VERITAS框架，通过两阶段协议（Best-of-N采样+批评引导MCTS）利用验证器反馈进行零样本定理证明，在miniF2F上达40.6%准确率，并发布组合学基准VERITAS-CombiBench。

RACL: Reasoning-Agent Control Layers for Continuous Metaheuristic Learning

RACL：用于连续元启发式学习的推理代理控制层

Antón Asla Manzárraga

机构 * Independent Researcher（独立研究者） 纠错

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

AI总结 提出RACL方法，在元启发式优化器之上添加推理代理，通过观察、推理和干预控制搜索行为，在车辆路径问题上平均成本降低0.641%-8.337%。

Comments 10 pages, 5 tables

FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

FM-Agent: 通过基于LLM的Hoare风格推理将形式化方法扩展到大型系统

Haoran Ding, Zhaoguo Wang, Haibo Chen

机构 * Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University（并行与分布式系统研究所，上海交通大学） 纠错

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

AI总结 提出FM-Agent框架，利用LLM自动生成函数级规范，实现大型系统的组合式推理，在143k行代码的系统中2天内发现522个新bug。

Process-Verified Reinforcement Learning for Theorem Proving via Lean

基于Lean的过程验证强化学习用于定理证明

Minsu Kim, Se-Young Yun

机构 * KAIST AI（韩国科学技术院人工智能系） 纠错

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

AI总结 提出利用Lean证明助手提供过程级验证信号，结合GRPO风格强化学习目标，通过策略级监督提升定理证明性能。

Analyzing the Narration Gap in LLM-Solver Loops

分析大语言模型-求解器循环中的叙述差距

Zunchen Huang, Songgaojun Deng

机构 * Eindhoven University of Technology（埃因霍温理工大学） 纠错

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

AI总结 研究LLM与SAT/SMT求解器混合推理中，将求解器输出转化为用户答案的叙述步骤存在的安全漏洞，通过形式化建模和实验评估发现证书门控可保证求解结果正确，但对抗攻击可反转结论。

Pseudo-Formalization for Automatic Proof Verification

伪形式化用于自动证明验证

Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma

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

AI总结 本文提出了一种名为伪形式化的证明格式，该格式在保持自然语言灵活性的同时，保留了形式证明的模块性和精确性，通过块验证算法实现了对自然语言证明的高效验证，其在错误发现的精度和召回率上优于现有基线方法。

Comments 31 pages, code available at https://github.com/Slim205/pseudo-formalization