arXivDaily arXiv每日学术速递 周一至周五更新

AI 大模型

大模型推理能力

大模型数学、逻辑、规划、多步推理和测试时计算能力。

共收录 1117 信号源:cs.CL, cs.AI, cs.LG

1. 代码与定理证明 1117 篇

2606.17073 2026-06-17 cs.RO cs.AI 新提交 57%

Extracting Semantics: LLM-Guided Automatic Population of Robot Ontology from URDF

提取语义:从URDF自动构建机器人本体的LLM引导方法

Bastien Dussard, Guillaume Sarthou

机构 * LAAS-CNRS, Department of Robotics, Toulouse, France(法国图卢兹机器人系CNRS实验室)

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

AI总结 提出利用大语言模型从URDF文件自动生成机器人语义本体,通过多数投票和语法验证确保与现有本体对齐,初步实验表明该方法能有效桥接低层描述与高层知识表示。

Journal ref 18th International Conference on Social Robotics (ICSR 2026), University of London, Jul 2026, Londres, United Kingdom

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.15258 2026-06-16 cs.AI 新提交 57%

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

Mask-Proof: 一种基于LLM的数学证明自动数据整理流水线

Jierui Zhang, Siyuan Tan, Xinhang Li, Longzhuangzhi Lin, Dailin Li, Chengfeng Gu, Xinping Li, Yaxian Hao, Shengjia Liang, Yuxiang Ren, Wenhao Liu

机构 * School of Computer Science, Beijing University of Posts and Telecommunications(北京邮电大学计算机学院) Graduate College for Engineers, Beijing University of Posts and Telecommunications(北京邮电大学研究生院工程师学院) School of Mathematical Sciences, Fudan University(复旦大学数学科学学院) School of Cyberspace Security, Beijing University of Posts and Telecommunications(北京邮电大学网络空间安全学院) School of Computer Science and Technology, Dalian University of Technology(大连理工大学计算机科学与技术学院) Chu Kochen Honors College, Zhejiang University(浙江大学竺可桢学院) Department of Psychological and Cognitive Sciences, Tsinghua University(清华大学心理学与认知科学系) State Key Laboratory of Virtual Reality Technology and Systems, Beihang University(北京航空航天大学虚拟现实技术与系统国家重点实验室) School of Intelligence Science and Technology, Nanjing University(南京大学智能科学与技术学院)

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

AI总结 提出Mask-Proof流水线,将真实证明转化为可自动检查的掩码步骤任务,通过LLM等价性判断器评估模型推理,构建包含292个问题的基准,推理增强模型性能提升12%-27%。

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.15096 2026-06-16 cs.AI 新提交 57%

VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization

VGPT-RSI 用于 RH 邻近形式化进展:边界证书、已验证的有限 Lagarias 不等式和显式故障定位

Zhixin Hu, Tao Xu, Xiaodian Sun, Li Jin, Momiao Xiong

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

AI总结 提出 VGPT-RSI 系统,通过构造并验证有限 RH 边界证书和 Lagarias 准则的有限形式化,实现 Riemann 假设邻近问题的部分形式化进展,并明确识别剩余数学障碍。

Comments 31 pages, 3 figures

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.15078 2026-06-16 cs.AI cs.GT physics.soc-ph 新提交 57%

Cognitive Debt: AI as Intellectual Leverage and the Dynamics of Systemic Fragility

认知债务:作为智力杠杆的AI与系统性脆弱性的动态机制

Shuchen Meng

机构 * New York University(纽约大学)

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

AI总结 本文提出认知债务的形式化理论,通过建立包含认知资本和认知债务的状态变量模型,证明理性代理人会积累认知债务,并导致认知明斯基时刻和系统性脆弱性。

Comments 46 pages, 3 figures. Preliminary version; comments welcome

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.12291 2026-06-16 cs.CL 新提交 57%

Measuring Epistemic Resilience of LLMs Under Misleading Medical Context

