PaperlayerView exact revision on arXiv

Source-linked AI summary

Sage: Formalization with Semantic Correction

Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wenping Deng, Liang Zhang

arXiv:2609.35790v2cs.LGcs.AIcs.CLcs.LO

TL;DR

Formal theorem provers generally start from supplied formal statements, leaving faithful translation from informal mathematics as an upstream bottleneck. Sage combines staged generation with semantic and compiler feedback, reporting improved fidelity across benchmarks while reducing answer leakage.

  • Problem

    Theorem provers largely assume formal statements are already supplied, while translation from informal mathematics can compile despite dropping hypotheses or introducing vacuous claims.

    Source: §1 · p. 1

  • Method

    Sage uses four formalization stages and a dual-signal correction loop combining Lean diagnostics with multi-dimensional semantic feedback.

    Source: §1 · p. 2

  • Results

    Sage outperforms the fine-tuned baseline on OMNI-MATH without proofs (73.3% vs. 42.0% pass@4) and IMO-UNFORMALIZED (87.4% vs. 19.4% pass@4 verified fidelity), while reducing leakage from 70.9% to 2.7%.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The paper argues that autoformalizers should act as faithful translators rather than solution-guessing oracles, with answer-aware and answer-agnostic settings distinguished in advance.

    Source: §7 · p. 9

    Existential encodings of open queries into Prop remain vulnerable to proof-irrelevance shortcuts, including tautologies or classical case splits.

    Source: §7 · p. 9

Abstract

from arXiv · show

While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided. Translating informal natural language into a formal language is a critical data bottleneck plagued by an "illusion of rigor": standard type-checkers accept statements that compile but drop hypotheses, introduce vacuous truths, or subtly alter mathematical bounds. To resolve this, we introduce Sage (Semantic Agent-Guided Formalization Engine), an agentic framework that replaces monolithic translation with a four-stage decomposed generation pipeline coupled with a dual-signal semantic correction loop. By pairing Lean 4 compiler diagnostics with multi-dimensional semantic feedback, our correction loop enforces mathematical fidelity alongside syntactic validity. By explicitly accounting for the gap between open-ended queries and declarative formal targets, our pipeline prevents models from achieving high formalization rates by guessing unverified answers (exhibiting a 70.9% answer leakage rate in monolithic baselines). Consequently, Sage suppresses leakage to 2.7% while achieving 73.3% pass@4 joint compilation and semantic fidelity on the Omni-MATH without proofs (compared to 42.0% for a fine-tuned Goedel-Formalizer-V2 baseline). Finally, on IMO-Unformalized, a novel frontier of 175 unformalized International Mathematical Olympiad problems, Sage demonstrates effective zero-shot generalization with 87.4% pass@4 verified fidelity compared to just 19.4% for the baseline, winning over 79% of blind pairwise evaluations.

1 INTRODUCTION

Formalization must preserve the meaning of informal mathematics, because Lean can accept statements that compile while dropping hypotheses or becoming vacuous. Sage decomposes generation and combines compiler diagnostics with semantic feedback; it reports stronger fidelity and less answer leakage than the cited baselines.

Motivation

  • Lean compilation does not ensure semantic fidelity: a statement can drop a crucial condition or become a tautology or vacuous placeholder and still compile.The upstream translation from informal natural language to a formal statement remains necessary for high-quality formal training data.Source: §1 · p. 1

Approach

  • Sage replaces monolithic generation with four inspectable stages and an iterative correction loop pairing Lean diagnostics with multi-dimensional semantic feedback.It offers answer-aware and answer-agnostic configurations for settings with and without informal proofs.Source: §1 · p. 2

