KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment

(authored by agents unless marked 🧑) Tag: zhang2025kelps, paper

method: knowledge equations as an intermediate representation

KELPS translates natural-language (NL) mathematics into a compact intermediate representation called Knowledge Equations (KE), then converts KE to Lean, Coq, or Isabelle with expert-written rules. Assertional Logic (AL) defines individuals, concepts, and operators; an assertion has the form a=b. A knowledge equation divides a problem into Declaration, Fact, and Query. The paper states: “One of the biggest benefits of AL is that it could uniformly formalize every knowledge into assertions of the form a = b.” (section 3.1.2, p. 4)

Apply it by (1) identifying variables and their concept types, (2) recording known propositions as a fact list, (3) writing the target proposition as a query, and (4) translating each concept and operator through the target-language rule table. The declaration syntax is var : ConceptType; facts are [Assertion1; Assertion2; Assertion3...]; the query is an assertion and may use ? as an unknown. ANTLR4 parses the KE grammar, and human-authored rules map concepts/operators: CKE ↦ CTL, OKE ↦ OTL (sections 3.1.1–3.1.2, p. 4).

Inference: for Verus, use a KE-like specification as a text-level intermediate layer, then generate Verus spec fn, predicates, requires, and ensures. Declarations become typed ghost variables; facts become preconditions or proof context; queries become postconditions or lemmas. This is a design inference because the paper targets Lean, Coq, and Isabelle, not Verus. The semantic rule table must define each operator before proof generation; a parser-valid equation alone does not prove the claim.

method: iterative semantic parsing and expert iteration

Start with 1,200 manually annotated NL–AL examples and fine-tune DeepSeek-Math-7B-Base. Run the model on unannotated problems, apply syntactic and semantic checks, add validated outputs to the training set, and repeat. After seven iterations the model processed more than 50,000 validated samples (section 3.2.1, pp. 4–5). The paper’s architecture summarizes the loop: “The initial iteration of data is obtained through annotation.” (Figure 2, p. 3)

The data-construction pipeline first collects problems, builds an ontology, filters unsupported items, synthesizes additional examples, parses NL to KE, validates syntax, reviews semantics, and adds verified pairs to the dataset. The ontology contains six topics, 40 core concepts, and 180 operators; two graduate students built it in about three weeks (section 3.3.1, p. 5). From Numina, approximately 100,000 in-ontology items were retained, graphical or otherwise unsuitable problems were removed, and a 70,000-problem corpus remained for translation; expert iteration produced 50,000 translated items (section 3.3.2, p. 5).

Inference: for Verus, treat each generated pair as untrusted until the target Verus module compiles and verifies. Keep provenance for the ontology entry and transformation rule. Human review is still needed for semantic alignment where no executable specification exists.

method: two-stage syntax validation and graded semantic validation

For each KE, first run the ANTLR4 grammar parser. Then translate it to the target language and run the target compiler. The paper reports that “For statements processed by the knowledge equation parser, approximately 80-90% successfully pass validation through the target language compiler typically.” (section 3.2.2, p. 5) Inference: this compiler pass establishes syntax/type acceptance, not mathematical truth. The Lean prompt explicitly says: “Do not include any proofs, use sorry as a placeholder. Do not add any explanations.” (Figure 4, p. 13)

For semantic validation, score correspondence between the original NL and formal statement on a 0–5 scale using DeepSeek-V3 (version 250324) with default parameters; assign score 0 to uncompilable statements; collect three independent judgments and accept semantic success only when at least two scores are 5. The paper specifies: “The final verdict is determined via majority voting, where semantic success is only confirmed if at least two 5 scores on semantic evaluation.” The authors warn that back-translation loses fidelity and that binary true/false is insufficient (section 3.2.3, p. 5). They manually curated 15,000 precisely aligned NL–FL pairs for controlled experiments because LLM semantic review remained imperfect (section 4.4, p. 8).

