iolai26-solve/DESIGN.md

IOL-AI 2026 Solver — System Design

Paradigm: single-shot LLM reasoning with deterministic tools. One model call per puzzle. Before the call, exact algorithms analyze the puzzle and inject what they found into the prompt; after the call, verified symbolic answers override the model where the verifier has real evidence, and format guards clean up the rest. The LLM does what only it can (compositional semantics, novel-rule reasoning); the tools do what they do perfectly (segmentation, alignment, arithmetic, verification against attested data); neither is asked to do the other's job.

This document describes the final v1 architecture: what runs, in what order, why each component exists, and the evidence behind the design choices.

---

1. Constraints the design answers to

Constraint	Design consequence
Single T4 (16 GB), 30-minute wall clock, offline	7–14B AWQ model max; one batched generation pass; symbolic work is ~free (seconds); hard budget cutoff with graceful degradation
Score = √(EMw · chrFw), points-weighted	Never emit an empty answer (geometric mean → one zero factor craters the row); chrF partial credit makes a plausible-but-wrong answer far better than nothing
EM = strip().lower() equality only	Punctuation and spacing are significant; answers must match the gold's surface conventions
Test set = fresh IOL 2026 problems (Linguini format)	Zero contamination help — the model must genuinely deduce; scaffolding is most valuable exactly here
Optional human-judged explanation track	Emit an explanation column; jury wants short structured bullets, not raw traces

Key empirical facts driving the architecture (from the literature survey and our own 160-puzzle Linguini baseline):

• All models score < 25% EM on Linguini; open T4-sized models are in the low single digits. The model is not a magic bullet at this scale.
• Explicit morpheme segmentation in the prompt is the best-evidenced intervention in the field (documented gains up to +60 points/puzzle).
• GPT-5 Pro scored 8/98 on the live IOL 2025 without scaffolding — fresh problems are brutal for pure single-shot reasoning at any scale.
• Our symbolic stack alone: EM 2.4% / chrF 20 on all 160 Linguini puzzles in ~9 seconds — comparable to what a naive T4 baseline can do, at ~0 cost.

2. Runtime flow

/tmp/data/test.csv
   │
   ▼
┌────────────────────────────────────────────────────────────┐
│ 1. SYMBOLIC PASS  (~seconds, no GPU)                       │
│    parse → route by task type →                            │
│      numeral CSP · table completion · template translation │
│      · Hungarian matching · analogy · fallback ladder      │
│    every item gets: answer + verifier confidence + method  │
└────────────────────────────────────────────────────────────┘
   │
   ▼
┌────────────────────────────────────────────────────────────┐
│ 2. SCAFFOLDED LLM PASS  (the 30-min budget)                │
│    for each puzzle with an unverified item, ONE call:      │
│      context + query                                       │
│      + morpheme segmentation hypotheses                    │
│      + word-alignment hypotheses                           │
│      + verified numeral values (when induced)              │
│      + symbolic candidate answers (conf ≥ 0.4 only)        │
│    → model reasons compositionally, emits                  │
│      FINAL ANSWERS: … then EXPLANATION: bullets            │
│    batched (4/batch) · greedy · weakest-puzzles-first ·    │
│    hard budget cutoff                                      │
└────────────────────────────────────────────────────────────┘
   │
   ▼
┌────────────────────────────────────────────────────────────┐
│ 3. MERGE + GUARDS                                          │
│    verified symbolic (conf ≥ 0.5)  >  LLM answer  >        │
│    never-empty fallback                                    │
│    per-task-type cleanup: digits for text_to_num, letter   │
│    extraction for match_letters, preamble/quote stripping  │
└────────────────────────────────────────────────────────────┘
   │
   ▼
submission.csv   (id, pred = JSON list, explanation = bullets)

The merge rule is the heart of the design: an answer is kept symbolic only when the verifier showed the producing rule actually generalizes (leave- one-out fit on the attested pairs, or a numeral system that round-trips every attested example). The LLM cannot verify itself; the tools can — so verified tool output outranks the model, and unverified tool output is demoted to a labeled hint inside the prompt instead of an override.

3. Components

Entry & orchestration

File	Purpose
script.py	Competition entrypoint. Sets offline env vars, reads the test CSV, calls the pipeline, writes submission.csv (id, pred, explanation). ~60 lines; all logic lives below.
solver/pipeline.py	run_pipeline() — the three-stage flow above, shared verbatim by script.py and the dev harness, so the locally tested path is exactly the submitted path. Owns the merge policy (CONF_KEEP = 0.5), the weakest-first LLM ordering, the budget cutoff, per-task format guards, and explanation assembly.
solver/budget.py	Wall-clock accounting: elapsed/remaining with a safety margin; the pipeline consults it before each LLM batch.

The LLM layer

