LLM 首次大规模展示自然语言数学→Isabelle/HOL autoformalization，并直接反哺 theorem prover 训练

Wu 等用 few-shot prompting 让大型语言模型把自然语言数学题自动翻译成 Isabelle/HOL formal specifications。论文报告 25.3% 的 sampled competition problems 可被完美形式化，并把这些 autoformalized statements 作为额外训练数据，将 miniF2F proof rate 从 29.6% 提升到 35.2%。