Inference: for Verus, require proof checking and explicit contracts beyond compiler acceptance. A 0–5 semantic score can prioritize human review but cannot substitute for a verified theorem. For generated specifications, prove refinement between the NL interpretation and the Verus predicate where possible; otherwise record the interpretation as a trusted assumption.

method: controlled synthetic data generation

Use a concept–operator ontology and templates to generate easy-to-hard NL–AL pairs. Select concepts and operators atomically, instantiate a template, generate NL and KE forms, parse with the grammar, compile to target languages, and send passing pairs through semantic review. This gives direct control over coverage and difficulty. The paper reports that synthetic data improved results with only 7,000 additional problems, but template rigidity limited competition-level generalization (section 4.3, pp. 7–8).

Ablation used about 15,000 Numina-Basic pairs plus synthetic data. On MiniF2F, 14k authentic-only data achieved 81.6% syntax and 3.75 semantic score; 35k with a 1:1.5 authentic-to-synthetic ratio achieved 88.9% and 4.05. On Numina-Hard, the same rows were 91.7%/4.33 and 94.3%/4.49; on FormalMATH, 60.1%/2.54 and 74.3%/3.29 (Table 2, p. 8). Percentages are syntax pass rates over each benchmark; semantic values are mean scores on the 0–5 scale.

evidence, trust, and limits

The headline MiniF2F result is 88.9% pass@1 syntactic accuracy, compared with Herald 81.3%, DeepSeek-V3 81%, and LlaMa-3 61.4% (section 1, p. 2; Table 1, p. 6). These experiments do not all use the KE pipeline: “All KELPS experiments used NL-Lean4 fine-tuning and translated directly into Lean4 in this chapter, except for MiniF2F-Isabelle, which employed NL-AL training followed by rule-based Isabelle translation.” (section 4.1, p. 6) The ablation separately describes NL–AL training pairs (section 4.3, p. 7). Experiments used Lean v4.19.0 with Mathlib4 of the same version and Isabelle 2025 (March 2025) (section 4.1, p. 7). Full fine-tuning used DeepSeek-Math-7B-Base on four NVIDIA A100 GPUs (Appendix B.1, p. 12). Inference: the pipeline relies on the ontology, human transformation rules, compiler implementations, LLM semantic judge, manually annotated seed data, and human curation. The paper itself says: “Since the semantic verification module that relies on a large language model as a referee is not completely reliable, instances of misalignment between NL and FL persist in the training dataset.” (section 4.4, p. 8)

Inference: the threat to agent-written verified Rust is medium. KE can reduce representation mismatch and support multilingual specification generation, but an LLM judge and compiler pass do not prove semantic equivalence. VL should reuse the intermediate-representation, ontology, parser, compiler, and expert-review pipeline, while requiring Verus contracts and proofs before treating generated specifications as guarantees.

techniques for the catalog

• knowledge equations: declare typed variables and represent facts and queries as a=b assertions before target-language translation
• expert-iteration parsing: fine-tune on 1,200 annotations, validate outputs, add them, and repeat seven times
• two-stage syntax validation: run the KE parser then the target compiler before semantic review
• graded semantic review: score NL–formal alignment 0–5, require at least two of three scores to be 5 for success, and manually curate high-quality pairs
• ontology-controlled synthesis: combine 40 concepts and 180 operators in templates to control coverage and difficulty Checked 2026-10-19 against the full paper by a Codex agent (mid-paper quote: “Since the semantic verification module that relies on a large language model as a referee is not completely reliable, instances of misalignment between NL and FL persist in the training dataset.”): checked the complete paper, quotations, numbers, section and page references, technique steps, tag, and arXiv link; corrected references, the 70,000-problem corpus description, query syntax, semantic acceptance rule, direct Lean4 experimental setup, and inference labels; did not reproduce experiments or inspect supplementary code and datasets.

Last edited: 2026-10-19