测量大语言模型在误导性医疗上下文下的认知韧性

Hongjian Zhou, Xinyu Zou, Jinge Wu, Sean Wu, Junchi Yu, Bradley Max Segal, Tobias Erich Niebuhr, Sara Amro, Michael Petrus, Sheikh Momin, Alexandra M. Cardoso Pinto, Rachel Niesen, Laura Sophie Wegner, Dhruv Darji, Jung Moses Koo, Joshua Fieggen, Kapil Narain, Mingde Zeng, Lei Clifton, Linda Shapiro, Fenglin Liu, David A. Clifton

机构 * University of Oxford(牛津大学) University of Washington(华盛顿大学) University College London(伦敦大学学院) University of Waterloo(滑铁卢大学)

专题命中 代码与定理证明 :reasoning(abstract);分类 cs.CL

AI总结 本研究提出MedMisBench基准,通过注入误导性上下文测试大语言模型在医疗场景中的认知韧性,发现模型准确率从71.1%降至38.0%,权威性虚假信息攻击成功率达69.5%。

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.13392 2026-06-15 cs.AI 新提交 57%

MiniMax Sparse Attention

MiniMax 稀疏注意力

Xunhao Lai, Weiqi Xu, Yufeng Yang, Qiaorui Chen, Yang Xu, Lunbin Zeng, Xiaolong Li, Haohai Sun, Haichao Zhu, Vito Zhang, Jinkai Hu, Jiayao Li, Rui Gao, Zekun Li, Songquan Zhu, Jingkai Zhou, Pengyu Zhao

机构 * MiniMax Peking University(北京大学) NVIDIA(英伟达) Zhejiang University(浙江大学) Huazhong University of Science and Technology(华中科技大学)

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

AI总结 提出 MiniMax 稀疏注意力(MSA),一种基于分组查询注意力的块级稀疏注意力机制,通过轻量索引分支选择 Top-k 键值块,实现高效长上下文处理,在 109B 模型上以 1M 上下文减少 28.4 倍注意力计算,并带来 14.2 倍预填充和 7.6 倍解码加速。

Comments 30 pages, 14 figures

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.13282 2026-06-12 cs.AI 新提交 57%

ERTS: Adversarial Robustness Testing of Ethical AI via Semantic Perturbation in a Bounded Consequence Space

ERTS: 通过有界后果空间中的语义扰动进行伦理AI的对抗鲁棒性测试

Pratyush Chaudhari

机构 * Pratyush Chaudhari(普拉蒂什·查德哈里)

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

AI总结 提出伦理鲁棒性测试系统(ERTS),通过有界伦理后果空间、语义扰动和领域自适应评估,测试AI在伦理推理中的对抗鲁棒性,实验表明仅33%模型通过测试。

Comments 8 pages, 10 tables

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.12594 2026-06-12 cs.AI 新提交 57%

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Pythagoras-Prover: 通过增强型Lean形式化推进高效形式化证明

Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

机构 * Imperial College London(伦敦帝国学院) University of Edinburgh(爱丁堡大学) Nanyang Technological University(南洋理工大学) MBZUAI(穆罕默德·本·扎耶德人工智能大学)

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

AI总结 提出Pythagoras-Prover系列,包括自回归和扩散模型,通过课程SFT、动态过滤和增强型Lean形式化(ALF)扩展验证数据,在MiniF2F-Test上以更少参数超越DeepSeek-Prover-V2。

Comments Pythagoras-Prover: Technical Report

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.27628 2026-06-12 cs.AI cs.CY cs.ET cs.MA cs.SY eess.SY 版本更新 57%

Intelligence as Managed Autonomy: Failure, Escalation, and Governance for Agentic AI Systems

智能作为受管自主:代理型AI系统的失败、升级与治理

Srini Ramaswamy

机构 * DNRS.ai USA(DNRS.ai美国公司)

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

