用大模型自动翻译数学证明系统间的定理，准确率达98%。
MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
- 三源输入：自然语言+Lean+Isabelle，生成Rocq定理
- 478/488个定理成功翻译，准确率98%
- 适合形式化验证与跨系统研究者参考
本文利用前沿大模型，将MiniF2F中的定理自动翻译为Rocq格式。任务基于自然语言描述、Lean形式化和Isabelle形式化三源信息生成Rocq定理。实验分三个阶段逐步提升复杂度，从单次提示到多轮交互并融入失败反馈。采用GPT-4o mini、Claude 3.5 Sonnet、o1 mini和o1等先进模型进行多轮翻译。最终成功完成478个定理的转换，成功率高达98%。数据集已开源：https://github.com/LLM4Rocq/miniF2F-rocq。
原文摘要 · Abstract (English)
In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that incorporate feedback from unsuccessful attempts. At each stage, we perform multiple rounds of translation using increasingly advanced models: GPT-4o mini, Claude 3.5 Sonnet, o1 mini, and o1. We successfully translated 478 out of 488 theorems. The dataset is opensource: https://github.com/LLM4Rocq/miniF2F-rocq.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。