File	Purpose
solver/llm.py	Client abstraction. HFTransformersClient (production: fp16, device_map=auto, greedy, LEFT-padded batching, version-drift-safe chat templating — the sandbox runs an older transformers than Colab); NullClient (no weights → symbolic-only pipeline still runs, used locally and as the crash floor); CallableClient (tests inject scripted models); VLLMClient (optional experiments only — never required). load_client() finds weights at the repo root (config.json), per the submission convention MODEL_ID = ".".
solver/direct.py	The single-shot solver. SYSTEM prompt (v1): derive rules only from the given data, don't assume English-like grammar, work compositionally (morphemes → order → sound changes), per-task-type answer formats, match the examples' punctuation; then FINAL ANSWERS: (one bare answer per line) then EXPLANATION: (2–4 bullets). parse_output() is a superset of the official baseline parser — a model that ignores the explanation instruction still parses. Explanations therefore cost zero extra forward passes.
solver/scaffold.py	Builds the tool-analysis prompt block: segmentation hypotheses (multi-morph words only), alignment hypotheses (top-2, score-filtered), verified numeral values, and symbolic candidates labeled with source + fit. Size-capped (≤ 40 seg lines, ≤ 30 align lines, 60-word vocab) — measured max prompt ≈ 1.5k tokens over the 160 real puzzles. Low-confidence candidates are excluded so garbage can't anchor the model.

The symbolic toolbox (all pure Python, no dependencies, runs anywhere)