AI总结 本文提出SMARt模型,通过形式化能力检测认知漂移、暂停推理、尝试恢复并在可靠性下降时放弃控制,以解决自主AI系统中的幻觉和持续不合理行为问题。

Comments This peer-reviewed paper is to appear in the Journal of Intelligent and Robotic Systems

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.09032 2026-06-09 cs.CL 新提交 57%

Bridging the Agent-World Gap: Text World Models for LLM-based Agents

弥合智能体-世界鸿沟:面向基于LLM的智能体的文本世界模型

Yixia Li, Hongru Wang, Peng Lai, Zhiwen Ruan, He Zhu, Youxin Zhu, Ganlong Zhao, Minda Hu, Yun Chen, Sibei Yang, Peng Li, Jeff Z. Pan, Jia Pan, Guanhua Chen, Yang Liu, Guanbin Li

机构 * Southern University of Science and Technology(南方科技大学) University of Edinburgh(爱丁堡大学) Peking University(北京大学) Sun Yat-sen University(中山大学) The Chinese University of Hong Kong(香港中文大学) Shanghai University of Finance and Economics(上海财经大学) Tsinghua University(清华大学) The University of Hong Kong(香港大学)

专题命中 代码与定理证明 :planning(abstract);分类 cs.CL

AI总结 本文系统综述了面向基于LLM的智能体的文本世界模型,围绕形式化框架和智能体生命周期,涵盖基础定义、构建范式、应用(训练时经验合成与推理时规划、验证、适应)及评估,旨在整合该领域并明确设计空间与开放挑战。

Comments Code: https://github.com/sustech-nlp/awesome-text-world-models

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.08256 2026-06-09 cs.AI cs.DL 新提交 57%

Traxia: A Framework for Verifiable, Agent-Native Scientific Publishing

Traxia:一个可验证的、智能体原生的科学出版框架

Wisdom Dogah

机构 * Faculty of Computing and Mathematical Sciences, University of Mines and Technology (UMaT), Tarkwa, Ghana(加纳塔夸矿业与技术大学计算与数学科学学院) BlackMatrix AI Research, Accra, Ghana(加纳阿克拉BlackMatrix AI研究院)

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

AI总结 提出Traxia框架,通过智能体身份、可验证出版、四层同行评审、声誉机制和知识图谱,解决科学出版中可验证性、归属和可重复性问题。

Comments 22 pages, 3 figures, 3 tables. Preprint. Under active development. Comments welcome

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.22763 2026-06-09 cs.AI 版本更新 57%

Advancing Mathematics Research with AI-Driven Formal Proof Search

用AI驱动的形式证明搜索推进数学研究

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

机构 * Google DeepMind(谷歌DeepMind) Aarhus University(奥胡斯大学)

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

AI总结 本文研究了如何利用大型语言模型生成形式证明,以解决开放性数学问题,并展示了AI辅助形式证明搜索在数学研究中的应用和贡献。

Comments The first three authors and the last author have equal contributions. The first three authors are in random order

详情

展开后加载摘要…

URL PDF HTML 收藏
2508.11874 2026-06-09 cs.GT cs.AI cs.DS cs.LO cs.PL 版本更新 57%

Discovering Expert-Level Nash Equilibrium Algorithms with Large Language Models

利用大型语言模型发现专家级纳什均衡算法

Hanyu Li, Dongchen Li, Xiaotie Deng

机构 * CFCS, School of Computer Science, Peking University, Beijing, China(计算机科学系,北京大学,北京,中国) School of Computing and Data Science, The University of Hong Kong, Pokfulam, Hong Kong(计算与数据科学学院,香港大学,薄扶林,香港)

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

AI总结 提出LegoNE框架,将专家证明策略编码为符号语言,自动验证算法的最坏情况保证,结合推理型LLM重新发现并改进了多人博弈的近似纳什均衡算法。

Comments accepted by Nature Communications

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.07113 2026-06-08 cs.AI 新提交 57%

