基于大语言模型的自然语言到一阶逻辑的自动形式化
Natural Language to First-Order Logic LLM-based Autoformalization
浏览论文内容
中文总结 AI 辅助
本文针对以一阶逻辑为目标形式体系的自动形式化领域缺乏统一任务定义与系统综述的问题，区分本体提取与逻辑翻译，综述相关数据集、指标及基于LLM的方法，并指出该领域的开放挑战。
中文摘要 AI 辅助
大语言模型（LLMs）重新激发了对自动形式化的兴趣。然而，当以一阶逻辑（FOL）作为目标形式体系时，该领域仍缺乏统一的任务定义和系统综述。本文填补了这一空白：我们首先通过区分本体提取与逻辑翻译，为FOL自动形式化任务提供了原则性定义，表明二者的混淆会模糊跨研究评估；我们综述了现有数据集、评估指标及基于LLM的方法，包括微调、提示和基于验证的优化；我们确定了基准测试、语义评估、本体感知方法和端到端应用方面的开放挑战。
英文摘要
Large Language Models (LLMs) have renewed interest in autoformalization. Yet, when First-Order Logic (FOL) is considered as the target formalism, the field still lacks a unified task formulation and a systematic survey. This paper addresses this gap: we first provide a principled definition for the FOL-autoformalization task by distinguishing Ontology Extraction from Logical Translation, showing how their conflation obscures (cross-study) evaluation; we review existing datasets, evaluation metrics, and LLM-based methods, including fine-tuning, prompting, and verification-based refinement; we identify open challenges in benchmarking, semantic evaluation, ontology-aware methods, and end-to-end applications.
发表机构
- University of Udine（乌迪内大学）
机构由 AI 辅助整理，请以论文原文为准。
