大模型推理能力

Process-Verified Reinforcement Learning for Theorem Proving via Lean

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

Minsu Kim, Se-Young Yun

专题命中 数学推理 ：定理证明强化学习

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

CombEval: A Framework for Evaluating Combinatorial Counting in Large Language Models

CombEval：评估大语言模型中组合计数的框架

Yuxu Zhou, Ondřej Kuželka, Yuyi Wang, Yuanhong Wang, Yi Chang

专题命中 数学推理 ：评估LLM在组合计数问题上的推理能力。

AI总结 提出CombEval动态基准，通过类型化Cofola规范生成组合计数问题，评估11个大语言模型在直接和代码增强设置下的表现，发现模型在有序对象、不可区分元素、相对位置约束和嵌套对象依赖上存在脆弱性。

Comments under review. Code: https://github.com/YuxuZhou-CN/combination-problem-generation

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

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

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

专题命中 数学推理 ：验证器引导的零样本形式定理证明。

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

Efficiently Representing Algorithms With Chain-of-Thought Transformers

高效表示链式思维Transformer中的算法

Yanhong Li, Anej Svete, Ashish Sabharwal, William Merrill

专题命中 数学推理 ：证明CoT Transformer高效模拟Word RAM算法，涉及排序等推理

AI总结 本文证明链式思维Transformer能以多对数开销高效模拟Word RAM算法，包括排序和Dijkstra算法，优于模拟图灵机的二次开销。

Hard or Just Unreached? Diagnosing the Sampling Blind Spot in Math-Reasoning Difficulty Estimation

困难还是未触及？诊断数学推理难度估计中的采样盲点

Luca Zhou, Sajel Shah, Emanuele Rodolà, Roberto Dessì

专题命中 数学推理 ：诊断数学推理难度估计中的采样盲点，提出确定性采样。

AI总结 发现pass@k在数学推理难度估计中存在盲点，通过激活嫁接的确定性采样可恢复10.3-22.9%的零解样本，揭示结构可识别性。

Comments 9 pages of main paper, 4 figures and 5 tables in the main paper, with more in the appendix

VIMPO: Value-Implicit Policy Optimization for LLMs

VIMPO: 值隐式策略优化用于大语言模型

Zhewei Kang, Aosong Feng, Sergey Levine, Dawn Song, Xuandong Zhao

专题命中 数学推理 ：方法在数学推理基准上优于GRPO。

AI总结 提出VIMPO方法，通过KL正则化强化学习的最优条件导出策略隐含值函数，无需训练评论家，实现细粒度信用分配，在数学推理基准上优于GRPO。

Pseudo-Formalization for Automatic Proof Verification

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

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

专题命中 数学推理 ：伪形式化用于自动证明验证

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

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

MoCA-Agent: A Market-of-Claims Code Agent for Financial and Numerical Reasoning

MoCA-Agent: 一种用于金融和数值推理的声明市场代码智能体

Abdelrahman Abdallah, AbdelRahim A. Elmadany, Sameh Al Natour, Hasan Cavusoglu, Adam Jatowt, Muhammad Abdul-Mageed

专题命中 数学推理 ：处理金融数值推理，涉及多步计算

AI总结 提出MoCA-Agent，通过声明级验证和代码生成解决金融表格问答中的数值推理错误，在十个基准上取得强性能。