Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

Ji Feng; Zhouxing Shi

Home/Archive/arXiv

arXiv · 2606.15972

Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

Ji Feng·Zhouxing Shi

View original source ↗Read source document ↗Export metadata ↓

Abstract

With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-checkable rigor, enabling use cases such as answer selection in test-time scaling with K sampled candidate answers. However, employing Lean requires that LLM outputs, originally in natural language, first be formalized. Existing Lean-based answer-selection work uses an autoformalization model to generate a formal statement in Lean for each candidate answer independently, incurring a significant computational cost. We propose BASE, a base-and-edit pipeline that formalizes a single base candidate per problem and derives the remaining K-1 statements by editing the answer expression in place. To facilitate this, we train a rewriter model LEANSCRIBE to localize the answer in the base formalization and generate a reusable edit function for the other K-1 candidates. BASE simultaneously improves selection accuracy and reduces formalization cost - a Pareto improvement that holds on all 12 (dataset, solver) configurations across four benchmarks and three solvers, cutting autoformalizer calls by about 5x at K=8, with the reduction expected to become larger as K grows. Code is available at https://github.com/ucr-rai/base-and-edit.

Explore related subjects

cs.CL cs.AI cs.LG

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Ji Feng, Zhouxing Shi. 2026-06-14. Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning. https://arxiv.org/abs/2606.15972

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Universal Topological Regularity of Syntactic Structures

Despite their widespread use, the principles governing the organisation of syntactic dependency trees remain poorly understood. I analyse dependency trees from 124 typologically, genetically, and geographically diverse languages. Their topology departs systematically from randomness. Relative to uniformly sampled random trees, dependency trees exhibit greater structural robustness and lower branching heterogeneity. I propose that these universal regularities emerge naturally from incremental grammatical encoding. I model this process using sublinear preferential attachment. The model accurately reproduces the observed topology. More generally, the results demonstrate how a universal statistical property of syntax can emerge from a simple, cognitively motivated generative process. They further illustrate a broader principle of efficiency by construction: communicatively efficient syntactic structures can emerge without direct optimisation for communication.

cs.CL↗

arXiv2026

An Incomplete Loop: Deductive, Inductive, and Abductive Reasoning in Language Models

Modern language models (LMs) can learn to perform new tasks in different ways: in instruction following, the target task is described explicitly in natural language; in few-shot prompting, the task is specified implicitly with a small number of examples; in instruction inference, LMs are presented with in-context examples and are then prompted to generate a natural language task description before making predictions. Each of these procedures may be thought of as invoking a different form of reasoning: instruction following involves deductive reasoning, few-shot prompting involves inductive reasoning, and instruction inference involves abductive reasoning. How do these different capabilities relate? Across four LMs (from the gpt and llama families) and two learning problems (involving arithmetic functions and machine translation) we find a strong dissociation between the different types of reasoning: LMs can sometimes learn effectively from few-shot prompts even when they are unable to explain their own prediction rules; conversely, they sometimes infer useful task descriptions while completely failing to learn from human-generated descriptions of the same task. Our results highlight the non-systematic nature of reasoning even in some of today's largest LMs, and underscore the fact that very different learning mechanisms may be invoked by seemingly similar prompting procedures.

cs.CL↗

arXiv2026

Thinking beyond the anthropomorphic paradigm benefits LLM research

Anthropomorphism, or the attribution of human traits to technology, is an automatic and unconscious response that occurs even in those with advanced technical expertise. In this position paper, we analyze hundreds of thousands of research articles to present empirical evidence of the prevalence and growth of anthropomorphic terminology in research on large language models (LLMs). We argue for challenging the deeper assumptions reflected in this terminology -- which, though often useful, may inadvertently constrain LLM development -- and broadening beyond them to open new pathways for understanding and improving LLMs. Specifically, we identify and examine five anthropomorphic assumptions that shape research across the LLM development lifecycle. For each assumption (e.g., that LLMs must use natural language for reasoning, or that they should be evaluated on benchmarks originally meant for humans), we demonstrate empirical, non-anthropomorphic alternatives that remain under-explored yet offer promising directions for LLM research and development.

cs.CL↗