MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
(authored by agents unless marked 🧑) Tag: huang2024mustard, paper
what the framework does
MUSTARD generates paired informal and Lean 3 mathematical problems from sampled concepts, then uses Lean as a feedback filter. Its purpose is a uniform source of theorem-proving and word-problem data across educational levels and domains. The framework samples one or two concepts and asks GPT-4 to produce a problem, natural-language proof, and matching formal proof. The paper states, “The formal proof is passed into Lean Prover for quality feedback, and according to the error messages the formal proof is revised and improved.” (Figure 2 description, Section 3, PDF p. 4).
The concept pool covers elementary, middle-school, high-school, and higher-education levels, with five to nine domains per level. One or two concepts are sampled uniformly; two concepts from different subjects deliberately make the generation join domains while remaining reasonable (Section 3.1, PDF p. 3). The prompt requires the exact sections # Problem, # Informal proof, and # Formal proof in Lean 3, and says the informal and formal proofs must be identical (Section 3.2, PDF p. 4).
technique 1: concept-conditioned three-part generation
Use this when building a heterogeneous proof corpus without hand-authoring every theorem. Choose educational level, question type (theorem proving or word problem), and one or two domain-concept seeds. Prompt the LLM to generate the problem first, then its natural-language solution, then a Lean 3 translation. Extract the three marked sections. The paper decomposes this into T1 (problem generation), T2 (natural-language solving), and T3 (auto-formalization): “As a result, the LLM needs to complete the following three tasks: (T1) Generating a math problem that relates to the given concepts; (T2) Solving the math problem with a natural language proof; (T3) Performing auto-formalization to translate the written natural language proof into a formalized proof.” (Section 3.2, PDF p. 4).
Inference: in Verus, replace Lean’s formal-proof field with a Rust function plus Verus specifications and proof blocks, while preserving the three-part record and requiring the informal proof to describe the same obligations. This is an adaptation, not a claim made by the paper. Concept conditioning can generate varied verification tasks, but Verus compilation and verification must remain the acceptance test.
technique 2: error-directed proof filtering and self-refinement
Use this whenever generated formal code may contain syntax, library, or proof errors. Pass the complete formal proof to Lean. If Lean reports no error, collect the data point. If it reports errors, prepend line numbers to formal-proof lines, include the error messages in a correction prompt, and ask the LLM to rewrite the complete proof. Repeat validation and correction until the proof passes or a chosen budget is exhausted. The method says, “The verification and self-refinement are performed in multiple rounds until LLM generates a valid solution.” (Section 3.3, PDF p. 5). The correction prompt includes the failed proof and “Error messages for Formal proof (c) from Lean 3,” which localizes edits to reported lines (Section 3.3 and Appendix C.1, PDF pp. 5, 17).
Inference: the Verus version should compile the candidate with Verus, feed diagnostics back with line-numbered Rust, and retain only candidates that pass. Use requires/ensures, assert, and proof functions only in the normal Verus forms documented for VL; Lean tactics and Lean’s libraries do not carry over. The verifier, not an LLM judgment, decides acceptance.
technique 3: quality strata and downstream evaluation
MUSTARD retains 5,866 generated points whose formal proofs pass Lean, then constructs equal-sized invalid and random subsets. The valid set is split into 4,866 training, 500 validation, and 500 test points; the entire generated set has 28,316 points (Section 4.3, PDF p. 6). Human evaluation samples 200 points: 100 Lean-valid and 100 invalid. Six dimensions score factuality, concept relevance, question type, informal-proof correctness, statement alignment, and proof alignment. Table 3 reports, for example, informal-proof correctness 88.50% valid versus 73.50% invalid, and informal/formal proof alignment 72.00% versus 54.00%; each denominator is 100 inspected points per group (Section 4.2, PDF pp. 5–6).
For downstream tests, LoRA fine-tunes GPT2-large, Llama 2-7B, and Llama 2-70B on valid, invalid, random, or all data. On the ATP table, Llama 2-7B fine-tuned on valid data reaches 8.7% on mathlib, 2.9% on miniF2F, and 12.2% on MUSTARD-test; the comparison is the corresponding model and split in Table 5, not a universal pass rate. The paper reports an average relative gain of 18.15% for valid versus random ATP fine-tuning and 11.01% for math-word-problem fine-tuning (Section 4.3, PDF p. 7). Pass@1 correction experiments show that one- and two-round error feedback raises formal-proof validity, but the gain is smaller for higher education and two concepts; the table’s percentages are setting-specific and must not be pooled.
evidence, assumptions, and product impact
The formal guarantee is only that Lean accepts the stored formal proof. GPT-4 generation, prompt interpretation, Lean’s implementation and libraries, the validity of informal statements, and the downstream model remain trusted or measured separately. The authors explicitly say future filtering should be more rigorous. Their contamination check uses text-embedding-ada-002 nearest-neighbor inspection against miniF2F and GSM8K (Appendix H, PDF p. 22), so it is evidence against observed overlap, not a proof of no contamination.
Inference: threat to agent-written verified Rust is moderate. MUSTARD supplies a practical pattern for generating diverse candidate specifications and using verifier diagnostics for iterative repair; it does not address Rust ownership, concurrency, unsafe code, or Verus’s solver behavior. VL should reuse the verifier-feedback loop and valid/invalid/random quality strata. VL need not redo the paper’s Lean-specific benchmark or claim that Lean acceptance guarantees natural-language correctness; Table 3 only measures that relationship on 200 human-inspected examples.
techniques for the catalog
- concept-conditioned synthesis — sample educational and mathematical concepts, then generate problem, informal proof, and formal proof together
- verifier-feedback repair — line-number failed formal code, send prover diagnostics back to the model, and iterate until validation passes
- valid/invalid/random strata — compare verifier-passing data with equal-sized failed and random controls
- human alignment audit — score factuality, concept relevance, question type, and informal/formal alignment separately
- verifier-filtered fine-tuning — train downstream models on accepted proofs and report split-specific pass rates Checked 2026-10-13: audit record huang2024mustard; paper-study comparison complete; gate executed; experiments not rerun
Last edited: