Lyra：在自动定理证明中编排双重修正
计算与语言
2024-08-27 v4 人工智能
摘要
大语言模型（LLMs）为形式化定理证明领域提供了一条引人探索的途径。然而，其全部潜力，尤其是关于幻觉缓解与通过证明器错误信息进行精炼的方面，仍是一个尚待深入研究的领域。为提升 LLMs 在该领域的有效性，我们引入了 Lyra，一种采用两种不同修正机制的新框架：工具修正（TC）与猜想修正（CC）。为在形式化证明的后处理中实施工具修正，我们利用先验知识调用预定义的证明器工具（如 Sledgehammer）以引导替换不正确的工具。工具修正显著有助于缓解幻觉，从而提高证明的整体准确性。此外，我们引入猜想修正，一种旨在与证明器交互并利用证明器错误信息精炼形式化证明猜想的错误反馈机制。相较于以往的精炼框架，所提出的猜想修正以指令精炼生成，而无需收集配对的（生成、错误与精炼）提示。我们的方法在 miniF2F 验证集（48.0% -> 55.3%）与测试集（45.5% -> 51.2%）上均取得了最先进（SOTA）性能。我们还展示了 3 道由 Lyra 解决的 IMO 题目。我们相信工具修正（用于幻觉缓解的后处理）与猜想修正（来自环境交互的子目标调整）可为该领域的未来研究提供一条有前景的途径。
引用
@article{arxiv.2309.15806,
title = {Lyra: Orchestrating Dual Correction in Automated Theorem Proving},
author = {Chuanyang Zheng and Haiming Wang and Enze Xie and Zhengying Liu and Jiankai Sun and Huajian Xin and Jianhao Shen and Zhenguo Li and Yu Li},
journal= {arXiv preprint arXiv:2309.15806},
year = {2024}
}
备注
Accepted to TMLR: https://openreview.net/forum?id=9Z0yB8rmQ2