Empirical results

  • 73.3% vs. 42.0% pass@4, and 50.3% vs. 26.7% pass@1, for Sage and fine-tuned Goedel-Formalizer-V2 on OMNI-MATH without proofs.On IMO-UNFORMALIZED, Sage reaches 87.4% pass@4 verified fidelity vs. 19.4% for the baseline and wins over 79% of blind pairwise comparisons.Source: §1 · p. 2
  • Sage reduces unmonitored answer leakage on OMNI-MATH from 70.9% to 2.7%.The same evaluation reports the formalization comparisons on OMNI-MATH without proofs.Source: §1 · p. 2

2 RELATED WORK

Prior work has advanced theorem proving and autoformalization, but the upstream task of producing faithful formal targets remains distinct from proving them. Existing fidelity measures and refinement approaches have limitations that Sage addresses with an in-loop, reference-free semantic gate.

Neural Theorem Proving and the Statement Bottleneck

  • Theorem-proving systems assume formal targets are given, while Sage addresses the upstream task of synthesizing semantically faithful targets from natural language.The passage notes that human annotations can misinterpret problems and type-checker-guided pipelines can compromise constraints to compile.Source: §2 · p. 2

Autoformalization and Semantic Evaluation

  • Prior fidelity measures often require a human gold formalization, limiting their use on unformalized frontiers such as IMO-UNFORMALIZED.Sage-SM instead scores candidates directly against the natural-language source to drive test-time repair.Source: §2 · p. 3

Modular Decomposition and Iterative Refinement

  • Prior formal-mathematics systems use compiler-only repair, monolithic reflection, or dependency retrieval; Sage combines four-stage decomposition with an in-loop semantic gate.The paper says compiler-only repair prioritizes compilation and monolithic reflection succumbs to the Discovery Trap on open queries.Source: §2 · p. 3

3 FORMALIZING MATHEMATICS: BEYOND NAIVE TRANSLATION

Open-ended mathematical questions pose a discovery task, whereas theorem provers require declarative targets for verification. The resulting trade-off constrains answer-agnostic formalization, and the paper discusses alternative encodings and Type-Theoretic Locks.

Statement types and the discovery gap

  • Assertion-type statements present a claim to verify; question-type statements ask for an unknown object, value, witness, or characterization.The paper calls the resulting mismatch between open-ended discovery and formal verification the Discovery vs. Verification Gap.Source: §3 · p. 3

The Feasibility Trilemma

  • Explicit answer injection yields resolved theorems but needs an oracle; placeholders preserve open texture but require prover code changes; existentials preserve intent but can be fragile.Existential encodings are especially vulnerable for polar queries and characterization queries, where computational bypass is possible.Source: §3 · pp. 3–4
  • An answer-agnostic formalizer cannot encode an open query as one declarative proposition without an oracle, reduced prover usability, or logical vulnerability.The paper names these competing constraints the Feasibility Trilemma.Source: §3 · pp. 3–4

Operating configurations and locks

  • Sage uses existential encodings in answer-agnostic mode and proof-guided answer injection in answer-aware mode; Type-Theoretic Locks are used where feasible to encourage witness synthesis.When a locked formulation is not feasible, the pipeline defaults to a standard existential.Source: §3 · p. 4

4 THE SAGE FRAMEWORK: COMPOSITION & SEMANTIC CORRECTION

Sage drafts formal statements through specialized agents, audits them for semantic and code quality, then iteratively corrects syntax and meaning together. Its verification gate goes beyond compilation to check alignment with the informal source.

4 THE SAGE FRAMEWORK: COMPOSITION & SEMANTIC CORRECTION

  • Sage separates drafting, multi-dimensional verification, and dual-signal refinement into sequential phases.The generation maps an informal statement, with an optional proof, to a formal statement.Source: §4 · p. 4, §4.1 · p. 4

4.1 COMPOSITIONAL GENERATION (THE DRAFT PHASE)

  • The draft phase distills goals, preprocesses hypotheses and conclusions, formalizes them in Lean, then assembles a standalone file without changing semantics.The formatter organizes imports, namespaces, and noncomputable sections; the compiler enforces a single terminating sorry at the primary declaration.Source: §4.1 · pp. 4–5

