High-Throughput Lean 4 Autoformalization Model for Local Inference

Lean4 Autoformalization Engine — mesh.applied Emailteam@meshapplied.comTagsmeshHigh-Throughput Lean 4 Autoformalization Model for Local Inference A memory-efficient, single-GPU training and inference architecture for formalizing natural language mathematics into Lean 4 statement code. Incorporates whole-model NF4 quantization of a sparse Mixture-of-Experts (MoE) model, custom parameter unfusing, Group Relative Policy Optimization (GRPO) with persistent Lean REPL compiler feedback, and a dual-tier retrieval augmentation mechanism. 1. Introduction 1.1 Autoformalization Bottleneck in Formal Mathematics Autoformalization, translating informal natural language mathematics into machine-checkable formal logic, is a primary bottleneck in formal verification. Modern interactive theorem provers, such as Lean 4, enforce rigid type-theoretic specifications. Minor syntax, namespace, or typeclass unification errors cause complete compilation failure. Manual translation is time-consuming, current autoformalization models are often expensive and error-prone. 1.2 Resource-Constrained Deployment State-of-the-art autoformalization models rely on dense multi-billion parameter LLMs requiring multi-GPU server clusters. Deploying fine-tuned models on consumer-grade single-GPU hardware presents severe memory limitations: 1. Dense models (>14B parameters in 16-bit precision) exceed VRAM limits during training and generation. 2. Standard 4-bit quantization libraries (such as bitsandbytes) fail on fused MoE weight tensors. 3. Execution of sparse MoE models on single cards suffers from launch-bound per-expert CUDA kernels. Evaluation of autoformalization methods is non-trivial, as correct compilation does not imply successful translation. This makes training environment construction difficult. The lack of proper training data and an accurate evaluation engine are critical issues in the field. This project aims to stretch the limits of a smaller transformer model at the domain of formal mathematics, test a set of fine tuning methods and assert their effectiveness, and eventually construct a multi-agent high-throughput system to rapidly iterate in problems. 2. System Architecture 2.1 Base Model Selection The base policy relies on Qwen3-Coder-30B-A3B, a sparse Mixture-of-Experts model containing 30B total parameters with ~3B active parameters per token across 48 transformer layers. Because Qwen-Coder is explicitly designed and pretrained for code generation and software synthesis, it has a better baseline comprehension of formal abstractions, strict type-theoretic semantics, and structured algorithmic logic required for interactive theorem proving compared to general-purpose language models. Furthermore, the sparse MoE architecture provides the expansive parameter capacity necessary to encode broad mathematical domain knowledge while constraining active forward-pass compute to ~3B parameters, this aids high throughput. 2.2 Memory Footprint & Quantization Engineering For training and inference, a standard Nvidia RTX 5090ti was used.In standard bfloat16 precision, the 30B model requires ~60 GB VRAM, exceeding the 32 GB budget of a single GPU. To fit both the base model and optimization states into VRAM: 1. Whole-Model NF4 Double-Quantization: The base model was loaded directly into host memory and quantized in-place using NormalFloat4 (NF4) with double quantization. 2. GPU Allocation: Model parameters reside entirely on GPU VRAM (~16.7 GB post-load, peak ~26–30 GB during training with micro-batch size 2). CPU offloading was completely disabled to avoid PCI-e latency bottlenecks. 2.3 MoE Expert Unfusing Engineering The standard implementation of Qwen3Moe stores expert weights in 3D fused tensors. Quantization libraries cannot process 3D fused parameters. To enable whole-model 4-bit quantization and expert-specific adapters, a custome layer is introduced: 1. Each layer’s fused expert block is decomposed into individual _Expert submodules containing standard nn.Linear layers (gate_proj, up_proj, down_proj). 2. Pretrained weights are copied from fused 3D tensors into the unfused nn.Linear modules. 3. Quantization is applied in-place via bitsandbytes.nn.Linear4bit. 4. The forward pass is modified to execute expert routing over explicit linear layers without modifying the base model output semantics. Pythonclass _Experts(nn.Module): def __init__(self, config): super().__init__() self.num_experts = config.num_experts self.act_fn = ACT2FN[config.hidden_act] for j in range(self.num_experts): self.add_module(str(j), _Expert(config.hidden_size, config.moe_intermediate_size))PEFT (Parameter-Efficient Fine-Tuning) automatically converts qwen3_moe expert target configurations into fused parameter names, missing custom unfused submodules. To bypass this, model.config.model_type is dynamically masked to "qwen3_moe_unfused" during PEFT injection, permitting explicit target module matching. 2.4 LoRA vs. DoRA Adapter modules are attached across attention and...

High-Throughput Lean 4 Autoformalization Model for Local Inference

Related Articles

Incident with Github.com

(no title)

Scientists reverse brain aging, with a nasal spray

NHS apologises and admits Palantir have access to identifiable patient data

Cursor Origin