Natural Language to First-Order Logic LLM-based Autoformalization

Andrea Brunello; Cristian Curaba; Luca Geatti; Michele Mignani; Angelo Montanari; Nicola Saccomanno

Natural Language to First-Order Logic LLM-based Autoformalization

Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

Correct Metadata for

Use this form to create a GitHub issue with structured data describing the correction. You will need a GitHub account. Once you create that issue, the correction will be reviewed by a staff member.

⚠️ Mobile Users: Submitting this form to create a new issue will only work with github.com, not the GitHub Mobile app.

Important: The Anthology treat PDFs as authoritative. Please use this form only to correct data that is out of line with the PDF. See our corrections guidelines if you need to change the PDF.

Title Adjust the title. Retain tags such as <fixed-case>.

Authors Adjust author names and order to match the PDF.

Abstract Correct abstract if needed. Retain XML formatting tags such as <tex-math>. You may use ... for bold, ... for italic, ... for underline, <sc>...</sc> for small-caps, <tt>...<tt> for typewriter text, <url>...</url> for URLs, <a href=...> for hyperlinks, and <par/> for paragraph breaks.

Verification against PDF Ensure that the new title/authors match the snapshot below. (If there is no snapshot or it is too small, consult the PDF.)

Authors concatenated from the text boxes above:

ALL author names match the snapshot above—including middle initials, hyphens, and accents.

Abstract

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.

Anthology ID:: 2026.emnlp-main.568
Volume:: Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing
Month:: October
Year:: 2026
Address:: Budapest, Hungary
Editors:: Hung-Yi Lee, Sunipa Dev, Jessy Li, Desmond Elliott
Venue:: EMNLP
SIG:: SIGDAT
Publisher:: Association for Computational Linguistics
Note:
Pages:: 13036–13050
Language:
URL:: https://aclanthology.org/2026.emnlp-main.568/
DOI:
Bibkey:
Cite (ACL):: Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, and Nicola Saccomanno. 2026. Natural Language to First-Order Logic LLM-based Autoformalization. In Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing, pages 13036–13050, Budapest, Hungary. Association for Computational Linguistics.
Cite (Informal):: Natural Language to First-Order Logic LLM-based Autoformalization (Brunello et al., EMNLP 2026)
Copy Citation:
PDF:: https://aclanthology.org/2026.emnlp-main.568.pdf

PDF Cite Search Fix data

Export citation

BibTeX
MODS XML
Endnote
Preformatted

@inproceedings{brunello-etal-2026-natural,
    title = "Natural Language to First-Order Logic {LLM}-based Autoformalization",
    author = "Brunello, Andrea  and
      Curaba, Cristian  and
      Geatti, Luca  and
      Mignani, Michele  and
      Montanari, Angelo  and
      Saccomanno, Nicola",
    editor = "Lee, Hung-Yi  and
      Dev, Sunipa  and
      Li, Jessy  and
      Elliott, Desmond",
    booktitle = "Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing",
    month = oct,
    year = "2026",
    address = "Budapest, Hungary",
    publisher = "Association for Computational Linguistics",
    url = "https://aclanthology.org/2026.emnlp-main.568/",
    pages = "13036--13050",
    ISBN = "979-8-89176-459-0",
    abstract = "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."
}

Download as File

<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="brunello-etal-2026-natural">
    <titleInfo>
        <title>Natural Language to First-Order Logic LLM-based Autoformalization</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Andrea</namePart>
        <namePart type="family">Brunello</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Cristian</namePart>
        <namePart type="family">Curaba</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Luca</namePart>
        <namePart type="family">Geatti</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Michele</namePart>
        <namePart type="family">Mignani</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Angelo</namePart>
        <namePart type="family">Montanari</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Nicola</namePart>
        <namePart type="family">Saccomanno</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2026-10</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Hung-Yi</namePart>
            <namePart type="family">Lee</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Sunipa</namePart>
            <namePart type="family">Dev</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jessy</namePart>
            <namePart type="family">Li</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Desmond</namePart>
            <namePart type="family">Elliott</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Budapest, Hungary</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-459-0</identifier>
    </relatedItem>
    <abstract>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.</abstract>
    <identifier type="citekey">brunello-etal-2026-natural</identifier>
    <location>
        <url>https://aclanthology.org/2026.emnlp-main.568/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>13036</start>
            <end>13050</end>
        </extent>
    </part>
</mods>
</modsCollection>

Download as File

%0 Conference Proceedings
%T Natural Language to First-Order Logic LLM-based Autoformalization
%A Brunello, Andrea
%A Curaba, Cristian
%A Geatti, Luca
%A Mignani, Michele
%A Montanari, Angelo
%A Saccomanno, Nicola
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-459-0
%F brunello-etal-2026-natural
%X 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.
%U https://aclanthology.org/2026.emnlp-main.568/
%P 13036-13050

Download as File

Markdown (Informal)

[Natural Language to First-Order Logic LLM-based Autoformalization](https://aclanthology.org/2026.emnlp-main.568/) (Brunello et al., EMNLP 2026)

Natural Language to First-Order Logic LLM-based Autoformalization (Brunello et al., EMNLP 2026)

ACL

Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, and Nicola Saccomanno. 2026. Natural Language to First-Order Logic LLM-based Autoformalization. In Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing, pages 13036–13050, Budapest, Hungary. Association for Computational Linguistics.