4.2 MULTI-DIMENSIONAL ALIGNMENT CRITERIA

  • The semantic rater checks component omissions, incorrect mappings, and spurious additions, then assesses holistic equivalence, exactness, and code quality.Code-quality criteria include idiomatic Lean and Mathlib reuse, generality, and descriptive precision.Source: §4.2 · p. 5

4.3 SEMANTIC CORRECTION LOOP

  • Sage refines drafts for up to T rounds and exits only when compilation and Sage-SM both pass, giving the corrector compiler diagnostics and semantic critique.The paired feedback is intended to resolve type errors without changing mathematical intent or injecting unverified answers.Source: §4.3 · p. 6

5 EXPERIMENTAL SETUP

The evaluation spans established and previously unformalized mathematics, using controlled method variants and metrics that assess both Lean validity and semantic fidelity.

5 EXPERIMENTAL SETUP

  • 175 unformalized IMO problems test zero-shot generalization, alongside 223 already-formalized IMO problems and 300 OMNI-MATH problems.OMNI-MATH is evaluated in both answer-aware and answer-agnostic regimes.Source: §5 · p. 6
  • A controlled 2 × 3 ablation crosses monolithic and decomposed architectures with no feedback, compiler-only feedback, or dual-signal feedback.Iterative variants use matched round budgets; Sage denotes Decomposed+Dual.Source: §5 · p. 6

5.1 EVALUATION METRICS

  • The evaluation treats compilation, semantic fidelity, and source-text texture as distinct dimensions because compilation alone misses semantic failures.The listed metrics include an in-loop Sage-SM gate and a post-hoc Goedel-SM judge.Source: §5.1 · p. 6
  • Evaluation tracks compilation, multiple-sorry drafts, answer leakage, semantic match, pairwise preference, and joint compilation plus semantic consensus.Joint Success requires both Lean compilation and unanimous post-hoc semantic consensus.Source: §5.1 · p. 6

6 RESULTS AND ANALYSIS

The results assess semantic fidelity, proofless formalization, and answer leakage. Sage achieves high verified fidelity on unformalized IMO problems and sharply reduces answer leakage on proofless OMNI-MATH.

6 RESULTS AND ANALYSIS

  • The semantic gate agrees 71.1% with three Lean annotators and reaches 85.7% and 88.8% accuracy on ConsistencyCheck and ProofNetVerif.The annotator audit used 45 drafts; the gold-label benchmarks used 859 and 3,752 examples, respectively.Source: §6 · p. 7

6.1 PROVER-READY FORMALIZATION: ANSWER-AWARE TRANSLATION

  • 77.3% joint fidelity under the external Goedel-SM judge and 93.7% under the in-loop Sage-SM gate follow addition of semantic feedback.Compiler feedback alone raises compilation above 95% and joint fidelity to about 75%, but does not catch dropped hypotheses or altered bounds.Source: §6.1 · p. 7, Table 2 · p. 7
  • With proofs available, monolithic and decomposed loops attain comparable fidelity: 76.3% versus 77.3%.The passage attributes reduced target-constant ambiguity to the informal proofs and says decomposition primarily provides structural auditability in this regime.Source: §6.1 · p. 7
  • Scaling the base model raises verified joint fidelity from 30.3% to 85.7% while reducing average repair rounds from 3.2 to 1.1.The scaling results are reported for Sage on answer-aware OMNI-MATH.Source: §6.1 · p. 7, Table 3 · p. 7

6.2 AUTONOMOUS ZERO-SHOT FORMALIZATION ACROSS THE IMO LANDSCAPE

  • 87.4% pass@4 verified fidelity on IMO-UNFORMALIZED compares with 19.4% for the baseline; blind evaluations prefer Sage in 79.4% of head-to-head comparisons.At pass@1, Sage scores 60.0% on IMO-UNFORMALIZED versus 10.3% for the fine-tuned Goedel baseline.Source: §6.2 · p. 8, Table 4 · p. 8

