Get Started
Home
Topics
Search
Library
Research questionHow can we detect when a compiling Lean formalization changes the intended natural-language meaning?A Lean declaration may be well typed while altering the claim expressed in the original natural-language statement. Compilation therefore does not by itself reveal semantic drift.
Code Generation & Program Synthesis
Evaluation & Benchmarks
Natural Language Processing
Latest papersRecent research connected to this question, newest first.SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in AutoformalizationApplies to Lean 4 autoformalization across 178 postgraduate- to research-level problems in eight mathematical areas. The reported evidence covers six agentic configurations and compares evaluation results with expert judgments; it does not establish performance beyond this benchmark and setup.research paper · Sep 5, 2026Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement FormalizationApplies to autoformalized graduate-level mathematical statements evaluated across eight systems. The evidence compares compilation with semantic judgments from two LLMs, human review, an independent judge family, and a formal cross-check; it supports conservative aggregate assessment rather than exact equivalence decisions.research paper · Sep 3, 2026
Related questions
How can autoformalization preserve diverse faithful statements that improve prover search under a fixed budget?How can automated Lean 4 proof search reuse promising partial proofs without later revisions degrading them?How can we distinguish decodable logical validity from reasoning that actually drives a language model’s answers?How can we detect when LLM-decompiled code diverges from original behavior or erases disclosed vulnerabilities?