Switch Space trainer defaults to math_conjecture_sota profile and remove DeepSeek references

README.md

@@ -11,7 +11,7 @@ emoji: 🧮
 
 # Math Conjecture Command Center
 
-An autonomous training app for DeepSeek-Math that runs multi-stage curriculum fine-tuning on Space GPU, executes post-training quality evaluation, and publishes only qualified adapters, checkpoints, and run reports to your Hugging Face model repository.
+An autonomous training app for Lean-aware and math-reasoning base models that runs multi-stage curriculum fine-tuning on Space GPU, executes post-training quality evaluation, and publishes only qualified adapters, checkpoints, and run reports to your Hugging Face model repository.
 
 The UI now uses a dark graphite command-center aesthetic with tactical green/cyan telemetry accents, higher-contrast cards, and mobile-friendly stacking while preserving the existing training controls.
 
@@ -23,7 +23,7 @@ This Space is the training app for `maths-conjuncture-solutions` and is wired to
 ## End-to-end flow
 
 1. Download released parquet splits (`train/validation/test`).
-2. Build runtime config from `configs/deepseek_math_sota.yaml`.
+2. Build runtime config from `configs/math_conjecture_sota.yaml` (default answered-conjecture solver profile).
 3. Run 4-stage curriculum LoRA fine-tuning with `scripts/train_sota.py`.
 4. Run post-train evaluation (`pass@1`, `pass@k`, exact/boxed, family metrics).
 5. Apply quality gate thresholds before hub push.
@@ -48,7 +48,7 @@ Credentials and publish permissions are handled by deployment runtime settings.
 
 ## Artifacts
 
-- runtime config: `workspace/runtime/deepseek_math_sota.runtime.yaml`
+- runtime config: `workspace/runtime/math_conjecture_sota.runtime.yaml`
 - run output root: `workspace/runs/math-conjecture-sota`
 - final adapter: `workspace/runs/math-conjecture-sota/final_adapter`
 - training summary: `workspace/runs/math-conjecture-sota/training_summary.json`
@@ -59,6 +59,8 @@ Credentials and publish permissions are handled by deployment runtime settings.
 ## Notes
 
 - Full training runs on GPU when available and automatically falls back to CPU mode when CUDA is unavailable.
+- Default SOTA profile uses `Qwen/Qwen2.5-Math-7B-Instruct` for answered-conjecture solving and Lean/formal-proof alignment.
+- Alternate SOTA profile `configs/qwen25_math_sota.yaml` targets `Qwen/Qwen2.5-Math-7B-Instruct`.
 - App handles Gradio copy-button compatibility across versions automatically.
 - The interface is optimized to stay legible on mobile, with telemetry cards collapsing into a single-column stack.
 

VALIDATION_LOG.md

@@ -11,7 +11,7 @@ Reviewed the full `space_trainer/` implementation surface used by the Hugging Fa
 - `space_trainer/PRODUCTION.md`
 - `space_trainer/.env.example`
 - `space_trainer/requirements.txt`
-- `space_trainer/configs/deepseek_math_sota.yaml`
+- `space_trainer/configs/math_conjecture_sota.yaml`
 - `space_trainer/scripts/preflight_check.py`
 - `space_trainer/scripts/train_sota.py`
 - `space_trainer/scripts/eval_sota.py`

app.py

@@ -36,7 +36,7 @@ HF_HOME_DIR = WORKSPACE_DIR / ".hf_home"
 HF_DATASETS_CACHE_DIR = HF_HOME_DIR / "datasets"
 HF_HUB_CACHE_DIR = HF_HOME_DIR / "hub"
 
-CONFIG_TEMPLATE = ROOT / "configs" / "deepseek_math_sota.yaml"
+CONFIG_TEMPLATE = ROOT / "configs" / "math_conjecture_sota.yaml"
 TRAIN_SCRIPT = ROOT / "scripts" / "train_sota.py"
 EVAL_SCRIPT = ROOT / "scripts" / "eval_sota.py"
 TRAIN_OUTPUT_DIR = WORKSPACE_DIR / "runs" / "math-conjecture-sota"
@@ -126,8 +126,8 @@ DEFAULT_AUTO_PUSH_TO_HUB = bool(TEMPLATE_HUB.get("push_to_hub", True))
 DEFAULT_MODEL_ARCH_FALLBACK = (os.environ.get("MODEL_ARCH_FALLBACK_BASE_MODEL") or "Qwen/Qwen2.5-0.5B-Instruct").strip()
 MODEL_ARCH_ERROR_MARKERS = (
     "does not recognize this architecture",
-    "KeyError: 'deepseek_v32'",
-    "model type `deepseek_v32`",
+    "KeyError: 'unsupported_model_architecture'",
+    "unsupported model architecture type",
 )
 
 