Beyond Post-hoc Explanation: Toward Glassbox AI via Probabilistic Mediation

超越事后解释:通过概率中介迈向玻璃箱AI

Manuele Leonelli

机构 * Manuele Leonelli(曼努埃尔·莱奥内利)

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

AI总结 针对大语言模型在关键领域的不透明性,提出玻璃箱框架,利用贝叶斯网络作为事前中介层,实现可审计推理、不确定性量化和可争议输出。

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.06531 2026-06-08 cs.AI quant-ph 新提交 57%

CARVE-Q: Quantum-Proposed, Classically Certified Interactive Driving Repair

CARVE-Q:量子提议、经典认证的交互式驾驶修复

Yifan Wang

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

AI总结 针对被否决的驾驶操作,提出CARVE-Q架构,通过量子最小搜索加速修复格搜索,同时保持安全认证的经典性,实现可审计的交互修复。

Comments 9 pages, 3 figures

详情

展开后加载摘要…

URL PDF HTML 收藏
2604.17948 2026-06-08 cs.CR cs.AI cs.MA 版本更新 57%

RAVEN: Retrieval-Augmented Vulnerability Exploration Network for Memory Corruption Analysis in User Code and Binary Programs

RAVEN: 用于用户代码和二进制程序中内存损坏分析的检索增强漏洞探索网络

Parteek Jamwal, Minghao Shao, Boyuan Chen, Achyuta Muthuvelan, Asini Subanya, Boubacar Ballo, Kashish Satija, Mariam Shafey, Mohamed Mahmoud, Moncif Dahaji Bouffi, Pasindu Wickramasinghe, Siyona Goel, Yaakulya Sabbani, Hakim Hacid, Mthandazo Ndhlovu, Eleanna Kafeza, Sanjay Rawat, Muhammad Shafique

机构 * University of California, Berkeley(加州大学伯克利分校)

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

AI总结 提出RAVEN框架,结合LLM代理与检索增强生成,自动生成遵循Google Project Zero模板的漏洞分析报告,在105个样本上平均质量得分54.21%。

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.23809 2026-06-05 eess.SY cs.LG cs.SY 57%

Advanced AI Service Provisioning in O-RAN through LLM Engine Integration

通过LLM引擎集成在O-RAN中的高级AI服务提供

Seyed Bagher Hashemi Natanzi, Pranshav Gajjar, Bo Tang, Vijay K. Shah

机构 * Department of Electrical and Computer Engineering, Worcester Polytechnic Institute(电气与计算机工程系,沃斯特理工学院) Department of Electrical and Computer Engineering, North Carolina State University(电气与计算机工程系,北卡罗来纳州立大学)

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

AI总结 提出一种双脑架构,结合LLM的推理能力和轻量级ML引擎的实时性,实现O-RAN中AI服务的自动化部署与配置。

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.04450 2026-06-04 cs.CL cs.CY 57%

Listening to the Workforce: Measuring Construction Worker Safety Attitudes from Social Media Discourse Using LLMs

倾听劳动力:使用LLMs从社交媒体话语中测量建筑工人安全态度

Farouq Sammour, Yuxin Zhang, Zhenyu Zhang

机构 * Texas A&M University(德克萨斯A&M大学)

专题命中 代码与定理证明 :reasoning(abstract);分类 cs.CL

AI总结 提出并验证了建筑安全态度框架(CSAF),通过LLM分类器从Reddit社区话语中测量工人安全态度,实现高精度多维分析。

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.03303 2026-06-04 cs.AI 57%

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

LEAP:利用智能体框架增强形式化数学的大语言模型

Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart, Quoc V Le, Burak Gokturk, Thang Luong, Tomas Pfister, Nanyun Peng

机构 * Google Cloud AI Research(谷歌云人工智能研究) Google Cloud(谷歌云) Google DeepMind(谷歌DeepMind)

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