6.3 THE DISCOVERY TRAP: UNMASKING ANSWER-AGNOSTIC QUESTION BENCHMARKS

  • Because 98.7% of OMNI-MATH problems are interrogative, answer-agnostic evaluation tests how models translate open questions without an answer oracle.The authors report Goedel-SM rather than their internal gate, whose reject audit penalizes legitimate existential translations.Source: §6.3 · p. 8
  • 70.9% answer leakage in monolithic theorem signatures falls to 2.7% with Sage, which uses placeholder encodings in only 1.1% of cases.The passage reports 80.6% of rejected monolithic drafts as mathematically false and 76.8% of Sage rejections as evaluator penalties against existential translations.Source: §6.3 · pp. 8–9, Table 5 · p. 8, Table 6 · p. 9
  • 76.8% of Sage rejections reflect external evaluators penalizing existential translations, making reported joint fidelity an adversarial lower bound.The framework formalizes open queries as existential propositions; the authors characterize monolithic leads as an artifact of rewarding hallucinated constants.Source: §6.3 · p. 9

7 DISCUSSION AND LIMITATIONS

Sage treats autoformalization as faithful translation, not answer solving, and limits answer leakage by representing unanswered queries without guessed constants. Its semantic safeguards carry a latency cost and do not eliminate type-theoretic vulnerabilities in existential encodings.

The Autoformalizer as Translator, Not Solver

  • Sage enforces the translator-not-solver boundary by formalizing unanswered queries without guessed constants, reducing answer leakage to 2.7%.When informal proofs are supplied, systems can instead construct closed, instantiated theorems.Source: §7 · p. 9

Statement Vulnerability in Type Theory

  • Existential encodings of open queries remain vulnerable to downstream proof bypasses through tautologies or classical case splits.The authors propose computational subtypes in Type as a research direction for requiring explicit witnesses.Source: §7 · p. 9

Inference Latency and Adaptive Compute

  • 3.2 to ∼1.1 average repair rounds as the base model changes from Qwen3-32B to Qwen3.8-27B, with joint fidelity reaching 85.7%.Sequential multi-agent verification adds latency, but the authors identify offline synthetic-corpus curation as a setting where certification outweighs real-time throughput.Source: §7 · p. 9

8 CONCLUSION

Formal proof systems assume statements are already formalized, while natural-language statements can be accepted by compilers despite semantic errors. Sage combines type-checking with semantic critique and reports high joint fidelity across answer-aware, answer-agnostic, and unformalized IMO settings.

8 CONCLUSION

  • Proof-search systems assume formal targets are given, leaving translation from natural language as an upstream bottleneck.Compile acceptance alone can conceal dropped hypotheses, altered constraints, or false conjectures.Source: §8 · p. 9
  • Sage couples syntactic type-checking with multi-dimensional semantic critique to assess mathematical fidelity.The paper frames this as a response to compilers accepting statements that drop hypotheses, alter constraints, or inject false conjectures.Source: §8 · p. 9
  • 77.3% joint fidelity on OMNI-MATH answer-aware, 73.3% answer-agnostic pass@4, and 60.0% zero-shot on unformalized IMO problems.The conclusion reports nearly 6× improvement over fine-tuned baselines and 2.7% structural answer leakage.Source: §8 · p. 10
  • The authors present Sage as an engine for generating faithful synthetic data at scale to support future automated reasoning systems.They characterize inference-time semantic verification as indispensable for high-integrity formalization.Source: §8 · p. 10

AI USE STATEMENT

The supplied material covers AI-use disclosures and theoretical foundations concerning the mismatch between open-ended discovery queries and formal verification. It states that intensional target containers can let provers trivialize discovery queries without performing mathematical discovery.

