<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="li-etal-2026-fiver">
    <titleInfo>
        <title>FIVER: Adaptive Fusion of Formal and Informal Verification for Mathematical Reasoning in LLMs</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Yujie</namePart>
        <namePart type="family">Li</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Ao</namePart>
        <namePart type="family">Xu</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Ziyou</namePart>
        <namePart type="family">Guo</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Tieru</namePart>
        <namePart type="family">Wu</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>Findings of the Association for Computational Linguistics: EMNLP 2026</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-462-0</identifier>
    </relatedItem>
    <abstract>Step-level verification is central to improving the reliability of multi-step mathematical reasoning in large language models (LLMs), yet existing methods typically adopt a fixed strategy between formal and informal proof. Formal methods can produce interpretable and machine-checkable proof objects. However, they are computationally expensive and limited by the success rates of formalization, semantic alignment, and proof search. Informal methods based on LLM judges offer lower cost and broader coverage, but their judgments cannot by themselves provide rigorous checkable proofs. Thus, a mathematical verification agent should adaptively choose the proof form for each step, covering the union of both capabilities while preferring cheaper informal verification in their overlap. Based on this formulation, we propose FIVER (Formal–Informal Verification Agent with Efficient Routing), a step-level mathematical verification agent that adaptively fuses formal and informal verification. FIVER uses a learnable router modeled with item response theory (IRT) to select either a formal or informal workflow, forming a new step-verification architecture. Under the Qwen3-8B setting, FIVER improves over the purely formal HERMES baseline by 10.77% on MATH-398 and 33.33% on AIME 2025, respectively, while using only 58.8% of HERMES’s verification tokens on average.</abstract>
    <identifier type="citekey">li-etal-2026-fiver</identifier>
    <identifier type="doi">10.18653/2026.findings-emnlp.702</identifier>
    <location>
        <url>https://aclanthology.org/2026.findings-emnlp.702/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>14730</start>
            <end>14750</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T FIVER: Adaptive Fusion of Formal and Informal Verification for Mathematical Reasoning in LLMs
%A Li, Yujie
%A Xu, Ao
%A Guo, Ziyou
%A Wu, Tieru
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F li-etal-2026-fiver
%X Step-level verification is central to improving the reliability of multi-step mathematical reasoning in large language models (LLMs), yet existing methods typically adopt a fixed strategy between formal and informal proof. Formal methods can produce interpretable and machine-checkable proof objects. However, they are computationally expensive and limited by the success rates of formalization, semantic alignment, and proof search. Informal methods based on LLM judges offer lower cost and broader coverage, but their judgments cannot by themselves provide rigorous checkable proofs. Thus, a mathematical verification agent should adaptively choose the proof form for each step, covering the union of both capabilities while preferring cheaper informal verification in their overlap. Based on this formulation, we propose FIVER (Formal–Informal Verification Agent with Efficient Routing), a step-level mathematical verification agent that adaptively fuses formal and informal verification. FIVER uses a learnable router modeled with item response theory (IRT) to select either a formal or informal workflow, forming a new step-verification architecture. Under the Qwen3-8B setting, FIVER improves over the purely formal HERMES baseline by 10.77% on MATH-398 and 33.33% on AIME 2025, respectively, while using only 58.8% of HERMES’s verification tokens on average.
%R 10.18653/2026.findings-emnlp.702
%U https://aclanthology.org/2026.findings-emnlp.702/
%U https://doi.org/10.18653/2026.findings-emnlp.702
%P 14730-14750

Markdown (Informal)

[FIVER: Adaptive Fusion of Formal and Informal Verification for Mathematical Reasoning in LLMs](https://aclanthology.org/2026.findings-emnlp.702/) (Li et al., Findings 2026)

• FIVER: Adaptive Fusion of Formal and Informal Verification for Mathematical Reasoning in LLMs (Li et al., Findings 2026)

ACL

• Yujie Li, Ao Xu, Ziyou Guo, and Tieru Wu. 2026. FIVER: Adaptive Fusion of Formal and Informal Verification for Mathematical Reasoning in LLMs. In Findings of the Association for Computational Linguistics: EMNLP 2026, pages 14730–14750, Budapest, Hungary. Association for Computational Linguistics.