@@ -137,7 +137,7 @@ PROJECT_DESCRIPTION = """
 This app runs the full training pipeline for the `maths-conjuncture-solutions` stack:
 
 1. Pull parquet splits from `NorthernTribe-Research/math-conjecture-training-corpus`.
-2. Build runtime config from `configs/deepseek_math_sota.yaml`.
+2. Build runtime config from `configs/math_conjecture_sota.yaml`.
 3. Execute staged LoRA curriculum via `scripts/train_sota.py`.
 4. Run post-training evaluation and read quality gate outcomes.
 5. Push artifacts only when policy/gates allow.
@@ -165,17 +165,12 @@ APP_HEADER_HTML = """
         <span>Hub Publish</span>
       </div>
     </div>
-    <aside class="mono-hero-panel">
-      <div class="mono-hero-panel-label">Mission Posture</div>
-      <div class="mono-hero-panel-value">Defense-tech telemetry</div>
-      <div class="mono-hero-panel-copy">Dark graphite shell, tactical green/cyan accents, high-contrast run state cards, and mobile-first operator controls.</div>
-    </aside>
   </div>
 </section>
 """
 
 APP_FOOTER_HTML = """
-<footer class="mono-footer">Graphite command center shell • NorthernTribe Research © 2026</footer>
+<footer class="mono-footer">NorthernTribe Research © 2026</footer>
 """
 
 UI_CSS = r"""
@@ -1681,7 +1676,7 @@ def write_runtime_config(
     cfg["quality_gate"]["min_pass_at_k"] = float(gate_min_pass_at_k)
     cfg["quality_gate"]["require_post_eval"] = bool(enforce_quality_gate and run_eval)
 
-    runtime_path = RUNTIME_DIR / "deepseek_math_sota.runtime.yaml"
+    runtime_path = RUNTIME_DIR / "math_conjecture_sota.runtime.yaml"
     runtime_path.write_text(yaml.safe_dump(cfg, sort_keys=False), encoding="utf-8")
     return runtime_path
 
@@ -2420,7 +2415,7 @@ with gr.Blocks(title="Math Conjecture Command Center") as demo:
         )
         base_model_id = gr.Textbox(
             label="Base Model ID",
-            value="deepseek-ai/deepseek-math-v2",
+            value="Qwen/Qwen2.5-Math-7B-Instruct",
         )
 
     with gr.Row():

configs/math_conjecture_sota.yaml

@@ -0,0 +1,151 @@
+global:
+  output_root: workspace/runs/math-conjecture-sota
+  seed: 17
+
+model:
+  base_model: Qwen/Qwen2.5-Math-7B-Instruct
+  trust_remote_code: false
+  use_bf16: true
+  load_in_4bit: true
+  bnb_4bit_quant_type: nf4
+  bnb_4bit_use_double_quant: true
+  attn_implementation: null
+  lora:
+    r: 96
+    alpha: 192
+    dropout: 0.05
+    bias: none
+    target_modules:
+      - q_proj
+      - k_proj
+      - v_proj
+      - o_proj
+      - gate_proj
+      - up_proj
+      - down_proj
+
+data:
+  default_train_file: workspace/data/releases/v1/train.parquet
+  default_validation_file: workspace/data/releases/v1/validation.parquet
+  prompt_field: prompt
+  target_field: target
+  final_answer_field: final_answer
+  proof_field: proof_formal
+  sample_weight_field: sample_weight
+  max_seq_length: 4096
+  min_loss_weight: 0.25
+  max_loss_weight: 6.0
+  family_boost:
+    conjecture_core: 3.0
+    formal_proof: 2.7
+    competition: 1.2
+    structured_reasoning: 1.1
+  system_prompt: |
+    You are NorthernTribe Research's math-conjecture solver model.
+    Prioritize solved-conjecture answer recovery, proof-quality reasoning,
+    and evidence-grounded uncertainty. Never claim a proof unless it is fully
+    supported by explicit assumptions or known cited results.
+
+training_defaults:
+  per_device_train_batch_size: 1
+  per_device_eval_batch_size: 1
+  gradient_accumulation_steps: 24
+  weight_decay: 0.01
+  warmup_ratio: 0.03
+  lr_scheduler_type: cosine
+  max_grad_norm: 1.0
+  gradient_checkpointing: true
+  logging_steps: 10
+  save_steps: 350
+  eval_steps: 350
+  save_total_limit: 3
+  dataloader_num_workers: 2
+
+stages:
+  - name: solved_corpus_bootstrap
+    max_train_samples: 240000
+    max_eval_samples: 4500
+    filters:
+      include_families:
+        - competition
+        - structured_reasoning
+        - formal_proof
+        - conjecture_core
+    training:
+      num_train_epochs: 1
+      learning_rate: 2.0e-5
+
+  - name: conjecture_answer_alignment
+    max_train_samples: 110000
+    max_eval_samples: 3000
+    filters:
+      include_families:
+        - conjecture_core
+        - formal_proof
+      min_sample_weight: 2.0
+    training:
+      num_train_epochs: 2
+      learning_rate: 8.0e-6
+      save_steps: 220
+      eval_steps: 220
+
+  - name: formal_consistency_refinement
+    max_train_samples: 70000
+    max_eval_samples: 2200
+    filters:
+      include_families:
+        - conjecture_core
+      require_conjecture_id: true
+    training:
+      num_train_epochs: 2
+      learning_rate: 4.5e-6
+      save_steps: 120
+      eval_steps: 120
+
+  - name: hard_case_polish
+    max_train_samples: 50000
+    max_eval_samples: 1500
+    filters:
+      include_families:
+        - conjecture_core
+        - formal_proof
+      require_conjecture_id: true
+      min_sample_weight: 3.0
+    training:
+      num_train_epochs: 1
+      learning_rate: 2.0e-6
+      gradient_accumulation_steps: 24
+      save_steps: 80
+      eval_steps: 80
+
+post_eval:
+  enabled: true
+  eval_file: workspace/data/releases/v1/test.parquet
+  max_samples: 260
+  k: 8
+  max_new_tokens: 512
+  temperature: 0.6
+  top_p: 0.92
+  seed: 17
+  output_json: workspace/runs/math-conjecture-sota/post_eval_report.json
+
+quality_gate:
+  enabled: true
+  require_post_eval: true
+  min_evaluated_rows: 140
+  min_pass_at_1: 0.02
+  min_pass_at_k: 0.09
+  max_final_eval_loss: 2.5
+  required_family_pass_at_k:
+    conjecture_core: 0.09
+    formal_proof: 0.06
+
+hub:
+  push_to_hub: true
+  repo_id: NorthernTribe-Research/math-conjecture-model
+  private: false
+  upload_stage_checkpoints: true
+  commit_message: Run autonomous multi-stage math-conjecture solver training with post-eval quality gates and publish qualified adapters/checkpoints.
+
+credentials:
+  path: huggingface-api-key.json