File	Purpose
solver/preprocess.py	Parsing reality. Normalization (NFC, keeps diacritics/tone/punctuation), context parsing (pipe tables 2–5 cols with header detection, numbered/lettered lists, =/dash pairs, prose hints), query parsing (numbered items that continue context numbering, bare-line items, (k) blank markers in any column, wrapped-line continuation, instruction detection that survives task-language colons), context-derived items for instruction-only queries. Item counts match gold on 158/160 real Linguini puzzles.
solver/align.py	Word alignment from tiny corpora: minimal-pair set-difference links (exact, high-precision), Dice co-occurrence, morphological back-off (single-word glosses project into inflected forms containing them), and competition/explaining-away (a target already claimed by a stronger suitor is demoted — breaks the pervasive ties of 10-sentence corpora).
solver/segment.py	MDL morpheme segmentation conditioned on alignment (shared-gloss groups get boundary bonuses). Feeds the scaffold — the field's best-evidenced intervention.
solver/template.py	Template translation: find the attested sentence closest to the query (bag distance, length-mismatch tie-break), swap the differing tokens through alignments; context-aware substitution (candidate must exist in the template's target) and affix-matched replacement (kupu:nakupu :: moko:namoko). Both directions. Abstains rather than fabricates.
solver/tables.py	Paradigm-table completion: match query-row cells to context-table columns (positional when same width, char-overlap otherwise; damaged/merged-marker rows handled), then learn the source→answer column mapping and pick the most learnable source column by LOO fit. Chain: template → char-level analogy voting → echo.
solver/numerals.py	Numeral CSP: induce morpheme values from attested (phrase, value) pairs under a multiplicative-additive convention, with constraint propagation and node caps (abstains fast instead of hanging on morphophonologically complex systems). Generation ranks candidate phrasings by attested-style consistency. Induced systems are round-trip verified against every attested example — the strongest confidence in the system (0.9).
solver/matching.py	match_letters: pure-Python Hungarian over lexical-alignment + structural-similarity scores. Real-data EM is weak (~5%), so its confidence (0.45) deliberately sits below the keep-threshold: the assignment reaches the model as a hint, never an override.
solver/analogy.py	Proportional analogy a🅱️:c:x (prefix/suffix/infix edits), with multi-exemplar voting. Used inside tables and fallback.
solver/fallback.py	The chrF floor: analogy transfer from the closest attested pair → echo of the closest attested target → word-by-word alignment gloss → the query itself. Guarantees no empty answer ever.
solver/router.py	Task-type dispatch producing (answers, confidences, methods) per item. Confidence semantics: LOO/eval fit of the producing solver; 0.9 for round-trip-verified numerals; 0.0 for fallback — "0.0" is precisely the signal "worth LLM budget".
solver/verifier.py	The single verification object: EM+chrF fit on attested pairs, with two honest regimes — fixed programs are evaluated directly (they must reproduce the data), fit-from-data predictors are scored leave-one-out (else memorization always beats generalization). Fold-capped at 12 for the time budget.

Research-track components (not in the runtime path)

File

Purpose

solver/dsl/ + solver/synth.py + prompts/

The CEGIS grammar-synthesis loop: LLM proposes a grammar in a small DSL (lexicon/affixes/rewrites/order), a deterministic interpreter executes it both directions, the verifier scores it, failures feed back. Fully built and tested, but not called by the pipeline: the literature says the proposer is the bottleneck and T4-sized models are weak proposers of formal artifacts. Kept as the ablation/ceiling-raising track (no published DSL/CEGIS solver exists for this domain — it's a genuine contribution if it pans out).

Metrics (runtime) & evaluation (dev-only, not in the submission repo)

File	Purpose
solver/metrics.py	Official semantics, dependency-free, needed AT RUNTIME by the verifier and fallback: EM = strip().lower() with per-item gold alternatives; chrF replicates sacrebleu exactly (0.0 delta over 500 fuzz cases); geomean aggregate.
eval/, tests/, data/	Local-only (gitignored) — the sandbox runs script.py alone, so the dev harness (runs run_pipeline over gold-labeled CSVs), the 5 test suites (50+ tests), and the Linguini dev-set generator stay out of the public HF repo. They live on disk in the working copy.

4. The prompt (v1 rationale)

Decisions, given the "don't ablate CoT now, pick a best v1" directive:

• Brief reasoning retained, but re-aimed. The literature shows generic step-by-step reasoning can hurt here (models anchor on English-like rules). The v1 prompt keeps concise reasoning — small models need scaffolding to organize composition — but adds the explicit counter-instruction: "Derive the rules ONLY from that data — do not assume the language works like English or any language you know," and directs the reasoning into a compositional procedure (morphemes → meanings → order → sound changes).
• Tool output is framed as hypotheses ("may contain errors — the attested data always wins"), and candidates carry their source and fit score, so the model can calibrate trust per hint.
• Output contract is baseline-compatible plus explanation. FINAL ANSWERS: parsing is a superset of the official notebook's parser; EXPLANATION: bullets ride in the same generation. Parser handles the reversed order too.
• Format guards, not format hopes. text_to_num answers are reduced to digits; match_letters answers to a single valid option letter; preambles ("The answer is…") and quotes stripped. EM's strict semantics make these worth real points.

5. Explanation track (opted in)

Every row ships an explanation:

• LLM-solved puzzles: the model's own EXPLANATION: bullets (rules found
  • key evidence) — the short structured form the jury asks for.
• Symbolically-solved puzzles: a generated trace sentence per method (e.g. numeral: "induced each morpheme's value … verified the system reproduces every given example"). These are true descriptions of what the solver did — arguably more faithful than any post-hoc model prose.

Coverage measured at 160/160 on the dev set (requirement: ≥ 50%).

6. Time budget

Measured: symbolic pass + scaffold building ≈ 11 s for 160 puzzles; prompts median ~800 tokens, max ~1.5k. Generation dominates. The shipped model is Qwen2.5-7B-Instruct-AWQ (~5.6 GB, Apache-2.0): same organizer-validated family as the workshop baseline, but 2–3× faster than the 14B on the T4 and leaving ~9 GB of KV headroom for batch 6 — under the 30-minute cap, more scaffolded puzzles per minute beats a smarter-but-slower model whose runs get cut off. (The 14B also physically cannot be prepared on the current dev machine: ~20 GB local footprint with git-lfs against ~13 GB free.) A full 160-puzzle set at 1536 new tokens would still exceed 30 minutes — the weakest-first ordering + cutoff degrades the tail to verified symbolic/ fallback answers rather than failing. The actual hidden test set is the IOL 2026 individual contest (typically ~5 problems reformatted → far fewer rows), which fits comfortably. Colab-tunable knobs, in order: MAX_NEW_TOKENS (1536 → 1024), LLM_BATCH (6 → 8), model swap via scripts/prepare_weights.py.

7. What was deliberately left out

• Agentic tool-calling loops — multiple forward passes per problem; 7–14B models are unreliable tool-callers; budget-hostile. The tools run before the call instead.
• Multi-agent orchestration — no evidence it helps at T4 scale; the one positive result used a frontier model on an adjacent benchmark.
• CEGIS in the runtime path — see research-track note above.
• Self-consistency / best-of-N — greedy decoding is mandated-adjacent (reproducibility) and no linguistics-specific evidence supports the spend.
• CoT A/B testing — explicitly deferred per direction; the v1 prompt takes the middle path described in §4.

8. Submission checklist

• script.py at repo root; reads /tmp/data/test.csv, writes submission.csv with id, pred (JSON list), explanation
• Offline: HF_HUB_OFFLINE=1, TRANSFORMERS_OFFLINE=1 set in-script; weights load from .
• Never-empty answers; per-row crash containment; budget cutoff
• OOM containment (learned from the first live submission, which crashed): prefill logits on the sandbox's transformers are batch-total-tokens × 152k vocab × fp32 — so generation batches are packed by a 3,500-token budget, OOM retries drop to single prompts then abstain, logits_to_keep=1 is passed when supported, and submission.csv is checkpoint-written after the symbolic pass and every LLM batch so ANY later crash still leaves a complete submission
• All 5 test suites green; dev harness runs the identical pipeline
• Weights in repo: Qwen2.5-7B-Instruct-AWQ at the repo root (git-lfs via .gitattributes; LICENSE retained; Apache-2.0 satisfies the competition's open-licensing/redistribution rule; README carries the HF model-card metadata)
• One Colab T4 validation run via the workshop notebook (timing + real model output through parse_output) before the first real submission