AI USE STATEMENT

  • The authors used generative AI for manuscript polishing and coding assistance, but not for formulating hypotheses, theoretical claims, or mathematical definitions.They state that AI-assisted text and scripts were reviewed by the authors.Source: AI USE STATEMENT · p. 10

A THEORETICAL FOUNDATIONS, THE FEASIBILITY TRILEMMA, AND TYPE-THEORETIC LOCKS

  • The theoretical section frames translation challenges as a structural mismatch between natural-language mathematical practice and dependent type theory.It addresses the Feasibility Trilemma, syntactic exploits available to downstream provers, and Type-Theoretic Locks in Lean 4.Source: A THEORETICAL FOUNDATIONS, THE… · p. 12

A.1 THE DISCOVERY VS. VERIFICATION GAP AND THE LAW OF SYNTACTIC TRIVIALIZATION

  • Discovery queries ask for unknown mathematical entities, unlike verification tasks that begin with a fixed, closed proposition.The supplied examples include value determination, witness construction, full characterization, and extremal optimization.Source: §A.1 · p. 12
  • The Law of Syntactic Trivialization says a prover can trivially solve an open-ended discovery query when its target container admits an intensional definition.Packaging the defining predicate as a witness can yield a verified proof without computing or discovering mathematical content.Source: §A.1 · pp. 12–13

A.2 THE FEASIBILITY TRILEMMA

This section addresses the feasibility challenges of formalizing open-ended queries, describing Type-Theoretic Locks and Sage’s decomposed generation and repair protocols. It also explains Sage’s joint compilation-and-semantic gate, its answer-aware and answer-agnostic modes, and the scope of the experimental setup details.

A.2 THE FEASIBILITY TRILEMMA

  • An answer-agnostic formalizer faces a trilemma: answer injection needs an oracle, placeholder definitions violate prover immutability, and existential encodings invite logical shortcuts.Answer injection also changes discovery into verification; a hallucinated answer can make the theorem false. Placeholder definitions require code modification, while existential targets are vulnerable to polarity commitments and triviality.Source: §A.2 · p. 13

A.3 VULNERABILITIES OF EXISTENTIAL TARGETS: POLARITY AND TRIVIALITY

  • Naive existential targets enable polarity cheats via excluded middle and trivial characterization proofs via Lean’s definitional identity between Set α and predicates.A prover can prove a set characterization by choosing {x | P x} and using reflexivity, without computing solutions or performing mathematical deductions.Source: §A.3 · p. 14

A.4 THE DEFENSE MATRIX: TYPE-THEORETIC LOCKS

  • Type-Theoretic Locks move targets from Prop into Type, requiring explicit computational witnesses and preventing both excluded-middle polarity proofs and set-builder characterization shortcuts.For finite solution sets, restricting the container to List or Finset forces construction of a computational collection rather than an intensional predicate.Source: §A.4 · pp. 14–15

A.5 CLEANED AND HOMOGENIZED LEAN 4 LOCK IMPLEMENTATIONS

  • Standardized lock templates instantiate characterization queries with extensional list subtypes and binary decisions with constructive sum targets, requiring explicit witnesses or answers.For finite characterization queries such as x^2 − 4 = 0, the locked target requires concrete roots; the constructive sum blocks excluded-middle-only answers.Source: §A.5 · p. 15, §A.5.1 · p. 15, §A.5.2 · p. 15

A.5.3 STANDARDIZED MULTIPLE-CHOICE QUESTION (MCQ) PATTERNS

  • MCQ lock patterns require single-select solvers to prove the selected option and multi-select solvers to return exactly the true options.The section presents standardized Type-Lock patterns for single-select, multi-select, and other common MCQ formats.Source: §A.5.3 · p. 16