configs/{deepseek_math_sota.yaml → qwen25_math_sota.yaml}

@@ -1,10 +1,10 @@
 global:
-  output_root: workspace/runs/math-conjecture-sota
+  output_root: workspace/runs/math-conjecture-sota-qwen25
   seed: 17
 
 model:
-  base_model: deepseek-ai/deepseek-math-v2
-  trust_remote_code: true
+  base_model: Qwen/Qwen2.5-Math-7B-Instruct
+  trust_remote_code: false
   use_bf16: true
   load_in_4bit: true
   bnb_4bit_quant_type: nf4
@@ -32,38 +32,37 @@ data:
   final_answer_field: final_answer
   proof_field: proof_formal
   sample_weight_field: sample_weight
-  max_seq_length: 3072
+  max_seq_length: 4096
   min_loss_weight: 0.25
   max_loss_weight: 6.0
   family_boost:
-    conjecture_core: 2.6
-    formal_proof: 1.8
-    competition: 1.25
-    structured_reasoning: 1.0
+    conjecture_core: 2.8
+    formal_proof: 2.2
+    competition: 1.35
+    structured_reasoning: 1.1
   system_prompt: |
     You are a frontier mathematical reasoning model focused on unsolved
-    conjectures. Your outputs must be precise, technically coherent, and explicit
-    about uncertainty. Never claim a full proof unless it is derivable from given
-    assumptions or already established in cited prior results.
+    conjectures. Prioritize formal consistency, proof structure, and explicit
+    uncertainty when a complete proof is unavailable.
 
 training_defaults:
   per_device_train_batch_size: 1
   per_device_eval_batch_size: 1
-  gradient_accumulation_steps: 16
+  gradient_accumulation_steps: 24
   weight_decay: 0.01
   warmup_ratio: 0.03
   lr_scheduler_type: cosine
   max_grad_norm: 1.0
   gradient_checkpointing: true
   logging_steps: 10
-  save_steps: 400
-  eval_steps: 400
+  save_steps: 350
+  eval_steps: 350
   save_total_limit: 3
   dataloader_num_workers: 2
 
 stages:
   - name: broad_math_bootstrap
-    max_train_samples: 180000
+    max_train_samples: 220000
     max_eval_samples: 4000
     filters:
       include_families:
@@ -76,7 +75,7 @@ stages:
       learning_rate: 2.0e-5
 
   - name: conjecture_specialization
-    max_train_samples: 80000
+    max_train_samples: 100000
     max_eval_samples: 2500
     filters:
       include_families:
