6 Logic

Update 2026-10-09 — routing gate 1.6.0: reads formal notation, stops sending chat to the solver — held-out F1 78.2 → 95.8 (+17.6 [+11.2, +25.5]); live, still watch-only

Correction first. This morning's held-out figure (F1 38.7) was mis-scored. It counted CC06-C items 291–300 as non-logic, but they are Band G "semantic compiler" logic items: formalise the wording, then solve. So all 100 items are logic problems. Corrected: the live gate 1.4.0 sent 34 of 100 to a logic route. Precision can't be measured on CC06-C, because the set contains no non-problems. The 38.7 row is now an anchor at 50.7 (recall-only F1).

What was wrong (two faults). - It missed notation. The gate fired on English connectives (if, must, unless). E1: X1 XOR X2 … = 1, X6 := NAND(X3, X4), K_A(X4=0) and edge lists carried no trigger word, so 66 of the 100 CC06-C items were kept from the solver. - It sent chat to the solver. Her seat passes the operator message to the gate with its [situated-frame] header attached (trust=1.0 when=2026-10-09 12:26). The gate read those as quantities and relations. Separately, any message with one quantifier, one number and a question mark counted as "representable". In the live shadow log, 30 of 119 ordinary turns went to a logic route, among them "What is the velvet glove", "All good?" and "Did you finish all 100 logic puzzles yet?".

The fix (gate 1.6.0, Claude). 1. The situated-frame header is stripped before classifying. 2. Notation route. Dense formal notation goes to the declarative front: operator words and calls, logic, modal and set symbols, ASCII ~ & |, forall/exists, indexed variables, var = value, and edge lists. Arrows count only between non-numeric operands, so 47.5 → 74.0 in a progress report does not count. 3. Problem-kernel guard on every word-triggered route. The message must name two or more quantities or entities, or a declared domain, or state two or more premises before an ask. Long first- and second-person prose is not a problem. 4. Logic-domain terms (satisfiable, knights/knaves, chromatic, cryptarithm, power set …) route when a kernel is present. 5. Code, SQL and log shapes are kept off the formal routes unless notation is dense.

How it was tested. - First attempt failed. 1.5.0 was preregistered (PREREG-G15) and judged on a fresh set of 154 messages written by an independent model that never saw the gate. It came in at F1 +4.3 [−1.5, +10.2] with recall 77.0, against bars of +10 and 80. Not installed. Its misses (ASCII connectives, modal logic, edge lists, no domain vocabulary) went into 1.6.0, and that set became development data. - 1.6.0 was preregistered (PREREG-G16) and judged once on a second fresh draw of 143 messages: 70 problems in 12 formats and 73 look-alike non-problems. The non-problems were status chat, reports with arrows, code, SQL, logs, stats questions, forum posts and task requests.

Change +17.6, bootstrap 95% CI [+11.2, +25.5]. All four preregistered criteria were met.

Checked as well. - Dev: CC06-C 100/100 (1.4.0: 32), suite A 96/100, canary pool 20/20 + 20/20. - Live shadow log: false positives 30 → 0 of 119. Logic turns 2 of 5 (1.4.0: 3 of 5). The miss is a long pasted list of web puzzles. - Her own gate checks give identical results to 1.4.0. - Speed: the readings post-pass takes at most 0.18 s per item.

Caveat. The second fresh set came from the same generator and prompts as the first, which 1.6.0 was tuned on. The pass shows the fix generalises within that distribution. The real test is her live traffic: in 48 h the new shadow rows will be read by hand.

Status. Installed 14:51 as a whole-file replace, after confirming the live file was unchanged (backup gate.py.bak-claude-g16-20261009). It is still watch-only: it logs, it does not route. Enforcement stays off.

Parts that do it - ~/cognition-bench/06-logic/gatefix/: PREREG-G15.txt (+ heldout/RESULT-G15.txt), PREREG-G16.txt, heldout2/ (items, sha256, label log, duplicate log), score_g16.py, evalgate.py, dev sets - Firefly learning/puzzle-lab/logiclab/gate.py 1.6.0

Update 2026-10-09 — held-out set CC06-C graded: she solves it (97/100 right, 3 partial, 0 wrong), but her routing gate fails it (F1 38.7; corrected later: 34/100 routed) — it reads English connectives, not constraint notation; it stays watch-only

The test. CC06-C is the operator's third logic set: 100 items written after her gate's last edit (the set arrived 10-07 14:41, the gate was last changed at 10:47). Her answers, emailed 10-07 15:32, were graded on 10-09 against the operator's key. The key was sealed on the bench machine and never placed on Firefly.

• No one saw the key early. Her answer file is byte-identical to what she sent (sha256 in her hand-in record). A scan of every worker session between 14:35 and 15:40 on 10-07 found no access to the key.

Solving: 97 of 100 fully right, 3 partial, 0 wrong.

• How the 90 formal items were graded. By machine, with a negative control: graded against a deliberately wrong key, the grader fails almost everything. The ten semantic items were graded by hand against the key's gold readings.
• The three partials share one pattern: a reading quietly strengthened.
• 293(b): the structural model's state conflicts with two observations; she resolved the conflict by fixing them and called the result consistent.
• 296: "A is not thereby required" became the forced literal "A is not obligatory".
• 298: "mechanical birds normally fly only when powered" became "unpowered ones do not fly", which is the converse the item tests for.

Routing: her gate fails the held-out set.

