@inproceedings{hossain-etal-2026-sage,
title = "{SAGE}: Satisfiability Guided Decoding for Mathematical Reasoning",
author = "Hossain, Tamanna and
Singh, Sameer and
Ahmed, Kareem",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {EMNLP} 2026",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.findings-emnlp.2313/",
doi = "10.18653/2026.findings-emnlp.2313",
pages = "49649--49665",
ISBN = "979-8-89176-462-0",
abstract = "Chain-of-thought prompting improves mathematical reasoning, but generated reasoning chains can appear locally plausible while being globally inconsistent. Later steps may derive equations inconsistent with claims asserted earlier. We propose SAGE, a training-free decoding approach that treats symbolic consistency as probabilistic conditioning over mathematical claims, conditioning each new claim on the symbolic state accumulated from earlier steps. SAGE approximates this conditional distribution online by resampling at mathematical span boundaries: candidate continuations are parsed into formal claims and selected according to satisfiability with the accumulated symbolic state. This statement-level decoding avoids intractable token-level constrained decoding while still using solver feedback online, before a complete solution has been generated. Across MATH-500, Gaokao, and Minerva, SAGE improves LLaMA, DeepSeek, and Qwen models over temperature sampling. On MATH-500, it improves accuracy by up to 6.3{\%} and by 3.1{\%} on average across four models. On Gaokao and Minerva datasets, SAGE yields consistent gains across models, improving Gaokao and Minerva pass@3 by up to 2{\%} and 3{\%}, respectively. We release our code at https://github.com/tamannahossainkay/sage"
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="hossain-etal-2026-sage">
<titleInfo>
<title>SAGE: Satisfiability Guided Decoding for Mathematical Reasoning</title>
</titleInfo>
<name type="personal">
<namePart type="given">Tamanna</namePart>
<namePart type="family">Hossain</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sameer</namePart>
<namePart type="family">Singh</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Kareem</namePart>
<namePart type="family">Ahmed</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>Chain-of-thought prompting improves mathematical reasoning, but generated reasoning chains can appear locally plausible while being globally inconsistent. Later steps may derive equations inconsistent with claims asserted earlier. We propose SAGE, a training-free decoding approach that treats symbolic consistency as probabilistic conditioning over mathematical claims, conditioning each new claim on the symbolic state accumulated from earlier steps. SAGE approximates this conditional distribution online by resampling at mathematical span boundaries: candidate continuations are parsed into formal claims and selected according to satisfiability with the accumulated symbolic state. This statement-level decoding avoids intractable token-level constrained decoding while still using solver feedback online, before a complete solution has been generated. Across MATH-500, Gaokao, and Minerva, SAGE improves LLaMA, DeepSeek, and Qwen models over temperature sampling. On MATH-500, it improves accuracy by up to 6.3% and by 3.1% on average across four models. On Gaokao and Minerva datasets, SAGE yields consistent gains across models, improving Gaokao and Minerva pass@3 by up to 2% and 3%, respectively. We release our code at https://github.com/tamannahossainkay/sage</abstract>
<identifier type="citekey">hossain-etal-2026-sage</identifier>
<identifier type="doi">10.18653/2026.findings-emnlp.2313</identifier>
<location>
<url>https://aclanthology.org/2026.findings-emnlp.2313/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>49649</start>
<end>49665</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T SAGE: Satisfiability Guided Decoding for Mathematical Reasoning
%A Hossain, Tamanna
%A Singh, Sameer
%A Ahmed, Kareem
%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 hossain-etal-2026-sage
%X Chain-of-thought prompting improves mathematical reasoning, but generated reasoning chains can appear locally plausible while being globally inconsistent. Later steps may derive equations inconsistent with claims asserted earlier. We propose SAGE, a training-free decoding approach that treats symbolic consistency as probabilistic conditioning over mathematical claims, conditioning each new claim on the symbolic state accumulated from earlier steps. SAGE approximates this conditional distribution online by resampling at mathematical span boundaries: candidate continuations are parsed into formal claims and selected according to satisfiability with the accumulated symbolic state. This statement-level decoding avoids intractable token-level constrained decoding while still using solver feedback online, before a complete solution has been generated. Across MATH-500, Gaokao, and Minerva, SAGE improves LLaMA, DeepSeek, and Qwen models over temperature sampling. On MATH-500, it improves accuracy by up to 6.3% and by 3.1% on average across four models. On Gaokao and Minerva datasets, SAGE yields consistent gains across models, improving Gaokao and Minerva pass@3 by up to 2% and 3%, respectively. We release our code at https://github.com/tamannahossainkay/sage
%R 10.18653/2026.findings-emnlp.2313
%U https://aclanthology.org/2026.findings-emnlp.2313/
%U https://doi.org/10.18653/2026.findings-emnlp.2313
%P 49649-49665
Markdown (Informal)
[SAGE: Satisfiability Guided Decoding for Mathematical Reasoning](https://aclanthology.org/2026.findings-emnlp.2313/) (Hossain et al., Findings 2026)
ACL