@@ -86,11 +85,11 @@ stages:
     training:
       num_train_epochs: 2
       learning_rate: 8.0e-6
-      save_steps: 250
-      eval_steps: 250
+      save_steps: 220
+      eval_steps: 220
 
   - name: conjecture_alignment
-    max_train_samples: 40000
+    max_train_samples: 60000
     max_eval_samples: 2000
     filters:
       include_families:
@@ -99,11 +98,11 @@ stages:
     training:
       num_train_epochs: 2
       learning_rate: 5.0e-6
-      save_steps: 100
-      eval_steps: 100
+      save_steps: 120
+      eval_steps: 120
 
   - name: hard_case_polish
-    max_train_samples: 30000
+    max_train_samples: 50000
     max_eval_samples: 1500
     filters:
       include_families:
@@ -113,7 +112,7 @@ stages:
       min_sample_weight: 3.0
     training:
       num_train_epochs: 1
-      learning_rate: 3.0e-6
+      learning_rate: 2.5e-6
       gradient_accumulation_steps: 24
       save_steps: 80
       eval_steps: 80
@@ -123,29 +122,29 @@ post_eval:
   eval_file: workspace/data/releases/v1/test.parquet
   max_samples: 240
   k: 6
-  max_new_tokens: 320
+  max_new_tokens: 512
   temperature: 0.7
   top_p: 0.95
   seed: 17
-  output_json: workspace/runs/math-conjecture-sota/post_eval_report.json
+  output_json: workspace/runs/math-conjecture-sota-qwen25/post_eval_report.json
 
 quality_gate:
   enabled: true
   require_post_eval: true
   min_evaluated_rows: 120
-  min_pass_at_1: 0.01
-  min_pass_at_k: 0.06
+  min_pass_at_1: 0.015
+  min_pass_at_k: 0.08
   max_final_eval_loss: 2.6
   required_family_pass_at_k:
-    conjecture_core: 0.06
-    formal_proof: 0.03
+    conjecture_core: 0.08
+    formal_proof: 0.05
 
 hub:
   push_to_hub: true
   repo_id: NorthernTribe-Research/math-conjecture-model
   private: false
   upload_stage_checkpoints: true
-  commit_message: Run autonomous multi-stage DeepSeek-Math training with post-eval quality gates and publish qualified adapters/checkpoints.
+  commit_message: Run autonomous multi-stage Qwen2.5-Math-7B training with post-eval quality gates and publish qualified adapters/checkpoints.
 
 credentials:
   path: huggingface-api-key.json

scripts/eval_sota.py

@@ -16,7 +16,7 @@ from peft import PeftModel
 from transformers import AutoModelForCausalLM, AutoTokenizer, set_seed
 
 SCRIPT_ROOT = Path(__file__).resolve().parents[1]
-DEFAULT_CONFIG_PATH = SCRIPT_ROOT / "configs" / "deepseek_math_sota.yaml"
+DEFAULT_CONFIG_PATH = SCRIPT_ROOT / "configs" / "math_conjecture_sota.yaml"
 DEFAULT_OUTPUT_JSON = SCRIPT_ROOT / "runs" / "latest_eval_report.json"
 
 BOXED_RE = re.compile(r"\\boxed\{([^{}]+)\}")

scripts/preflight_check.py

@@ -17,7 +17,7 @@ import yaml
 
 
 ROOT = Path(__file__).resolve().parents[1]
-CONFIG_PATH = ROOT / "configs" / "deepseek_math_sota.yaml"
+CONFIG_PATH = ROOT / "configs" / "math_conjecture_sota.yaml"
 HF_HOME_DIR = ROOT / "workspace" / ".hf_home"
 HF_DATASETS_CACHE_DIR = HF_HOME_DIR / "datasets"
 HF_HUB_CACHE_DIR = HF_HOME_DIR / "hub"

scripts/train_sota.py

@@ -30,13 +30,13 @@ from transformers import (
 )
 
 SCRIPT_ROOT = Path(__file__).resolve().parents[1]
-DEFAULT_CONFIG_PATH = SCRIPT_ROOT / "configs" / "deepseek_math_sota.yaml"
+DEFAULT_CONFIG_PATH = SCRIPT_ROOT / "configs" / "math_conjecture_sota.yaml"
 DEFAULT_EVAL_SCRIPT = Path(__file__).resolve().with_name("eval_sota.py")
 
 
 def parse_args() -> argparse.Namespace:
     parser = argparse.ArgumentParser(
-        description="Train DeepSeek-Math with a multi-stage SOTA curriculum recipe."
+        description="Train math-conjecture solver with a multi-stage SOTA curriculum recipe."
     )
     parser.add_argument(
         "--config",