arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.25018

Structure-Aware Equivalence for Evaluating Autoformalized Statements

Yi Yu·Yu-Hsuan Wu·Guang Lin·Yuhui Zhang·Yuxiang Peng
View original source ↗Read source document ↗Export metadata ↓

Abstract

Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but whole-statement logically equivalent pairs, while Mathesis LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either set as equivalent.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yi Yu, Yu-Hsuan Wu, Guang Lin, Yuhui Zhang, Yuxiang Peng. 2026-10-18. Structure-Aware Equivalence for Evaluating Autoformalized Statements. https://arxiv.org/abs/2610.25018

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

KEEP EXPLORING

Related papers

arXiv2026

Instrumentation Optimization for Practical Dynamic Race Detection

Dynamic data race detectors are successful at flagging concurrency bugs, but their high runtime overhead limits adoption. This overhead stems primarily from pervasive instrumentation of memory accesses -- a significant fraction of which is for safe accesses. We address this inefficiency through a compiler-integrated approach that identifies safe accesses using static analysis and eliminates instrumentation for these. We strike a careful balance between analysis precision and cost, to ensure applicability to real-world applications. We show that our optimizations never cause ThreadSanitizer to miss races it would otherwise detect. We further observe that many checks are redundant: They only flag a race if a preceding check has already flagged an equivalent race for the same memory location. We show that, when reporting one representative per class is sufficient, even more instrumentation can be eliminated. Lastly, we introduce a dynamic technique that skips instrumentation when there is only one thread at runtime, even when this could not be determined statically. We integrate these static analyses and program transformations into the ThreadSanitizer race detector based on LLVM. Our experiments on a diverse suite of real-world applications, including Memcached, Redis, SQLite, MySQL, and Chromium, demonstrate that our optimizations reduce the number of instrumentation calls at runtime by up to 91% and yield application-level speedups of up to 1.91x, a geometric-mean Chromium speedup of 1.25x on Blink and 1.14x on Speedometer 3.0, and peak speedups reaching 2.28x on Memcached with two server threads. Our optimizations are in the process of being upstreamed into ThreadSanitizer.

cs.PL↗
arXiv2026

A Taxonomy of Predicate Transformer Monads for Specifying Monadic Programs

Monads of weakest precondition predicate transformers are the foundation of several verification frameworks for monadic programs. For specifying monadic computations with nondeterminism and nontermination, in addition to weakest preconditions, we introduce the first strongest postcondition monads covering all combinations of angelic or demonic nondeterminism and partial or total interpretations of nontermination. For extending these base strongest postcondition monads with side effects such as mutable state, monad transformers do not yield the expected monads, so we instead generalize the base monads to arrows and use arrow transformers. We give a taxonomy of weakest precondition and strongest postcondition monads, for the base monads and for their versions with state, and show that the known relationships between under- and over-approximate triples based on predicate transformers already hold at the level of the predicate transformers themselves. We use the predicate transformer monads to define under- and over-approximate triples and, where possible, Dijkstra monads. Finally, we relate these two specification styles.

cs.PL↗
arXiv2026

Compiling Environment Classifiers to Contextual Modal Types

Type systems for metaprogramming take one of two approaches to safeguarding the scopes of variables in generated code. They either use Environment Classifiers (EC) to identify scopes by name (Taha and Nielsen, 2003), or they use Contextual Modal Type Theory (CMTT) to match scopes by structure (Nanevski, Pfenning, and Pientka, 2008). In this paper, we connect these two approaches by compiling a calculus with polymorphic environment classifiers, subtyping, and mutable references to a CMTT-based calculus with polymorphic contexts, mutable references, and first-class substitutions. The key idea is to map each environment classifier to a context. We prove that the compilation preserves types and that compilation preserves the behavior of metaprograms. Both proofs are mechanized in Agda. The compilation shows that CMTT is at least as expressive as environment classifiers. We conjecture that the converse compilation is difficult, because environment classifiers impose a stricter regime on the metaprogram.

cs.PL↗