![图片](https://image.jiqizhixin.com/uploads/editor/7f79bb0f-09f3-4d34-9db7-33d4fd01a6ac/640.png)
AIxiv专栏是机器之心发布学术、技术内容的栏目。过去数年,机器之心AIxiv专栏接收报道了2000多篇内容,覆盖全球各大高校与企业的顶级实验室,有效促进了学术交流与传播。如果您有优秀的工作想要分享,欢迎投稿或者联系报道。投稿邮箱:liyazhou@jiqizhixin.com;zhaoyunfeng@jiqizhixin.com。
![图片](https://image.jiqizhixin.com/uploads/editor/e7d65822-3b3c-4167-996e-96484eef065f/640.png)
论文题目: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/
![图片](https://image.jiqizhixin.com/uploads/editor/42ca5c0e-2048-4d9b-8cc0-3d25ecbc9b80/640.png)
![图片](https://image.jiqizhixin.com/uploads/editor/05c339f3-82cd-4a6a-87d0-18f8112c7381/640.png)
MUSTARDSAUCE-valid:经过了 Lean 形式化证明器验证的 5866 条数据; MUSTARDSAUCE-invalid:未能通过 Lean 形式化证明器验证的 5866 条数据; MUSTARDSAUCE-random:随机的 5866 条数据; MUSTARDSAUCE-tt:MUSTARD 生成的所有 28316 条数据。
![图片](https://image.jiqizhixin.com/uploads/editor/415ef69e-81dc-4bec-8aaa-3cdeca136470/640.png)
![图片](https://image.jiqizhixin.com/uploads/editor/96d8f3ff-1011-4d23-910a-4bef1066edff/640.png)
![图片](https://image.jiqizhixin.com/uploads/editor/427ebf0c-a6a5-4609-b0f9-725634b52597/640.png)
![图片](https://image.jiqizhixin.com/uploads/editor/0c24dc0b-f201-4a7f-bad8-2b695f094945/640.png)
赛道 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/