AI总结 提出LEAP智能体框架,通过分解问题、与Lean编译器交互及自我优化,使通用大模型在形式化定理证明上达到最先进性能,并在Putnam竞赛和Lean-IMO-Bench上超越专业系统。

详情

展开后加载摘要…

URL PDF HTML 收藏
2606.01160 2026-06-02 cs.AI 57%

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形式验证。

详情

展开后加载摘要…

URL PDF HTML 收藏
2511.12081 2026-06-02 cs.IR cs.LG 57%

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

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.31064 2026-06-01 cs.IR cs.AI 57%

Fighting Numerical Hallucinations via Data-centric Compilation for Online Financial QA

通过数据为中心的编译对抗在线金融问答中的数值幻觉

Hao Chen, Xing Tang, Qirui Liu, Weijie Shi, Shiwei Li, Fuyuan Lyu, Weihong Luo, Xiku Du, Xiuqiang He

机构 * Shenzhen Technology University(深圳科技大学) FiT, Tencent(腾讯金融科技部) South China University of Technology(华南理工大学) The Hong Kong University of Science and Technology(香港科学与技术大学) Huazhong University of Science and Technology(华中科技大学) McGill University(麦吉尔大学)

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

AI总结 提出数据为中心推理编译器(DCRC),通过对抗数据构建、多阶段训练和编译执行推理流程,解决在线金融问答中检索增强生成面临的噪声敏感、计算脆弱和可审计性危机,实现可靠的数值推理。

Comments Accepted by KDD 2026 ADS track

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.30914 2026-06-01 cs.LG cs.SE 57%

Automating Formal Verification with Reinforcement Learning and Recursive Inference

用强化学习和递归推理自动化形式验证

Max Tan

机构 * Department of Electrical Engineering and Computer Science(电气工程与计算机科学系) Massachusetts Institute of Technology(麻省理工学院)

专题命中 代码与定理证明 :verifier(abstract);分类 cs.LG

AI总结 研究通过可验证奖励的强化学习和验证器引导的推理搜索,提升大语言模型生成验证程序和证明的能力,在Dafny和Lean上取得显著进展。

Comments Master's thesis, 140 pages, 16 figures, 17 tables

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.30861 2026-06-01 cs.AI 57%

Distilling LLM Feedback for Lean Theorem Proving

蒸馏LLM反馈用于Lean定理证明

Gaetan Narozniak, Gérard Biau, Rémi Munos, Ahmad Rammal, Pierre Marion

机构 * FAIR at Meta(Meta 的 FAIR 部门) Inria(法国国家科学与技术研究院) Sorbonne Université(索邦大学) Institut universitaire de France(法国国家科学研究院) CERMICS École des Ponts ParisTech(巴黎理工学院 CERMICS 实验室) ENS, PSL Research University(巴黎高等师范学院与巴黎科学实验室)

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

AI总结 提出反馈蒸馏方法,通过让模型在token级别匹配自身分布(基于语言模型提供的特权反馈)来训练,以解决GRPO在推理后训练中的稀疏奖励和模式崩溃问题,并在Lean4定理证明中取得更好效果。

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.30144 2026-05-29 cs.AI cs.MA 57%

AgentSchool: An LLM-Powered Multi-Agent Simulation for Education

AgentSchool:基于LLM的多智能体教育模拟系统

Yulei Ye, Wenhao Li, Zhong Wen, Yunshu Huang, Yichen Hu, Zifan Wei, Yige Wang, Xinyu Xie, Haoxuan Yang, Yanjun Huang, Ruijia Li, Hong Qian, Yu Song, Bo Jiang, Bingdong Li, Lijun Li, Bo Zhang, Pinlong Cai, Xingcheng Xu, Shuangye Chen, Xia Hu, Liang He, Aimin Zhou, Jingjing Qu, Jing Shao, Xiangfeng Wang

