大模型推理能力

Text2Model: Modeling Copilots for Text-to-Model Translation

Text2Model: 用于文本到模型翻译的建模副驾驶

Serdar Kadioglu, Karthik Uppuluri, Akash Singirikonda

机构 * AI Center of Excellence, Fidelity Investments（富达投资人工智能卓越中心） ； Department of Computer Science, Brown University（布朗大学计算机科学系） 纠错

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

AI总结 本文提出Text2Model和Text2Zinc，通过统一架构和数据集、求解器无关的方式，利用多种LLM策略实现文本到组合优化与满足问题的模型翻译，并开源副驾驶和排行榜以缩小性能差距。

Comments AAAI'25 Bridge Program on Machine Learning and Operations Research CPAIOR'26 Master Class on LLMs for CP/OR

MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

MathlibLemma: 形式化数学中的民间引理生成与基准测试

Xinyu Liu, Zixuan Xie, Amir Moeini, Claire Chen, Shuze Daniel Liu, Yu Meng, Aidong Zhang, Shangtong Zhang

机构 * Department of Computer Science, University of Virginia（弗吉尼亚大学计算机科学系） ； Astronomy , California Institute of Technology（加州理工学院天文学系） ； Purdue University（普渡大学） ； Massachusetts Institute of Technology（麻省理工学院） 纠错

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

AI总结 提出基于LLM的模块化流水线MathlibLemma，自动挖掘、形式化并证明数学中缺失的民间引理，生成包含4028个类型检查的Lean语句的基准测试集。

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

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 上超越现有开源基线。