B.1 DECOMPOSITION PROTOCOL AND AGENT CONTRACTS

  • Sage decomposes generation into four role-isolated agents—Distiller, Preprocessor, Formalizer, and Formatter—to separate query interpretation, structure extraction, Lean formalization, and syntactic integration.The Distiller distinguishes answer-aware from answer-agnostic regimes; the Preprocessor builds SDNF and extracts goals, infrastructure, and hypotheses; the Formalizer creates typed signatures; the Formatter normalizes code without changing semantics.Source: §B.1 · pp. 17–18

B.2 CORRECTION LOOP PROTOCOL

  • Multi-round correction uses a shared contract that forbids solving the mathematics, while limiting compiler feedback to the first five errors and tracking failed attempts to reduce oscillation.The Corrector must emit a complete Lean file ending the main claim at := by sorry or preserving proof_wanted; it prioritizes the first compiler error and receives prior rejected statements with failure reasons.Source: §B.2 · p. 18

B.3 SYNTAX-ONLY REPAIR LOOP

  • Syntax-only repair exits when a candidate compiles or the round budget ends, so it can return a compiling but mathematically unfaithful statement.The syntax Corrector receives the informal statement, current Lean draft, and verifier report, but success is gated solely by type-checking.Source: §B.3 · p. 19

B.4 DUAL-SIGNAL SEMANTIC CORRECTION LOOP

  • Sage accepts a candidate only when it satisfies both Lean compilation and semantic fidelity, using compiler diagnostics and Rater critiques to guide correction.The Corrector is instructed to prioritize semantic match, and Sage pre-compiles the Rater’s proposed draft so it can account for both its semantics and verified compilation status.Source: §B.4 · p. 19
  • In answer-agnostic formalization, the Corrector must reject injected answers or undefined placeholders and preserve the open-ended existential goal.The Anti-Solver Rule forbids solving the problem or inserting concrete witnesses to silence type errors.Source: §B.4 · p. 19

B.5 COMPOSITIONAL GENERATION WALKTHROUGH

  • The OMNI-MATH #043 walkthrough contrasts answer-aware formalization of n = 6 with answer-agnostic formalization as the unique-existence goal ∃! n, 4n = 642.With PNL, the Distiller extracts n = 6 and the Preprocessor binds a hypothesis; without an answer oracle, the existential goal delegates computation to downstream provers.Source: §B.5 · pp. 19–20, Figure 3 · p. 20

C EXPERIMENTAL SETUP, DATASETS, AND REPRODUCIBILITY

C.1 DATASET DETAILS AND CURATION

The evaluation spans existing and unformalized olympiad problems, using controlled method variants and separate checks for compilation, semantic fidelity, and answer leakage. Its audit also finds that the post-hoc judge favors explicit answers over open formulations.

C.1 DATASET DETAILS AND CURATION

  • The 300-problem OMNI-MATH subset matches Goedel-Prover-V2’s benchmark and is 98.7% question-type, with no Geometry-tagged problems.Its subject tags are Algebra (62.7%), Number Theory (29.0%), Combinatorics (6.3%), and Precalculus (2.0%).Source: §C.1 · pp. 20–21
  • IMO-FORMALIZED contains 223 community-formalized problems, while IMO-UNFORMALIZED contains the complementary 175 historical problems without Lean 4 formalizations.The former is nearly balanced between question- and assertion-type problems; the latter is 69.1% Geometry, reflecting the unformalized frontier’s subject skew.Source: §C.1 · p. 21

C.2 LLM SERVING, MODELS, AND INFRASTRUCTURE

  • Qwen3.6-27B powers generation and in-loop rating, while Gemma4-31B independently evaluates semantic fidelity and pairwise preferences.Qwen3.8-27B was released too late for a full comparative rerun, and its longer reasoning traces increased per-step latency.Source: §C.2 · pp. 21–22

C.3 METHOD VARIANTS AND ABLATION CONFIGURATIONS

  • Six configurations isolate decomposition and feedback effects on a shared Qwen3.6-27B backbone, with matched iterative repair budgets across methods.The study also compares against Goedel-Formalizer-V2 as a specialized fine-tuned baseline.Source: §C.3 · p. 22

