一、题目与评测：从研究级证明到科学规律
【1】The Endless Exam: Mathematical Constructions from Today’s Models toward Superintelligence
https://arxiv.org/abs/2609.24555
数学构造题为探索能力提供了一种直观的检验方式：模型提交一个对象，程序检查其有效性，再将质量与已有结果比较。The Endless Exam 收录14类参数化构造问题，支持通过调整参数持续增加难度，也允许得分超出参考水平。
【2】TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science
https://arxiv.org/abs/2609.35606
TCSAlgBench 从 STOC 和 COLT 2026 的138篇论文中整理出398个定理级挑战，覆盖算法发现与自然语言证明。每道题保留必要的背景、计算假设和定量保证，模型还可查阅被引工作。论文还比较了证明者与验证者的讨论、任务分解和智能体规划等流程对解题覆盖的影响。
【3】AutoformBench: A Lean Formalization Benchmark for Advanced Mathematics
https://ai.meta.com/research/publications/autoformbench-a-lean-formalization-benchmark-for-advanced-mathematics/
一段高级数学证明进入 Lean，往往要先补齐定义、引理和库中的基础设施。AutoformBench 围绕这一过程，从24份数学来源中整理了341个 Lean 4 形式化任务，并提供相应的非形式化证明。任务涵盖定义构建、中间引理补全和支撑代码编写，呈现了完整数学形式化过程中的多项工作。
【4】SciGame: Let Agents Play the Scientific Discovery Games in the Real and Counterfactual World
https://arxiv.org/abs/2610.37919
SciGame 将科学文献整理成结构化任务卡，为每张卡构建原始规律与量纲一致的反事实环境，让智能体通过观察和实验推断规律。评测覆盖候选规律识别与开放式发现，并比较固定数据和自适应实验等条件。这样的设计让读者能够观察：已有知识怎样影响判断，新增实验带来多少信息，以及得到的规律能否预测未见输入。
【5】POSEIDON: Scaling Training Environments for Scientific Agents from Code Repositories
https://arxiv.org/abs/2610.32448
POSEIDON 从科学代码仓库中提取复现、子流程、补全和纠错四类任务，并把它们转化为可执行、可验证的训练环境。作者据此构建 Pearl，包含来自7,110个公共仓库、覆盖10个学科的97,659个环境。它为科研智能体提供了更丰富的练习材料：运行已有分析、接续研究流程，并根据执行结果修正代码。
二、假设与实验：把探索推进到具体研究
【6】Open-ended Scientific Discovery with Possibilistic Reasoning
https://arxiv.org/abs/2610.11289
科学探索需要随着证据积累不断提出和检验假设。这篇论文用可能性理论描述这一过程，提出可计算的溯因效用来衡量发现进度，并设计可能性前沿搜索算法。在相应条件下，算法兼顾持续检验的统计有效性与渐近优化保证。它提供了一个方法框架，将假设空间的扩展、证据更新和搜索进度放在一起研究。
【7】OptScientist: Automated Discovery of Optimization Laws
https://arxiv.org/abs/2610.28562
OptScientist 尝试从观测数据中寻找背后的优化目标与约束，再提取紧凑的符号表达。其智能体流程结合文献先验，生成候选规律、概括机制，并建议下一步收集的数据。作者在包含99个物理来源优化问题的 OptFeynman，以及人类风险选择和货币政策数据上评估这一方法，为从现象走向可解释模型提供了具体案例。
【8】ADAPT for Science: A Multi-Agent System for Self-Evolving Scientific Optimization
https://arxiv.org/abs/2610.30851
ADAPT 将科学优化分成“在哪里搜索”和“怎样搜索”两个相互关联的决定。系统利用历史设计选择起点，把计算逐步分配给有潜力的方向，再根据执行反馈改进优化程序。论文以可微物理模拟器中的引力波探测器设计为对象，在相同评估预算下测试8种未见拓扑，展示了利用领域约束和历史经验提高搜索效率的路径。
【9】Accelerating scientific discovery with Co-Scientist
https://www.nature.com/articles/s41586-026-10644-y
Co-Scientist 围绕研究者给定的目标，组织多个智能体持续生成、评议、排序和改进假设，并允许研究者随时补充约束、调整方向。论文在药物再利用、新靶点和抗菌药耐药机制三个生物医学方向开展验证，其中急性髓系白血病的候选用药及组合方案经过体外实验检验。它展示了文献推理、假设筛选与实验验证之间的衔接。
【10】Collaborative AI agents for autonomous experimental research with solid-state quantum spins
https://arxiv.org/abs/2610.40589
这项研究让协作智能体围绕金刚石中的量子自旋提出问题、推导结果，并设计能够区分不同预测的实验。系统推导了预测一类微波脉冲序列响应所需的最少校准设置，再进行计算检查和实验检验。参考测量发现信号漂移后，智能体修订测量方案，最终获得满足既定验收条件的结果；实验反馈由此直接参与了研究路线的调整。
三、过程监督与训练：把反馈落到关键步骤
【11】The Missing Primitive: Diagnosing and Repairing Mathematical Reasoning in Large Language Models
https://arxiv.org/abs/2610.02191
这篇论文把数学理解拆成发现、生成、理解和执行四个维度，用 Mathematical Primitive 刻画解题所需的关键结构。作者进一步利用包含关键结构信息的推理进行选择性自蒸馏，将能力诊断与后训练结合，提升模型发现和运用解题思路的能力。
【12】STEP: Soft Trajectory Estimation of Prediction Correctness via Per-Step Probability Scoring
https://arxiv.org/abs/2610.34537
STEP 沿着推理步骤追踪候选答案的概率分布，用置信度及其变化估计最终输出是否正确。整个框架无需训练，通过轻量前向计算提取轨迹特征。作者发现，给后期较稳定的答案分布更高权重，能明显改善正确性估计。对具有明确候选答案的任务，这提供了一种利用已有推理过程进行质量判断的方法。
【13】LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
https://arxiv.org/abs/2610.17697
LeanPRM 让模型同时写出自然语言证明与配对的形式证明，再用 Lean 生成逐步标签，并由另一个模型过滤纯粹由形式语法引起的失败。由此得到的标签可用于训练自然语言证明验证器。它把形式检查器的反馈转化为可学习的过程监督，为长证明的自动评阅提供了数据来源；自然语言与形式步骤之间的配对是这条流程的关键。
【14】Guided-RLVR: Guided Exploration in Reinforcement Learning with Verifiable Rewards
https://arxiv.org/abs/2610.37041
Guided-RLVR 在训练采样中加入轻量控制器，通过具有语义作用的引导 token，推动模型尝试不同推理方向。作者在数学和代码任务中观察到更丰富的推理轨迹及性能提升。它关注的是探索发生的位置：在关键步骤改变后续走向，让一次训练中的多条尝试覆盖更多解法。
【15】Correlation-Aware Exploration for Long-Trace Reasoning
https://arxiv.org/abs/2610.34949
Info-GRPO 在训练提示中加入潜在种子，利用潜变量与整条推理轨迹之间的互信息组织探索。不同种子引导不同策略，同一种子下的策略则可以逐步收敛。论文在推理基准上报告了相对 GRPO 及熵正则化方法的收益。它将多样性的组织单位放在完整解题路径上，为长推理训练中的探索与收敛提供了新的协调方式。
四、搜索与证明：在验证反馈中推进
【16】Lean Graph Search for Formal Theorem Proving
https://arxiv.org/abs/2610.22339
LeanGraphSearch 把 Mathlib 中声明与其依赖前提连接成图，从语义检索得到的候选出发，沿多跳依赖寻找支撑引理，再重新排序。这样的搜索能触及与目标文字相似度较低、却在相关证明中经常出现的结果。论文还将检索接入 Lean 反馈循环，考察引理召回的提升如何转化为完整证明的成功率。
【17】Maestro: Agentic Formal Proof Development by Coordination
https://arxiv.org/abs/2610.25920
Maestro 的核心是对证明失败进行全局协调。局部证明者报告卡住的原因，协调者结合整个证明决定下一步：补充指导、修正错误引理，或撤回一段分解重新规划。论文在数学与软件验证任务上评估这一机制。它把失败信息变成调整证明计划的依据，也让多智能体之间的协作有了具体对象。
【18】h1: A Taste of the Bitter Lesson in Automated Theorem Proving
https://arxiv.org/abs/2610.35962
h1 给模型提供高效的 Lean 4 接口，通过验证反馈与自我反思持续推进证明，并研究增加推理时计算的效果。论文的消融和同模型比较强调了接口效率：反馈如何返回、一次尝试需要多少执行成本，都会影响最终解题率。这为证明系统的优化提供了直接切入点——让模型更顺畅地尝试、检查和修订。
【19】Efficient Proof Generation for Lean Statements with Multiple Candidate Answers
https://arxiv.org/abs/2610.34490
面对上游求解器给出的多个候选答案，这篇工作将答案选择、补充新答案和证明生成放进一次联合推理。论文报告，在所测基准上，它以约六分之一的 token 成本达到逐候选证明方法相同的成功率。此外，对于原本具有唯一答案的问题，如果两个不同答案都能在同一形式化陈述下获得证明，这也提供了定位语义失真的线索。
【20】PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
https://arxiv.org/abs/2610.31810
PaperFormalizer 从论文 LaTeX 源码出发，构建陈述依赖图，检查歧义与证明缺口，再完成 Lean 形式化。涉及论文含义的修订由作者决定。最终输出包括带注释的修订稿、修改记录和可追溯到原文陈述的 Lean 代码。这项工作展示了作者参与的论文核验流程，也让后续研究有机会直接复用经过检查的形式化结果。
五、语义与迁移：检查结论，积累解题经验
【21】MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization
https://arxiv.org/abs/2610.35269
MechAlign 从整个项目的依赖关系检查论文陈述与形式化实现是否对应。工具 LeanTrace 提取声明依赖图，保留定义内容和结构约束，再交给模型结合上下文评阅，并给出问题所在的局部证据。它把审查范围扩展到主定理背后的定义与假设，使研究者能够追踪一项结论在代码中究竟表达了什么。
【22】Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs
https://arxiv.org/abs/2610.36767
这篇工作以带专家评分的 USAMO 2025 候选解为基础，系统评测模型对自然语言证明的评分能力，并用 TROJAN 生成包含隐蔽问题的对抗证明。作者进一步提出 MABGrader，将评分建模为离散分数上的多臂老虎机选择。数据、对抗样例和评分方法共同构成了一套检验证明评阅质量的工具。
【23】When Form Changes but Logic Doesn’t: Building Logic-invariant LLMs through Logical Structure
https://arxiv.org/abs/2610.25402
同一道逻辑问题可以有多种表达。LoGIST 将输入映射为表示逻辑结构的决策图，再把图编码为逻辑嵌入，辅助模型推理。论文报告，这种做法提升了模型面对逻辑等价表述时的一致性，以及对未见逻辑形式的泛化。对推理评测而言，它增加了一条清楚的检查轴：题面变化之后，结论能否保持稳定。
【24】Mathematical Transfer in LLMs Follows Reasoning Approach More Than Topic
https://arxiv.org/abs/2610.00331
数学知识怎样跨题型迁移？这篇论文交叉安排概率、组合、数论、几何等主题与不变量、双计数、补集、抽屉原理等解题方法，比较“同方法、不同主题”和“同主题、不同方法”的训练来源。在所测组合中，共享解题方法带来更好的迁移。这个结果提示我们，组织数学训练数据时，可以把推理策略作为一条独立的标注维度。
【25】What Outcome RL Buys: Finishing, Reliability, Rarely Reach
https://arxiv.org/abs/2610.34894
这篇分析将结果奖励强化学习带来的变化拆成三项：在预算内完成回答、完成后的正确率，以及相对基础模型新增的解题覆盖。作者在固定 token 预算下比较20个模型，发现预算紧张时收益主要来自完成率，预算较充足时更多体现为可靠性。文中的新增覆盖按有限次采样定义；这一分解有助于读者具体理解一次分数提升来自哪里。
六、工具与系统：连接实验设备和推理流程
【26】An agentic artificially intelligent X-ray scientist
https://www.nature.com/articles/s42256-026-01261-5
这篇工作把智能体接入同步辐射实验流程，完成单晶样品对准所需的规划、指令生成和观测分析。系统先在虚拟六圆衍射仪上开发和测试，再部署到真实束线，识别参考反射并确定取向矩阵。首次真实演示由实验人员转执行模型指令，以满足设施安全要求。这个案例具体展示了推理模型如何利用测量反馈推进仪器操作。
【27】S3AC: Stabilized, Selective, and Scalable Actor-Critic for LLM Reasoning
https://arxiv.org/abs/2610.35518
S3AC 围绕长推理链中的价值模型训练，设计稳定的 actor-critic 流程。训练后的 critic 提供 token 级优势和题目级基线，后者又用于估计难度，在生成之前选择更值得投入预算的题目。它把反馈精度与采样效率联系起来：既研究一次回答中哪些位置值得更新，也研究下一轮训练应该选择哪些问题。
【28】CAMR: Compatibility-Aware Memory Replay for Continual Learning in Large Language Models
https://arxiv.org/abs/2610.36734
CAMR 面向持续学习，同时决定怎样学习新样本、怎样回放历史样本。系统结合兼容性检查与记忆门控，在学习新例、联合强化相关例以及跳过已掌握的重复例之间选择。作者在事实更新和包含数学、代码等任务的序列上评估知识获取与保留。它关注的是持续更新时，有限训练预算怎样分配给新旧内容。
【29】Harness-Delta Attribution: Dissecting Gains From Harness Evolution
https://arxiv.org/abs/2610.22466
HDA 提出一套系统增益归因协议，将外部提示、工具与流程优化带来的提升，拆成基准特定过拟合、推理时计算增加所解释的部分，以及剩余部分；剩余量给出可泛化改进的上界。通过留出任务、分布变化和计算预算对齐，这套协议让不同系统的提升更容易比较，也为下一轮优化指出值得追踪的来源。
【30】Understanding the Benefits of Scaffolds through Computational Separations
https://arxiv.org/abs/2610.27157
这篇论文研究外部流程多次调用模型并保存跨调用状态时，能获得怎样的计算能力，以及这些收益能在多大程度上通过轨迹蒸馏传给学生模型。作者在特定计算模型与复杂性假设下给出表示能力分离，并结合竞赛数学实验考察模型容量、推理链长度与任务难度的影响。它为理解外部状态和控制流程的作用提供了理论视角。
