AIxiv专栏是机器之心发布学术、技术内容的栏目。过去数年,机器之心AIxiv专栏接收报道了2000多篇内容,覆盖全球各大高校与企业的顶级实验室,有效促进了学术交流与传播。如果您有优秀的工作想要分享,欢迎投稿或者联系报道。投稿邮箱:liyazhou@jiqizhixin.com;zhaoyunfeng@jiqizhixin.com。
论文题目:MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data 论文链接:https://openreview.net/forum?id=8xliOUg9EW 代码链接:https://github.com/Eleanor-H/MUSTARD 数据集链接:https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view 作者主页:https://eleanor-h.github.io/
MUSTARDSAUCE-valid:经过了 Lean 形式化证明器验证的 5866 条数据; MUSTARDSAUCE-invalid:未能通过 Lean 形式化证明器验证的 5866 条数据; MUSTARDSAUCE-random:随机的 5866 条数据; MUSTARDSAUCE-tt:MUSTARD 生成的所有 28316 条数据。
赛道 1-1 (自动形式化):https://www.codabench.org/competitions/2436/ 赛道 1-2 (自动非形式化):https://www.codabench.org/competitions/2484/ 赛道 2 (自动定理生成和证明):https://www.codabench.org/competitions/2437/ 赛道 3 (代码辅助的运筹优化问题自动求解):https://www.codabench.org/competitions/2438/