SAPSE-Synergy: Balancing Formal Soundness and Empirical Coverage in Neural Theorem Proving

Abstract Large language models (LLMs) can propose candidate lemmas, yet translating natural-language reasoning into verified Coq artifacts remains difficult due to semantic drift, missing abstractions, and weak type discipline. Most existing systems treat the prover as a black-box filter: as long as some candidates verify, little is known about which transformations are semantically safe, or how much coverage must be sacrificed to obtain formal guarantees. We present Semantic Alignment for Proof Strategy Extraction (SAPSE), a retrieval-first framework that links natural-language proof steps with formal lemmas through dual-domain embeddings and type-aware abstraction. At its core, SAPSE introduces an abstract syntax tree (AST) sanitizer whose verified fragment, mechanized in Rocq 9.1.0 for a minimal calculus, consists of two concretely implemented transformations, require injection and equality canonicalization, together with a parametric binder-normalization schema that is currently instantiated as the identity on terms. For all admissible inputs in this calculus, these verified passes are proved to preserve both typing and logical equivalence under import-only context extension. A production sanitizer extends this core with unverified but practical passes: scope resolution, list parameterization, and formatting for complete Coq syntax, while reusing the same verified interface. On top of this verified core, we develop an adaptive Synergy pipeline that first applies unverified heuristic repairs to maximize empirical coverage and then invokes the verified core under admissibility guards to enforce soundness. Rather than optimizing raw verification accuracy, Synergy exposes a reproducible safety-coverage frontier: on a 2,000-lemma real Coq benchmark, a retrieval-only baseline verifies 37.6% of generated candidates, while the Synergy configuration verifies 32.8% with zero unsafe rewrites among guarded repairs and comparable runtime. Fragment-coverage analysis shows that 98.1% of benchmark lemmas lie in the mechanized fragment and that every Synergy success falls inside this fragment, so the AST-level soundness theorem applies directly. A differential analysis of the 96 lemmas that the retrieval-only baseline verifies but Synergy fails on decomposes these “lost successes” by semantic category, structural complexity, and failure mode, turning the observed performance gap into a diagnostic tool for future verified transformations. Overall, SAPSE-Synergy provides a partially mechanized but practically effective bridge between probabilistic lemma generation and formally verified transformation. It quantifies, for the first time, how much empirical coverage must be traded for a small, compositional verified core that safely mediates heuristic repairs in neural theorem proving. (Source code and full experimental artifacts are publicly available at: https://github.com/leochenminrui/SAPSE-Synergy )