The live gate (1.4.0) was run read-only on a copy of her code. The gate decides from English connectives such as if, then and must, plus a representability heuristic. It does not recognise symbolic constraint notation:

• the 48-variable XOR systems and the repair problems were judged "not representable" and kept away from the solver;
• the announcement and causal items had "no formal signal";
• the natural-language items, full of if and then, went to the solver.

Her own 10-07 report warned that its numbers were "a development reading, not a validation". This is the validation, and it fails. The gate must stay watch-only. It is now (135 logged turns), so her answers were not affected: she chose z3 herself and solved the set.

Summary score. The summary keeps routing F1 as its metric, now measured on the held-out set: 0 (no formal path) → 38.7. The development numbers are kept as reference rows. [Corrected 10-09 PM: 38.7 was mis-scored, because items 291–300 are logic items, not negatives. It is now a reference row (recall 34/100). The summary is now the matched held-out test of gate 1.4.0 vs 1.6.0: 78.2 → 95.8; see the later update.] Solving accuracy (98.5 with partials at half) is a separate reference row.

Readings lane. Piper delivered the readings lane the operator asked for on 10-07; it is part of gate 1.3.0+. Claude re-ran her numbers and they came out identical.

Next. The gate needs to read constraint notation (XOR, =, variable lists, edge lists) as formal, and connective words alone should not be enough. Test it on a fourth set before any enforce.

Parts that do it - Bench: ~/cognition-bench/06-logic/grade_cc06c.py, grade-cc06c-20261009.json, cc06c-routing-gate140*.json; sealed key and answers /var/lib/cognition-bench/06-logic/cc06c/ (root only)

Update 2026-10-07 — CC06-B graded against the operator's key: 85 of 85 keyed items correct, and her encodings are faithful

Graded by Claude, off Piper's machine. The key never went to Firefly. Her answer files were copied off read-only.

How it was checked. Getting the verdict right is not the whole test. For every SAT item, the operator's planted solution was evaluated against her encoding of the constraints. If she had misread a single constraint, the planted solution would usually fail it. None failed. For every UNSAT item her unsat core was inspected. The ordering bands' cores are exactly the injected 4-cycle. Some Boolean cores are shorter than the injected 7-clause cycle because they shortcut through a ↔ clause (e.g. 108: B03, B08↔B03, B08→¬B03), which is still a valid contradiction.

What it means. Her exact path is correct on everything a solver should own. The open problem is entirely upstream, in deciding what goes to the solver. On the semantic items she already did the right thing by hand: she enumerated every defensible reading of each ambiguous clause, solved each one, and reported "robust" when all readings agreed (10 items). When they didn't (5 items), she reported the separating assumption. That procedure is what the router should send ambiguous wording to. Today the gate either sends it to the solver as certain or sends it nowhere.

Update 2026-10-07 — her own upgrade, read from her logs: a solver path now exists and answered both suites with Z3; the routing gate is accurate on formal items but over-routes prose, and runs in shadow only

What she did (project cognitive-component-06, 10-06 → 10-07, closed done; everything in foundation/state/cc06/). Working from the operator's logic paper, she: - built a logic gate (logiclab/gate.py 1.2.0). It is a deterministic router that sorts a request into formal / quantitative / code / hybrid / open, with a representability check so a vague request is not forced through a solver; - built a semantic lint that flags constructions with two readings ("only if", "knows", "exactly") and solves both; - keyed the operator's CC06 suite (items 1–100): 71 items by independent brute-force code that shares nothing with the gate, and 29 reading-dependent items by stated convention. She then answered all 100; - answered the harder CC06-B suite (items 101–200, 20–50 variables each) with Z3 5.1.0. Every SAT witness was re-checked against the parsed constraints by a separate evaluator (0 bad models), and each UNSAT verdict carries an unsat core. Both answer sheets went to the operator's laptop (sha256 verified); - wired the gate into the router in shadow: it classifies each operator message and logs it (shadow.jsonl), and the result is discarded.

Baseline (review, 09-30). Formal logic was absent. No rule routed anything to Z3, no worker had ever solved anything with logiclab, and Z3 was installed only in a lab venv. Probability (probkit) was real. The base model (deepseek-flash, no tools) already gets the 21 small keyed CC06 items right (21/21), so on small problems the gap was never the model's reasoning. It was the absence of an exact path for large or trap-laden ones.

Where it stands (her measurements; the routing numbers re-run by Claude 10-07 and identical):

Reading it. - The exact path now exists and works. Z3 solves the large items and every witness checks out, and she built a key that does not depend on the machinery it grades. That is the paper's core recommendation done, on the bench. - The router is the weak link. It sends nearly every formal item to the solver, but it also sends most reading-dependent prose there as "certain". That is the exact failure the paper warns about, a solver giving a confident answer to one reading of an ambiguous sentence. The lint is meant to catch these, but it is not yet good enough to rely on (38 false flags). - Wired in, but watch-only. The gate runs inside her turn path (foundation_router.py → cc06_shadow.py) on every operator message and logs a decision; the decision is not acted on. Live routing is 13/17 right, below the paper's bar, so keeping it watch-only is the right call for now.

Next. 1. ~~Grade CC06-B against the operator's key~~ done 10-07: 85/85. 2. Fix gate precision on prose: ambiguous wording goes to a readings lane (see next entry), not straight to the solver. 3. Re-score live shadow turns before any switch to enforce.