大模型推理能力

Measuring Information Burden: From Coalition-Based Reasoning to the Price System

衡量信息负担：从基于联盟的推理到价格体系

Shuige Liu

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

AI总结 本文通过形式化框架衡量价格体系节省的信息量，证明在可转移效用博弈中，核心与一致同意等价所需的最小信息结构是每个联盟至少被其一个成员所知，且平均每代理信息负担随经济规模指数增长。

Automated Conjecture Resolution with Formal Verification

自动猜想解决与形式化验证

Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai, Bin Dong

机构 * School of Mathematical Sciences, Peking University（北京大学数学科学学院） ； Westlake Institute for Advanced Study, Westlake University（西拉雅大学先进研究所） ； School of Mathematics, Tianjin University（天津大学数学学院） ； Research Institute for Mathematical Sciences, Kyoto University（京都大学数学研究所） ； Department of Mathematics, Stanford University（斯坦福大学数学系） ； IQuest Research（IQuest研究） ； New Cornerstone Science Laboratory, School of Mathematical Sciences, Peking University（北京大学数学科学学院新基石科学实验室） ； Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University（北京大学国际数学研究所以及新基石科学实验室） ； Center for Machine Learning Research, Peking University（北京大学机器学习研究中心） ； Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University（大湾大学先进研究所智能计算中心） ； Zhongguancun Academy（中关村学院） 纠错

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

AI总结 提出一个集成非形式化推理与形式化验证的自动框架，通过两个组件Rethlas和Archon解决研究级数学问题，并成功解决交换代数中的开放问题并在Lean 4中形式化验证。

Comments Code and resources are available at: Rethlas (https://github.com/frenzymath/Rethlas), Rethlas Results (https://github.com/frenzymath/Rethlas_results), Archon (https://github.com/frenzymath/Archon), and the formalization results (https://github.com/frenzymath/Anderson-Conjecture)

Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification

形式数学验证中生成式奖励建模的期望值对齐

Shihao Ji, Haotao Tan, Zihui Song, Mingyu Li

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

AI总结 提出期望值对齐（EVA）方法，通过从模型词元分布中提取连续分数，在保持生成式奖励模型离散输出的同时实现连续评分，用于Lean 4形式验证。

From Scaling to Structured Expressivity: Rethinking Transformers for CTR Prediction

从规模到结构化表达能力：重新思考用于CTR预测的Transformer

Bencheng Yan, Yuejie Lei, Zhiyuan Zeng, Zheye Deng, Di Wang, Kaiyi Lin, Pengjie Wang, Chuan Yu, Jian Xu, Bo Zheng

机构 * Alibaba Group（阿里巴巴集团） 纠错

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

AI总结 针对CTR预测中Transformer模型因结构错位导致收益递减的问题，提出Field-Aware Transformer (FAT)，通过场感知参数重构和基组合超网络实现结构化表达能力，在理论（Rademacher复杂度标度律）和实验（AUC提升+4.38%，线上CTR+2.33%，RPM+0.66%）上均优于现有方法。

Comments KDD 2026; The first four authors contributed equally to this work