@inproceedings{sultan-etal-2026-reliable,
title = "Reliable Proof Generation with {LLM}s via Analogical Retrieval and Symbolic Verification: A Case Study in {E}uclidean Geometry",
author = "Sultan, Oren and
Stern, Eitan and
Shahaf, Dafna",
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.501/",
pages = "10488--10506",
ISBN = "979-8-89176-462-0",
abstract = "Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning, such as mathematical proof generation. We propose a neuro-symbolic approach centered on the hypothesis that structurally analogous problems often admit similar proofs. As a proof-of-concept, we focus on SAT-level geometry problems. Our approach is two-fold: (1) We retrieve analogous problems and use their proofs to guide the LLM, and (2) a formal verifier evaluates the generated proofs and provides feedback, helping the model fix incorrect proofs.\par Our complete pipeline substantially improves proof accuracy across model families, achieving 68{\%}-96{\%} accuracy compared with 10{\%}-44{\%} for LLM-only baselines that use neither analogy retrieval nor verifier feedback. When comparing against models with the same verifier feedback and inference budget, analogical guidance improves accuracy from 88{\%} to 96{\%} for GPT-5, 78{\%} to 86{\%} for Claude Sonnet 4.6, 72{\%} to 86{\%} for Gemini-Flash-2.5, and 52{\%} to 80{\%} for OpenAI o1. More broadly, shifting to LLMs that generate provably correct conclusions has the potential to dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="sultan-etal-2026-reliable">
<titleInfo>
<title>Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry</title>
</titleInfo>
<name type="personal">
<namePart type="given">Oren</namePart>
<namePart type="family">Sultan</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Eitan</namePart>
<namePart type="family">Stern</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Dafna</namePart>
<namePart type="family">Shahaf</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>Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning, such as mathematical proof generation. We propose a neuro-symbolic approach centered on the hypothesis that structurally analogous problems often admit similar proofs. As a proof-of-concept, we focus on SAT-level geometry problems. Our approach is two-fold: (1) We retrieve analogous problems and use their proofs to guide the LLM, and (2) a formal verifier evaluates the generated proofs and provides feedback, helping the model fix incorrect proofs.\par Our complete pipeline substantially improves proof accuracy across model families, achieving 68%-96% accuracy compared with 10%-44% for LLM-only baselines that use neither analogy retrieval nor verifier feedback. When comparing against models with the same verifier feedback and inference budget, analogical guidance improves accuracy from 88% to 96% for GPT-5, 78% to 86% for Claude Sonnet 4.6, 72% to 86% for Gemini-Flash-2.5, and 52% to 80% for OpenAI o1. More broadly, shifting to LLMs that generate provably correct conclusions has the potential to dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness.</abstract>
<identifier type="citekey">sultan-etal-2026-reliable</identifier>
<location>
<url>https://aclanthology.org/2026.findings-emnlp.501/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>10488</start>
<end>10506</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry
%A Sultan, Oren
%A Stern, Eitan
%A Shahaf, Dafna
%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 sultan-etal-2026-reliable
%X Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning, such as mathematical proof generation. We propose a neuro-symbolic approach centered on the hypothesis that structurally analogous problems often admit similar proofs. As a proof-of-concept, we focus on SAT-level geometry problems. Our approach is two-fold: (1) We retrieve analogous problems and use their proofs to guide the LLM, and (2) a formal verifier evaluates the generated proofs and provides feedback, helping the model fix incorrect proofs.\par Our complete pipeline substantially improves proof accuracy across model families, achieving 68%-96% accuracy compared with 10%-44% for LLM-only baselines that use neither analogy retrieval nor verifier feedback. When comparing against models with the same verifier feedback and inference budget, analogical guidance improves accuracy from 88% to 96% for GPT-5, 78% to 86% for Claude Sonnet 4.6, 72% to 86% for Gemini-Flash-2.5, and 52% to 80% for OpenAI o1. More broadly, shifting to LLMs that generate provably correct conclusions has the potential to dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness.
%U https://aclanthology.org/2026.findings-emnlp.501/
%P 10488-10506
Markdown (Informal)
[Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry](https://aclanthology.org/2026.findings-emnlp.501/) (Sultan et al., Findings 2026)
ACL