arXiv:2502.04671v2 宣告类型: 替换
摘要：神经网络在交互式证明助手（ITPs）如Lean和Coq中的自动定理证明方面展现出了巨大的潜力。然而，大多数神经定理证明模型仅限于特定的ITPs，这限制了不同ITPs之间的跨语言迁移。我们通过一个名为${\rm P{\small ROOF}W{\small ALA}}$的多语言证明框架解决了这一问题，该框架允许神经定理证明器与两个已建立的ITPs（Coq和Lean）进行标准化交互。它能够收集多语言证明步骤数据——即在ITP状态上执行证明操作的结果数据——用于训练神经证明器。${\rm P{\small ROOF}W{\small ALA}}$允许通过高效并行证明搜索算法系统地评估模型在不同ITPs和问题领域中的性能。我们展示了${\rm P{\small ROOF}W{\small ALA}}$支持的多语言训练可以实现ITPs之间的成功迁移。具体来说，基于${\rm P{\small ROOF}W{\small ALA}}$生成的Coq和Lean数据的混合训练模型，在标准的prove-at-$k$指标上优于仅使用Coq或仅使用Lean的数据训练的模型。我们开源了所有代码，包括${\rm P{\small ROOF}W{\small ALA}}$框架的代码（https://github.com/trishullab/proof-wala）和多语言ITP交互框架的代码（https://github.com/trishullab/itp-interface）。
arXiv:2502.00691v2 宣称类型: 替换
摘要：最近在语言模型（LMs）用于数学问题解决方面的进展结合了链式思考（CoT）推理和代码执行，以利用它们各自的优点。然而，现有的混合框架存在一个关键限制：它们依赖于外部指令或固定的代码集成模板，缺乏元认知意识——即动态评估内在能力并在何时何地自主决定如何集成工具的能力。这种僵化促使我们研究自主代码集成，使模型能够在其训练过程中随着推理能力的演变来适应工具使用策略。
虽然增强学习（RL）在大规模提升语言模型（LLMs）的推理能力方面展现出潜力（例如，DeepSeek-R1），但我们展示其在学习自主代码集成方面的低效率，这是因为探索CoT-代码交替模式的广泛组合空间不足。为解决这一挑战，我们提出了一种新颖的期望最大化（EM）框架，该框架将结构化探索（E步）与离策RL优化（M步）相结合，创建了一种自我强化循环，即元认知工具使用决策与其不断发展的能力之间相互促进。实验结果显示，我们的方法通过改进探索实现了更优的结果。值得注意的是，我们的7B模型在MATH500上提高了11%以上，在AIME上的表现提高了9.4%，而无需类似o1的CoT。
arXiv:2502.00510v2 宣告类型: 替换
摘要：大型语言模型（LLM）代理框架通常采用模块化结构，整合计划、推理、动作执行和反思等组件，以应对复杂的任务。然而，量化每个模块对整体系统性能的贡献仍然是一个重大挑战，阻碍了优化和可解释性。为了解决这一问题，我们引入了CapaBench（能力评估基准），该基准框架基于合作博弈论的Shapley值，系统地度量了模块及其交互对代理架构的影响。通过在所有可能的组合中替换默认模块为测试变体，CapaBench提供了一种归因方法。关键贡献包括：(1) 我们首次提出了基于Shapley值的方法来量化LLM代理中能力的贡献；(2) 具有高Shapley值的模块在组合时始终能带来可预测的性能提升，从而使优化更具针对性；(3) 我们构建了一个涵盖多个领域和实际任务场景的多轮数据集，包含了超过1,500个条目，这使得代理能力的全面评估成为可能。CapaBench弥合了组件级评估与整体系统评估之间的差距，为优化模块化LLM代理并推动其在复杂、实际场景中的部署提供了操作性见解。
arXiv:2501.16207v2 公告类型：替换
摘要：基于AI的形式数学推理研究展现出了不可阻挡的增长趋势。这些研究在国际数学奥林匹克(IMO)等数学竞赛中表现出色，并取得显著进展。本文集中于形式验证，这是形式推理的直接应用场景，并将其分解为子任务。我们通过提炼gpt-4o，构建了跨五种形式规范语言（Coq、Lean4、Dafny、ACSL和TLA+）的18000个高质量指令-响应对，并针对包括最近流行的DeepSeek-R1在内的十个开源LLMs进行了评估。我们还微调了几种7-8B的小模型，使其在性能上与Deepseek-R1-671B相当。有趣的是，我们观察到，使用形式数据进行微调也增强了数学、推理和编码能力。微调后的模型可在以下地址发布：https://huggingface.co/fm-universe。
arXiv:2501.15857v2 公告类型: 替换
摘要：人类通过整合各种来源的知识展现出卓越的组合推理能力。例如，如果某人从一个来源学到 (B = f(A))，从另一个来源学到 (C = g(B))，他们可以推断出 (C = g(B) = g(f(A)))，即使没有同时遇到 (ABC)，这展示了人类智能的泛化能力。在本文中，我们介绍了一个合成学习任务“FTCT”（训练阶段分散，测试阶段连贯）来验证变压器在复制这种能力方面的潜力并解释其内在机制。在训练阶段，数据由整个因果图中的分散知识片段组成。在测试过程中，变压器必须通过整合这些片段来推断完整的因果图踪迹。我们的研究发现，少量的思维链提示使变压器能够在FTCT上进行组合推理，即使这些组合未出现在训练数据中。此外，组合推理能力的出现与模型复杂性和训练-测试数据的相似性之间存在强烈的相关性。我们不仅从理论上而且从实验上提出了变压器在训练过程中学习了一个潜在的可泛化程序，在测试过程中实现了有效的组合推理。
arXiv:2501.13622v2 宣告类型: 替换
摘要：过程奖励模型（PRM）在数学推理任务中发挥着重要作用，需要高质量的监督过程数据。然而，我们观察到大型语言模型（LLMs）生成的推理步骤往往不能严格体现出逐步递增的信息，导致冗余，从而妨碍有效的推理。为了解决这一问题，我们提出了一种简单而有效的从粗到细的方法。而不是专注于冗余步骤的检测，我们的方法首先建立一个粗粒度的窗口，将相邻的推理步骤合并为统一的整体步骤。然后逐步减少窗口大小以提取细粒度的推理步骤，从而在不同粒度下进行数据收集进行训练。通过利用这种分层细化过程，\model 减轻冗余同时保留了重要的细粒度知识。在三个损失标准下的两个推理数据集上的广泛实验验证了 \model 的有效性和灵活性。
arXiv:2501.11429v2 通知类型: 更新
摘要：最近的研究揭示了当前在可解释人工智能（XAI）中使用Shapley值中存在的关键缺陷，即所谓的SHAP得分。这些缺陷非常严重，因为提供给人类决策者的得分可能会误导人。尽管这些负面结果可能会让人认为Shapley值不应该在XAI中使用，但本文持相反观点。具体而言，本文提出了一种新的SHAP得分定义，克服了现有的缺陷。此外，论文概述了一种实用高效的解决方案，用于严格估计新的SHAP得分。初步的实验结果证实了我们的观点，并进一步强调了当前SHAP得分的缺陷。
arXiv:2501.09640v2 通知类型: 替换
摘要: 从传统的纸质记录到复杂的电子健康记录（EHR）的关键转变，使通过描述性统计系统地收集和分析患者数据成为可能，从而为患者群体中的模式和趋势提供了洞察。这一演变继续向预测分析发展，使医疗服务提供者能够在问题发生之前预测患者的预期结果和潜在并发症。从基本的数字记录保存到复杂的预测建模和数字孪生，反映了医疗保健向更加集成、以患者为中心的方法的转变，这些方法结合了数据驱动的见解和个人化护理的交付。本章探讨了医疗信息系统的发展和意义，从考察英国和美国的EHR实施开始。它提供了国际疾病分类（ICD）系统的综合概述，追踪其从ICD-9到ICD-10的发展过程。这一讨论的核心是MIMIC-III数据库，这是医疗数据共享的一个里程碑成就，可能是目前世界上研究人员可用的最全面的重症监护数据库。MIMIC-III使高质量医疗数据的访问变得民主化，为研究和分析提供了前所未有的机会。本章探讨了其结构、临床结果分析能力及其通过案例研究的应用，重点是死亡率和住院时间指标、生命体征提取和ICD编码。通过详细的实体-关系图和实际示例，本文阐明了MIMIC复杂的数据结构，并展示了不同的查询方法可能导致的结果稍有不同，强调了理解数据库架构对于准确数据提取的重要性。
arXiv:2501.09628v2 宣布类型: 替换
摘要：随着人工智能（AI）在医疗卫生服务中越来越广泛的应用，本文探讨了开发可靠和伦理的临床决策支持系统（CDSS）的关键方面。从传统的统计模型过渡到复杂的机器学习方法开始，本文考察了严格验证策略和性能评估方法，包括模型校准和决策曲线分析在其中的关键作用。本文强调，在医疗卫生中创建值得信赖的AI系统不仅需要技术上的准确性，还需要仔细考虑公平性、可解释性和隐私性。确保通过AI实现公平的医疗卫生交付的挑战得到了强调，讨论了识别并在临床预测模型中减轻偏差的方法。随后，本文深入探讨了以人为中心的CDSS的核心——可解释性。这一焦点反映了这样的理解：医疗专业人员不仅需要信任AI的建议，还需要理解其背后的推理过程。讨论进一步深入到医疗AI系统的隐私漏洞，从深度学习模型中的数据泄漏到模型解释的高级攻击。文本探讨了保护隐私的策略，如差分隐私和联邦学习，同时承认在隐私保护与模型性能之间的固有权衡。从技术验证到伦理考量的这一进展，反映了开发能够无缝且可靠地融入日常临床实践的AI系统，同时保持最高标准的病人护理和数据保护的复杂挑战。
arXiv:2501.02725v2 Announce Type: replace
摘要：人工智能（AI）的迅猛发展，特别是生成性AI和大型语言模型（LLMs）的进步，对创意产业产生了深刻影响，通过促进创新内容创作、提升工作流程效率以及使创意工具更加普及。本文探讨了自2022年我们上次回顾以来的重大技术变革，突显了这些发展如何扩大了创意机会和效率。这些技术进步增强了文本到图像、文本到视频和多模态生成技术的能力。特别是，大型语言模型的关键突破建立了对话AI的新基准，而在图像生成器方面的进步则彻底改变了内容创作。我们还讨论了AI在后期制作工作流程中的集成，这已显著加速并精细化了传统流程。尽管这些创新带来了许多机遇，但媒体行业仍面临挑战，特别是创意内容产生的通信流量需求。因此，本文还涵盖了数据压缩和质量评估。此外，我们指出了统一的AI框架的趋势，这种框架能够解决多种创意任务，并强调人类监督的重要性，以减少AI生成的不准确性。最后，我们探讨了AI在创意领域未来的潜力，强调需要导航新兴挑战，以最大化其益处并应对相关风险。