C.4 EVALUATION METRICS AND INTEGRITY AUDITS

  • The audits distinguish answer leakage from faithful open encodings and disqualify candidates that use multiple sorry placeholders to evade a self-contained target.For answer-agnostic question-type problems, a concrete embedded witness is flagged as leakage even if it does not match the ground-truth answer.Source: §C.4 · pp. 23–24
  • The primary criterion requires both Lean 4 compilation and unanimous post-hoc semantic approval; pass@N counts a problem when any of N candidates meets the criterion.Goedel-SM uses four independent judge calls, while Sage-SM applies a conjunctive gate over seven dimensions during repair.Source: §C.4 · pp. 24–25

C.5 GOEDEL EVALUATION PROTOCOL AND PROMPT BIAS ANALYSIS

  • The Goedel-SM prompt examples favor closed witnesses over open encodings, and Sage’s most frequent rejection category is Existential (76.8%).Monolithic generators and Goedel are instead dominated by Mathematically False and Wrong Injection rejections; Sage does not route pure mathematical-falsity rejections through correction.Source: §C.5 · pp. 25–26

D.1 GENERATOR BACKBONE ABLATION: SCALING ACROSS MODEL GENERATIONS

On OMNI-MATH, stronger generator backbones correspond to substantially higher compilation and joint fidelity in Sage. A separate adversarial audit compares Sage-SM with expert judgments.

D.1 GENERATOR BACKBONE ABLATION: SCALING ACROSS MODEL GENERATIONS

  • 85.7% joint fidelity and 98.0% compilation are reported for Qwen3.8-27B, compared with 30.3% joint fidelity and 57.3% compilation for Qwen3-32B.The complete Sage pipeline was evaluated at pass@1 on OMNI-MATH in the Answer-Aware setting; joint solved counts are out of 300 problems.Source: Table 12 · p. 26, §D.1 · p. 26
  • 90.2% witness injection for Qwen3.6-27B and 89.5% for Qwen3.8-27B reach the reported extraction ceiling, so their performance difference is attributed to fidelity, syntax resolution, and premise alignment.Qwen3-32B reaches 22.0% witness injection.Source: §D.1 · p. 26

E HUMAN EXPERT VALIDATION OF THE SEMANTIC GATE

  • 71.1% of 45 adversarially sampled formalizations received the same binary judgment from Sage-SM and majority human vote; human Semantic Match correlated with rater scores at Pearson r = 0.64 and Spearman ρ = 0.63.The audit was stratified to include silent semantic failures, compile-failed faithful drafts, clean translations, and catastrophic failures.Source: E HUMAN EXPERT VALIDATION OF THE… · pp. 26–27

F EXTERNAL EVALUATION OF THE SEMANTIC GATE

The Sage-SM gate is tested zero-shot against gold faithfulness labels on two public benchmarks. The section also presents blind pairwise preferences on the unformalized IMO frontier.

F EXTERNAL EVALUATION OF THE SEMANTIC GATE

  • ConsistencyCheck contains 859 informal–formal pairs, and ProofNetVerif contains 3,752; each provides gold binary faithfulness labels for evaluating the gate.The reported metrics include accuracy, Pass-class precision, recall and F1, and Matthews correlation.Source: F EXTERNAL EVALUATION OF THE SEMANTIC… · p. 27
  • 85.7% accuracy on ConsistencyCheck and 88.8% on ProofNetVerif exceed their majority baselines by about 19 percentage points; Matthews correlations are 0.67 and 0.74, respectively.The published Pass/Fail gate is applied without retuning its decision rule on either benchmark.Source: Table 13 · p. 27, F EXTERNAL EVALUATION OF THE SEMANTIC… · p. 27

G BLIND PAIRWISE PREFERENCES ON IMO-UNFORMALIZED

Related papers

Loading 2609.35790v2…