机构 * Shanghai Institute of AI for Education(上海人工智能教育研究院) School of Computer Science and Technology(计算机科学与技术学院) East China Normal University(东华大学) School of Design(设计学院) Faculty of Education(教育学院) Shanghai Artificial Intelligence Laboratory(上海人工智能实验室)

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

AI总结 提出AgentSchool,一种LLM驱动的多智能体模拟器,通过可成长的学生智能体(带知识图谱、思维工作流和错误概念)与自适应教师智能体(基于最近发展区)模拟学习过程,支持多尺度模拟,实验验证了其生成差异化掌握轨迹和符合课堂社会理论的行为模式。

Comments 39 pages, 10 figures

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.27485 2026-05-28 cs.LO cs.LG cs.SE 57%

Automating Formal Verification with Agent-Guided Tree Search

利用智能体引导的树搜索自动化形式验证

Leo Yao

机构 * Massachusetts Institute of Technology(麻省理工学院) Department of Electrical Engineering and Computer Science(电气工程与计算机科学系)

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

AI总结 本文提出智能体引导的树搜索方法,通过状态和上下文两种编排器改进基于大语言模型的Lean形式验证代码生成性能,在基准测试中达到95.0%的通过率。

Comments 78 pages, 8 figures

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.26959 2026-05-28 cs.LO cs.CL 57%

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

MerLean-Prover:用于 Lean 4 定理证明的递归循环框架

Jinzheng Li, Zeru Zhu, Yuanjie Ren

机构 * Northeastern University(东北大学) Stony Brook University(石溪大学) Massachusetts Institute of Technology(麻省理工学院)

专题命中 代码与定理证明 :planning(abstract);分类 cs.CL

AI总结 提出一种基于递归循环框架的端到端 Lean4 定理证明器 MerLean-Prover,通过规划、检查与证明三种智能体协作,无需微调或定制强化学习,在 FormalQualBench 和 Putnam2025 上超越现有开源基线。

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.27320 2026-05-27 cs.AI cs.CY econ.GN q-fin.EC 57%

Modeling Agentic Technical Debt and Stochastic Tax: A Standalone Framework for Measurement, Simulation, and Dashboarding

建模代理技术债务与随机税:一个用于测量、模拟和仪表盘展示的独立框架

Muhammad Zia Hydari, Raja Iqbal, Narayan Ramasubbu

机构 * School of Business, University of Pittsburgh(匹兹堡大学商学院)

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

AI总结 本文提出一个形式化且可管理的框架,区分代理技术债务(累积的设计与治理负债存量)与随机税(使用随机代理时产生的运营负担流),并通过应付账款模拟和电子表格说明其应用。

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.27051 2026-05-27 cs.SE cs.AI 57%

ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification

ConVer:使用合约和循环不变式合成实现可扩展的形式化软件验证

Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous, Konstantin Korovin, Lucas C. Cordeiro

机构 * The University of Manchester(曼彻斯特大学)

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

AI总结 提出一种自上而下的组合验证工具ConVer,利用大语言模型合成函数合约,并通过CEGAR-CEGIS循环迭代精炼合约,以解决大规模C程序形式化验证中的状态空间爆炸问题。

Comments 12 pages; 6 figures

详情

展开后加载摘要…

URL PDF HTML 收藏
2605.20690 2026-05-27 cs.AI 57%

Declarative Data Services: Structured Agentic Discovery for Composing Data Systems

声明式数据服务:用于组合数据系统的结构化智能体发现

Shanshan Ye, Duo Lu

机构 * Northeastern University(东北大学) Brown University(布朗大学)

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

AI总结 提出声明式数据服务(DDS)架构,通过分层类型契约将全局搜索分解为有界子搜索,解决无界智能体发现无法稳定收敛的问题,并在交易后端工作负载上验证其有效性。

Comments Accepted at AI Agents for Discovery in the Wild (AID-Wild), Workshop at ACM CAIS 2026

详情

展开后加载摘要…

URL PDF HTML 收藏