Summary / 6. Logic / Document
2026-10-06
Shared copy: the operator's name and machine names are replaced by roles. Nothing else is changed.
Rendering…
# Piper Cognitive Component 6 — Logic ## Solver-Gated Formal Reasoning: Research Review, Architecture, Benchmark, and Engineering Design **Component:** 6 — Logic **Working definition:** Applying formal or rule-based relationships **System:** Piper **Status before this work:** Latest — not scored; baseline — absent; live use — partial and mostly outside formal logic **Date:** 2026-10-06 --- ## Abstract Piper already contains the right kind of machinery for exact logical work but does not yet reliably *use* it. `logiclab` and Z3 provide a deterministic constraint-solving substrate; `probkit` provides a tested home for probability and statistical calculations; and `code-check` provides deterministic syntax and lint checks. The architecture claim is therefore stronger than the observed behavior. The reviewer audit found substantial real use of `probkit` and `code-check`, but no meaningful historical use of `logiclab` for formal reasoning. In practice, formal solver use is an installed capability rather than an operational cognitive behavior. This paper defines Logic narrowly enough to measure it. The target capability is not “sounding logical” or producing persuasive chains of thought. It is the ability to recognize when a problem has a formal structure, translate the relevant natural-language statements into a faithful symbolic representation, send that representation to an appropriate deterministic solver, correctly interpret the result, and refuse or fall back when the problem cannot be safely formalized. This distinction matters because modern language models can reach correct answers with invalid reasoning, while symbolic solvers can produce perfectly correct answers to incorrectly formalized problems. The system therefore has two distinct failure surfaces: **semantic formalization** and **formal inference**. The recommended Piper architecture is a small **Logic Gate** in front of existing exact tools. It classifies tasks into solver-shaped formal logic, quantitative/probabilistic calculation, deterministic code checking, ordinary semantic reasoning, or hybrid tasks. For solver-shaped tasks, Piper becomes a semantic parser and repair controller rather than the final reasoner. The path is: > detect formal structure → extract entities/relations/constraints → formalize → validate the formalization → solve → verify witness or contradiction → reconstruct the answer → log the full trace. This follows the strongest practical lesson from SatLM, Logic-LM, LINC, certified deductive reasoning systems, and recent formalization benchmarks: **make the language model responsible for meaning, and make a deterministic formal system responsible for consequences of that meaning.** The proposed `LOGIC-v1` battery contains sealed, exactly gradable tests for routing, natural-language-to-formal translation, rule chains, propositional and first-order fragments, constraint satisfaction, scheduling, satisfiability/contradiction, and boundary cases where Z3 should *not* be used. A separate probability track tests whether quantitative questions are routed to `probkit` without allowing probability accuracy to inflate the Logic score. Live-use telemetry measures whether solver-shaped real work actually reaches the solver. The immediate engineering priority is therefore not a new logical-reasoning model. It is to make the existing solver path unavoidable when appropriate, observable when used, and falsifiable when it fails. --- # 1. Current Piper Claim ## Piper — what it is > Formal constraint work is delegated to a real solver rather than reasoned at: puzzles, scheduling and Latin-square problems go to Z3 through the logic lab, and every probability or odds question goes through one tested implementation instead of inline arithmetic. That last rule exists because I have been confidently wrong about arithmetic before, and a wrong number I then act on is worse than no number. ## Piper — the parts that do it - `logiclab` v1.0 - Z3 - `probkit` v0.2.0 - `code-check` v1.0.1 ## Reviewer Claude, 2026-09-30 **Reviewer’s read before testing: good for probability, absent for formal logic.** The architectural concept is correct: formal logic should be handed to a real solver instead of improvised in prose. The behavioral claim is not yet supported. The reviewer found no rule in the main agent instructions or active bridge that reliably routes solver-shaped work to `logiclab`; no historical worker evidence of meaningful Z3 solving; and only inspection commands confirming that the tool existed. In contrast, `probkit` had been used roughly 85 times and `code-check` roughly 325 times. The reviewer’s key distinction is the right one: > “Puzzles, scheduling and Latin squares go to Z3” currently describes an intended policy, not an observed behavior. --- # 2. Audit Reconciliation The current component description mixes three different capabilities: 1. **formal logical/constraint reasoning** — `logiclab` + Z3; 2. **quantitative/probabilistic computation** — `probkit`; 3. **deterministic program checking** — `code-check`. All three belong to the same broader engineering philosophy: do not ask a stochastic language model to perform work that a deterministic instrument can perform more reliably. But they should not be scored as one capability. For Component 6, the primary score should answer: > Can Piper recognize formalizable rule and constraint problems, faithfully represent them, invoke an exact solver, and correctly use the solver result? `probkit` is relevant as a **routing boundary**. If a question asks for odds, expected values, Bayes updates, sampling statistics, or confidence intervals, Piper should route to `probkit`, not Z3. Correct `probkit` use therefore demonstrates tool-selection discipline but should not raise the formal Logic score. Likewise, `code-check` is evidence that Piper already benefits from deterministic verification, but lint success is not logical inference. It belongs in the broader verification architecture rather than the core Logic score. ### 2.1 Version note The existing component description says “z3-solver v4.x,” while the reviewer reported Z3 5.1.0. The reviewer’s number is plausible: Z3 5.1.0 was released in August 2026. The correct engineering response is not to keep either hand-written number. `logiclab` should log the actual runtime solver version automatically on each evaluation run or once per environment hash. **Rule:** system inventory should be measured from the executable environment, not remembered in prose. --- # 3. Operational Definition of Logic For Piper, **Logic** should mean: > The ability to identify formal relationships among propositions, rules, entities, variables, and constraints; represent those relationships without materially changing their meaning; derive or verify consequences using an appropriate formal method; and correctly distinguish valid, invalid, satisfiable, unsatisfiable, entailed, contradicted, and underdetermined cases. This definition has four required stages: \[ \text{Logic success} = \text{recognition} \times \text{formalization fidelity} \times \text{inference correctness} \times \text{result interpretation} \] The multiplicative form is intentional. A zero in any stage can destroy the result. A perfect solver cannot rescue a mistranslated premise. A perfect translation is useless if the solver is never called. A correct solver result can still be misreported to the user. A solver should not be forced onto a problem that cannot be faithfully formalized. --- # 4. What Counts as Logic The component should include the following classes. ## 4.1 Propositional reasoning Examples: - If A then B. - A. - Therefore B. - A or B. - Not A. - Therefore B. - Determine whether a collection of Boolean constraints is satisfiable. These can be represented with Boolean variables and connectives and are natural Z3 targets. ## 4.2 Rule-chain deduction Examples: - Every employee with access to the vault must have clearance. - Dana has access to the vault. - Therefore Dana has clearance. This includes multi-hop implication chains and finite rule systems. ## 4.3 Syllogistic and quantified fragments Examples: - All A are B. - No B are C. - Some A exists. - What follows? A bounded or otherwise supported fragment can be sent through Z3 or an appropriate theorem prover, provided the representation is explicit and the system handles quantifiers carefully. ## 4.4 Constraint satisfaction Examples: - logic-grid puzzles; - Latin squares; - assignment problems; - mutually exclusive choices; - resource constraints; - ordering constraints; - exact-count rules; - combinatorial placement. This is one of the strongest Z3 use cases because the language model does not need to search the combinatorial space itself. ## 4.5 Scheduling feasibility Examples: - Alice cannot work Tuesday. - Bob must work exactly three shifts. - No person may work two overlapping shifts. - Every shift requires two qualified workers. The key word is **feasibility**. Finding a schedule satisfying formal constraints is Logic. Deciding *which goals are worth scheduling* belongs to Planning. ## 4.6 Satisfiability and contradiction Examples: - Are these rules mutually consistent? - Which added constraint makes the system impossible? - Is the conclusion entailed, contradicted, or still possible? This is a direct match for SMT-style solving. ## 4.7 Formal checking of proposed solutions A worker may produce a proposed assignment, schedule, ordering, or set of values. Logic can verify that the proposal satisfies all formal constraints even if the proposal was generated elsewhere. This is important for Piper because the solver can be used not just as a generator but as a **critic**. --- # 5. What Does Not Count as Logic Component boundaries matter because otherwise Piper can appear to improve simply by counting adjacent tools. ## 5.1 Arithmetic by itself `37 × 281` is calculation, not formal logic. Use a calculator or deterministic arithmetic. ## 5.2 Probability and statistics Probability has formal rules, but Piper already has a dedicated quantitative instrument. Probability questions should route to `probkit` and be reported separately. ## 5.3 Causal reasoning “If I intervene on X, what happens to Y?” belongs to Component 9 — Causal Reasoning, even when a formal causal graph is used. ## 5.4 Counterfactual reasoning Counterfactual interventions belong to Component 35, even when implemented using symbolic machinery. ## 5.5 Planning Constructing a useful sequence of actions toward a goal belongs to Planning. A planner may call Logic to test feasibility or solve a constrained subproblem. ## 5.6 General argument quality An essay can be coherent, evidentially strong, and rational without being reducible to formal logic. Logic should not become a generic “good reasoning” score. ## 5.7 Code syntax and lint `code-check` is valuable deterministic validation but should not count as formal logical competence. --- # 6. The Central Engineering Distinction: Solver Correctness vs. Formalization Correctness A symbolic solver has a useful property: once given a correctly encoded problem within its supported theory, its output is far more dependable than an LLM improvising a solution token by token. But this creates a tempting false conclusion: > “If Z3 says it, the answer is correct.” That is only true **relative to the encoded formula**. Suppose the natural-language rule says: > Every technician works at most one site on Monday. If Piper accidentally encodes: \[ \forall t:\ \text{works}(t,\text{site}_1) \lor \text{works}(t,\text{site}_2) \] instead of an at-most-one constraint, Z3 can solve the wrong problem flawlessly. This makes formalization the critical trust boundary. SatLM’s core insight is to have the language model generate a declarative specification and let a theorem prover perform the search. Logic-LM similarly uses an LLM to produce symbolic formulations and then hands inference to deterministic solvers, with solver errors feeding a refinement loop. LINC treats the LLM primarily as a semantic parser into first-order logic before invoking formal inference. Later work on automated formalization continues to find that semantic translation remains imperfect and benefits from automatically generated tests and verification. For Piper, the best architecture is therefore not: > user → LLM → Z3 → answer It is: > user → task classifier → structured extraction → symbolic formalizer → formalization checks → Z3 → witness/counterexample checks → answer reconstruction → trace --- # 7. Research Findings Relevant to Piper ## 7.1 SatLM: declarative specification beats asking the model to search SatLM uses the model to generate a declarative problem specification and delegates actual search to an automated theorem prover. The important engineering lesson is not the exact benchmark result. It is the architectural division: - language models are useful at mapping natural language to structure; - general token generation is a poor substitute for systematic constraint search; - a declarative representation is often easier for the model to produce faithfully than an imperative solving procedure; - the formal engine can guarantee correctness relative to that representation. **Piper implication:** `logiclab` should accept declarative constraints, not expect Piper to manufacture a procedural search algorithm. ## 7.2 Logic-LM: symbolic solver plus repair loop Logic-LM formalizes natural-language logic tasks, invokes a symbolic solver, and uses solver feedback to repair malformed symbolic representations. The repair loop is directly relevant to Piper: \[ \text{formalize} \rightarrow \text{parse/type check} \rightarrow \text{solver} \rightarrow \text{error/counterexample} \rightarrow \text{repair} \] This is better than silently falling back to free-form reasoning when the formal representation fails. **Piper implication:** syntax/type errors, unsupported constructs, and unsatisfied sanity constraints should return machine-readable diagnostics to the formalizer. ## 7.3 LINC: the LLM as semantic parser LINC explicitly separates natural-language understanding from logical inference. This provides a useful conceptual boundary for Piper: the LLM’s role is to understand what the words mean and express that meaning formally; the inference engine owns derivation. **Piper implication:** do not celebrate “LLM reasoning” when a deterministic engine can own the actual proof/search stage. ## 7.4 Certified deductive reasoning: constrain what the model may claim Certified Deductive Reasoning with Language Models shows a complementary idea: a formal logical system can guide or constrain the model’s stepwise generation so that intermediate statements remain valid. Piper does not necessarily need to expose a long formal proof to the user. But this work supports an important policy: > If Piper presents a statement as a logical consequence of formal premises, the statement should be derivable from the formal state or accompanied by an explicit non-formal qualifier. This helps prevent “solver result + invented explanation.” ## 7.5 ProofWriter: exact rule reasoning can be behaviorally tested ProofWriter demonstrates that rule-based reasoning can be tested using generated theories with known implications and proof depths. **Piper implication:** much of `LOGIC-v1` can be machine generated. That makes the sealed set cheap to rotate and allows controlled changes in proof depth, distractor count, branching, negation, and contradiction. ## 7.6 FOLIO: natural-language first-order reasoning remains difficult FOLIO pairs natural-language reasoning problems with first-order logical structure. It is particularly useful because it evaluates the semantic interface between text and logic, not just solver competence. **Piper implication:** the benchmark should contain both synthetic templated tasks and natural-language paraphrases. Solving only clean generated syntax would test Z3, not Piper. ## 7.7 ZebraLogic: complexity still breaks LLM-only logical reasoning ZebraLogic generates logic-grid/CSP-style tasks with controllable complexity and shows substantial accuracy degradation as search complexity rises, even for strong reasoning models and with more inference-time computation. This is an especially strong justification for Piper’s original instinct. Search-space growth should be handled by a solver designed for search, not by “thinking harder” in prose. **Piper implication:** difficulty should be parameterized by constraint structure and search-space complexity, and Piper should increasingly prefer solver use as complexity rises. ## 7.8 2026 formalization work: the parser remains the dangerous part Recent work on post-condition formalization found that current LLMs can generate useful formal specifications, but none of the tested systems correctly formalized every task; automatically generated tests exposed errors that would otherwise have passed. A 2026 Z3-based verification system for zkEVM code likewise uses the LLM as a formalization front-end and the SMT solver as correctness arbiter, with decomposition and verification-guided repair. **Piper implication:** the symbolic translation must itself be tested and logged. “Z3 returned SAT” is not sufficient evidence. --- # 8. Proposed Piper Architecture: The Logic Gate The minimal useful new component is not another solver. It is a deterministic routing and verification wrapper around the tools Piper already owns. ```text ┌──────────────────────┐ User / worker problem ──▶│ Logic Gate │ └──────────┬───────────┘ │ classify task shape / risk │ ┌─────────────────────────────┼────────────────────────────┐ │ │ │ ▼ ▼ ▼ FORMAL_EXACT QUANT_EXACT CODE_CHECK logiclab/Z3 probkit code-check │ ▼ structured semantic extraction │ ▼ symbolic formalization │ ▼ formalization validation │ ▼ Z3 solve / optimize / check │ ├── SAT ─────▶ model / witness validation ├── UNSAT ───▶ contradiction / optional unsat core └── UNKNOWN ─▶ abstain or alternate method │ ▼ natural-language answer reconstruction │ ▼ trace + metrics + failure memory ``` The architecture should make five task classes explicit. ## 8.1 `FORMAL_EXACT` Use when the problem can be represented faithfully as Boolean, finite-domain, arithmetic, ordering, set, scheduling, or other supported constraints. Examples: - logic-grid puzzle; - employee assignment constraints; - exact scheduling feasibility; - rule entailment; - satisfiability; - mutually exclusive configuration requirements. ## 8.2 `QUANT_EXACT` Use for probability, statistics, odds, expected values, distributions, or other quantitative operations already covered by `probkit`. ## 8.3 `CODE_CHECK` Use for deterministic syntax, lint, parse, schema, or similar code checks. ## 8.4 `SEMANTIC_OPEN` Use normal language-model reasoning where a complete symbolic model would be artificial or misleading. Examples: - “Which business strategy is better?” - “Does this argument rely on an unstated assumption?” - “What are the tradeoffs in this architecture?” ## 8.5 `HYBRID` Use when part of the task is semantic and part exact. Example: > “Given these staffing requirements and employee restrictions, propose a sensible schedule that minimizes split shifts.” The model interprets soft preferences, while the formal engine enforces hard constraints and can optimize a formal objective. --- # 9. A Deterministic Routing Policy The reviewer’s main failure was not that Z3 was unavailable. It was that no active rule made Piper use it. The routing policy should be short enough to be deterministic. ## 9.1 Candidate triggers Mark a task as potentially `FORMAL_EXACT` when it contains one or more of: - explicit if/then rules; - all/none/some/exactly/at least/at most; - mutually exclusive alternatives; - fixed domains and assignments; - ordering or precedence; - schedules with hard availability constraints; - “is this possible?”; - “does this follow?”; - “which arrangement satisfies all rules?”; - contradiction / consistency / satisfiability; - finite puzzle structure; - exact combinatorial restrictions. This list is not a final classifier; it is a cheap candidate detector. ## 9.2 Escalation by consequence A second rule should capture consequential work even when lexical triggers are weak: > If Piper is about to act on a claim that depends on a finite set of exact constraints, attempt formalization before acting. For example, real staff scheduling is not a “puzzle,” but it is solver-shaped. ## 9.3 Do not force symbolic solving Routing to Z3 should require a representability check: \[ R = f(\text{formal structure}, \text{constraint explicitness}, \text{domain closure}, \text{consequence}) \] A problem with vague predicates such as “reasonable,” “fair,” “good,” or “similar” may need semantic interpretation before it can be formalized. If the interpretation would invent constraints not present in the request, Piper should not pretend the solver makes the result objective. --- # 10. The Formalization Contract `logiclab` should not accept an opaque block of solver code as the only artifact. It should accept or emit a structured contract. A useful conceptual schema is: ```yaml problem_id: task_class: entities: variables: domains: constraints: - id: source_span: normalized_meaning: formal_expression: assumptions: objective: query: expected_output: solver: timeout_ms: ``` The key field is `source_span`. Every formal constraint should be traceable back to the words that justified it. This gives Piper a lightweight evidence lineage: \[ \text{text span} \rightarrow \text{normalized proposition} \rightarrow \text{formal constraint} \] If the answer is wrong, the trace makes it possible to distinguish: - bad routing; - missed premise; - incorrect semantic interpretation; - incorrect symbolic translation; - solver error; - answer reconstruction error. Without this separation, all failures collapse into “logic got it wrong.” --- # 11. Formalization Validation Formalization is the dominant risk. Piper therefore needs checks *before* trusting solver output. ## 11.1 Parse and type validation The easiest layer: - expression parses; - all variables declared; - sorts/types are consistent; - no undefined symbols; - no accidental integer/real mismatch; - expected constraints are present. ## 11.2 Constraint-count sanity For generated or structured tasks, compare extracted constraints to expected source units. If a problem contains 11 numbered rules and only 8 reach the solver, that is a warning. This is not sufficient—one sentence can contain multiple constraints—but it catches silent omissions cheaply. ## 11.3 Round-trip paraphrase After formalization, have a separate step reconstruct each formal rule in plain language. Compare: ```text source: "Bob cannot work before Alice." formal: bob_time > alice_time round-trip: "Bob's time is later than Alice's." ``` A mismatch does not automatically prove failure, but it is a useful semantic alarm. The round-trip step should not be the sole validator because the same model may reproduce its own misconception. It is a filter, not a guarantee. ## 11.4 Generated witness tests Where possible, test the formalization against examples. If the statement says “exactly one of A, B, C,” evaluate several assignments: - A only → should pass; - B only → should pass; - A and B → should fail; - none → should fail. For many logical constructs, these truth-table-style microtests are cheap. ## 11.5 Mutation tests Deliberately mutate the formalization: - flip `<` to `<=`; - remove `Not`; - change `And` to `Or`; - change exactly-one to at-least-one; - remove one premise. If the benchmark oracle cannot distinguish the mutation, the test may be too weak. For production tasks, mutations can be used selectively on consequential constraints. ## 11.6 Model/witness replay For SAT results, retrieve the satisfying model and independently evaluate all encoded constraints under that model. This catches bugs in result extraction and some wrapper failures. ## 11.7 Contradiction diagnostics For UNSAT results, label constraints so an unsat core can be requested where useful. The user does not always need the core, but Piper can use it to explain which rules conflict. --- # 12. Result Semantics Piper should not reduce every solver call to a single Boolean. The minimum result vocabulary should be: - `SAT` - `UNSAT` - `ENTAILED` - `CONTRADICTED` - `BOTH_POSSIBLE` / `UNDERDETERMINED` - `OPTIMUM_FOUND` - `UNKNOWN` - `TIMEOUT` - `FORMALIZATION_FAILED` These statuses should remain distinct through the answer layer. ## 12.1 Why `UNKNOWN` matters A solver saying `unknown` is not a license for Piper to silently manufacture an answer. The correct response is to: 1. inspect the reason; 2. try an allowed alternate encoding/solver path if configured; 3. otherwise report that exact resolution failed. Abstention is a successful behavior when the formal path cannot establish an answer. --- # 13. Answer Reconstruction A subtle failure mode occurs *after* the solver. Suppose Z3 finds: ```text Alice = Tuesday Bob = Wednesday Cara = Monday ``` Piper can still mistranscribe or embellish the result. The final answer should therefore be constructed from structured solver output rather than from memory of the reasoning. For exact tasks: > “The satisfying assignment is: Cara Monday, Alice Tuesday, Bob Wednesday.” Then optionally explain the binding constraints. Do not ask the model to recreate the schedule from a prose summary of the solver result. --- # 14. Proposed Benchmark: `LOGIC-v1` ## 14.1 Goal Measure whether Piper can: 1. notice that exact formal reasoning is appropriate; 2. choose the correct exact instrument; 3. preserve the meaning of the problem in a formal representation; 4. obtain the correct formal result; 5. correctly report that result; 6. avoid claiming exactness when formalization is unsupported. The benchmark should score **behavior**, not installed packages. --- # 15. `LOGIC-v1` Test Tracks A practical first frozen suite is **420 sealed items**, mostly machine-generated. The exact count can be changed before freezing; the important part is the track structure. ## Track A — Routing discrimination: 80 items Balanced examples from: - formal logic / Z3; - probability / `probkit`; - code checking / `code-check`; - ordinary semantic reasoning; - hybrid tasks. ### Measure - correct route; - unnecessary solver calls; - missed solver calls; - inappropriate inline arithmetic; - inappropriate free-form logical solving. ### Why it matters This directly tests the reviewer’s observed gap. A solver that is never invoked contributes nothing to cognition. --- ## Track B — Natural language → formal representation: 80 items Use generated formal worlds rendered into multiple natural-language paraphrases. Examples include: - exactly one; - at most one; - implication; - biconditional; - exclusion; - ordering; - finite quantification; - integer bounds; - membership; - all-different constraints. Each item has a hidden canonical semantics. ### Scoring Do not compare source code strings. Compare semantics. Possible methods: - equivalence under exhaustive finite assignments; - solver equivalence checks; - mutation tests; - canonical truth conditions. ### Primary failure classes - omitted rule; - reversed implication; - quantifier error; - negation error; - scope error; - equality vs inequality; - exactly vs at-least; - temporal/order reversal; - entity binding error; - invented assumption. --- ## Track C — Deduction and rule chains: 80 items Draw from the ProofWriter/PrOntoQA style: - fact sets; - implication rules; - negated facts; - multi-hop chains; - distractor rules; - contradictory branches where explicitly defined. Control proof depth: - depth 1; - depth 2–3; - depth 4–6; - depth 7+. ### Required output - entailed; - contradicted; - unknown/underdetermined. ### Important design point Include examples where the conclusion is *not* provable but sounds plausible. This tests whether Piper imports world knowledge that is absent from the formal world. --- ## Track D — CSP, logic grid, Latin square, and scheduling: 80 items Machine-generate finite constraint problems with known solutions. Vary: - domain size; - number of variables; - constraint density; - distractor wording; - unique vs multiple solutions; - SAT vs UNSAT; - optimization objective present/absent. ### Measures - correct route to solver; - valid solution; - complete satisfaction of constraints; - detection of multiple valid solutions; - correct declaration of unsatisfiable instances; - latency and solver cost. ### Complexity ladder Difficulty should be measured structurally rather than by prompt length alone: \[ C = \alpha |V| + \beta |D| + \gamma |K| + \delta B + \epsilon S \] where: - \(V\) = variables; - \(D\) = effective domain size; - \(K\) = constraints; - \(B\) = branching/search complexity proxy; - \(S\) = semantic/paraphrase difficulty. This allows testing the point at which LLM-only solving collapses while solver-backed performance remains stable. --- ## Track E — Satisfiability, contradiction, and adversarial formalization: 50 items Include: - subtly inconsistent rules; - redundant rules; - irrelevant distractors; - near-duplicate entities; - double negatives; - implication reversal traps; - vacuous truth cases; - “unless” and exclusive-or language; - multiple possible models; - insufficient information. ### Why this track is separate A model can often solve easy puzzles while still mishandling logical status. Logic requires distinguishing: > “I found one valid model” from > “this is the only possible model” and > “the conclusion is entailed by every valid model.” --- ## Track F — Boundary and tool-selection cases: 50 items These are deliberately adjacent to logic. Examples: - probability question → `probkit`; - arithmetic → deterministic calculator/probkit as configured; - causal intervention → causal subsystem; - open-ended policy tradeoff → semantic reasoning; - planning problem with a constraint-solving subproblem → hybrid route; - code syntax issue → `code-check`; - ambiguous natural-language rule → request interpretation internally or expose ambiguity rather than formalize silently. ### Purpose A good Logic system knows when *not* to use Logic. --- # 16. Scoring The primary formal Logic score should not be a simple accuracy average. Recommended component score: \[ S_{\text{logic}} = 0.50C + 0.20R + 0.20F + 0.10H \] where: - \(C\) = final formal correctness; - \(R\) = routing correctness; - \(F\) = formalization fidelity; - \(H\) = handling of ambiguity, unknown, timeout, and unsupported cases. Probability correctness is reported separately. ## 16.1 Hard floor A component should not receive a high Logic score if routing is poor. Suggested gate: > If formal-task solver-routing recall is below 80%, cap the component score at 60/100. Reason: Piper cannot claim solver-backed logic if she frequently bypasses the solver. ## 16.2 Catastrophic-error penalty Wrong confident answers on consequential exact tasks should be more expensive than abstention. For benchmark scoring: - correct exact answer: +1 - correct abstention where formalization is impossible: +1 - unnecessary abstention on supported item: 0 - wrong answer: −1 - wrong answer after claiming deterministic verification: −2 The last category matters. “Verified” should carry a stricter contract than ordinary reasoning. --- # 17. Diagnostic Scores Report at least: | Metric | Meaning | |---|---| | route precision | when Piper invokes Z3, was Z3 appropriate? | | route recall | when Z3 was appropriate, did Piper invoke it? | | formalization semantic accuracy | did the symbolic representation preserve the problem? | | solve correctness | was solver output used correctly? | | reconstruction accuracy | did final prose match structured result? | | abstention accuracy | did Piper stop when exact resolution was unavailable? | | SAT accuracy | correct satisfiable classifications | | UNSAT accuracy | correct unsatisfiable classifications | | entailment accuracy | correct universal consequence | | underdetermined accuracy | correctly recognized multiple possibilities | | verified-wrong rate | wrong answers carrying a “verified” status | | solver latency | end-to-end exact path | | solver timeout rate | time/resource failure | | repair success rate | malformed formalizations repaired successfully | The **verified-wrong rate** should be treated as a critical safety metric and targeted toward zero. --- # 18. Baselines and Experimental Arms Before adding routing, freeze a baseline. ## Arm 0 — Current Piper No new rule. Give the sealed tasks through the normal system. Measures actual present behavior. ## Arm 1 — Model-only Explicitly disable exact tools. This estimates the base LLM’s own logical ability. ## Arm 2 — Oracle routing + Z3 A test harness tells Piper exactly which items belong to Z3. This removes routing as a failure source and measures formalization + solver integration. ## Arm 3 — Logic Gate + Z3 Full proposed architecture. This is the target production system. ## Arm 4 — Oracle formalization + Z3 Provide the correct formal representation directly to the solver. This is the solver ceiling. The five-arm decomposition is extremely useful: \[ \text{Total error} = E_\text{routing} + E_\text{formalization} + E_\text{solver integration} + E_\text{reconstruction} \] The terms are not perfectly additive in practice, but the experimental arms let Piper estimate where the real loss occurs. --- # 19. Expected Initial Result The current audit predicts a specific pattern: - `probkit`: strong live usage; - `code-check`: strong live usage; - formal solver-routing recall: near zero in natural work; - model-only logic: nonzero but unknown; - Z3 ceiling: near perfect on supported generated formal tasks; - largest new gain: routing plus formalization discipline. This is testable. The current status should therefore remain: > **Logic — unmeasured, with exact solver infrastructure present but not operationally integrated.** Do not label the component “good” merely because Z3 is installed. --- # 20. Anti-Gaming and Leakage Controls Because most tasks can be generated cheaply, `LOGIC-v1` should be difficult for Piper to memorize. ## 20.1 Seal generators, not just instances If Piper knows every generation template, she can learn superficial lexical cues. Hold out: - templates; - paraphrase families; - entity vocabularies; - constraint combinations; - proof-depth distributions. ## 20.2 Separate training/dev from sealed evaluation Piper may inspect and improve against a public/dev generator. Final score comes from a separately seeded sealed generator. ## 20.3 Paraphrase variation The same semantics should appear in varied forms: - “A must happen before B.” - “B cannot precede A.” - “A is earlier than B.” - “By the time B occurs, A must already have occurred.” This tests semantic extraction rather than phrase matching. ## 20.4 Distractor facts Include irrelevant but plausible statements. ## 20.5 Counterbalanced labels Avoid correlations such as: - longer prompts are more often UNSAT; - “not” implies false; - scheduling tasks always have one solution; - solver-shaped wording always means Z3. ## 20.6 No self-scoring Piper should not determine whether its own formal answer is correct from prose. Ground truth must come from benchmark generation or an independent exact evaluator. --- # 21. Live-Use Measurement Benchmarks answer “can Piper do it under test?” The reviewer also identified the more important question: > Does she actually use it? Add a rolling seven-day live-use panel. ## 21.1 Counters - number of candidate formal tasks detected; - number routed to `logiclab`; - number solved SAT; - number solved UNSAT; - number returned UNKNOWN; - number of formalization failures; - number of repair attempts; - number of successful repairs; - number of solver-backed answers acted upon; - number of probable solver opportunities answered without solver; - `probkit` calls; - `code-check` calls. ## 21.2 Sample-based audit A nightly or weekly reviewer can sample real turns and label: - solver warranted; - solver optional; - solver inappropriate. Compare this to actual calls. This produces real-world routing precision/recall. ## 21.3 Important principle Do not optimize for solver call count. The target is not “more Z3.” The target is “Z3 whenever exact formal structure makes it the safer method.” --- # 22. Logging Schema Every `logiclab` execution should leave a durable record such as: ```json { "task_id": "...", "timestamp": "...", "route": "FORMAL_EXACT", "router_reason": ["ordering_constraints", "finite_assignment"], "formalizer_model": "...", "solver_name": "z3", "solver_version": "...", "logic_fragment": "...", "source_constraint_count": 9, "formal_constraint_count": 9, "validation": { "parse_ok": true, "type_ok": true, "roundtrip_ok": true, "witness_checks": 6, "witness_failures": 0 }, "result": "SAT", "repair_attempts": 0, "latency_ms": 31, "answer_reconstruction_check": true } ``` This makes the cognition inspectable. --- # 23. Failure Taxonomy The benchmark should classify failures, not merely record wrong answers. ## L1 — Missed formal structure Piper should have used a solver but answered directly. ## L2 — Wrong tool Piper routed probability to Z3, formal constraints to `probkit`, or an open semantic question to an exact tool. ## L3 — Entity extraction failure An actor, option, variable, or domain member was omitted or conflated. ## L4 — Constraint omission A premise never reached the formal representation. ## L5 — Semantic reversal Common examples: - before/after; - if/only if; - all/some; - at-most/at-least; - allowed/required; - inclusive/exclusive OR. ## L6 — Scope or quantifier error A local rule becomes global, or vice versa. ## L7 — Invented assumption The formalizer adds a restriction the user never supplied. ## L8 — Unsupported formalization The system forces vague semantics into rigid symbols without acknowledging ambiguity. ## L9 — Solver misuse Wrong theory, incorrect optimization direction, broken API call, inappropriate timeout, or misunderstood solver status. ## L10 — Result reconstruction error The solver output is correct but Piper reports something else. ## L11 — Exactness laundering Piper labels an answer “verified” even though only part of the task was formally verified. ## L12 — Failure to abstain Formalization or solving failed, but Piper produced a definite answer anyway. These labels should become regression categories. --- # 24. Repair Loop A bounded repair loop is justified because many formalization failures are mechanical. ```text formalize │ ▼ parse/type check ──fail──▶ diagnostic │ │ pass repair │ │ ▼ └───────┐ solve │ │ │ ├── malformed/unsupported ────────┘ │ ├── SAT ─▶ witness check ├── UNSAT ─▶ contradiction checks └── UNKNOWN ─▶ alternate encoding or stop ``` Recommended cap for v1: - maximum 2 repair attempts for syntax/type failures; - maximum 1 semantic re-formalization after validation mismatch; - then stop and record `FORMALIZATION_FAILED`. Unlimited self-repair invites loops and makes latency unpredictable. --- # 25. Using Z3 as Critic, Not Only Solver Piper’s broader cognition program benefits when exact systems attack proposed answers. Suppose the planner generates a staffing schedule. Instead of asking Z3 to create the schedule from scratch, Piper can assert: 1. all real constraints; 2. the proposed schedule as fixed assignments. Then ask whether the combined system is SAT. If UNSAT, the schedule is invalid. This pattern generalizes: > generative subsystem proposes → exact subsystem attacks. This is often more valuable than replacing generation entirely. Potential consumers include: - Planning; - Transfer; - code synthesis; - scheduling; - resource allocation; - configuration; - policy/rule compliance. --- # 26. Optimization Some tasks ask for more than feasibility: - minimize total overtime; - minimize number of split shifts; - maximize coverage; - minimize travel; - maximize preference satisfaction. Z3 supports optimization over formal constraints, but Piper must distinguish: 1. **hard constraints** — may never be violated; 2. **soft preferences** — objective terms; 3. **weights/priorities** — must come from explicit policy or user instruction. The LLM must not silently convert a vague preference into a hard rule. A good internal representation is: ```text HARD: every shift has >= 2 qualified workers no overlapping assignments employee availability respected SOFT: minimize overtime prefer consecutive shifts OBJECTIVE ORDER: 1. feasibility 2. overtime 3. split shifts ``` --- # 27. Ambiguity Handling Formal systems force precision, which is an advantage only when the source is precise enough. Example: > “Alice normally works before Bob.” Does “normally” mean: - a hard rule; - a preference; - a probabilistic tendency; - background information? Piper should not choose silently. For internal tasks, it can branch: ```text Interpretation A: hard ordering constraint Interpretation B: soft preference ``` Then determine whether the answer changes. If both interpretations yield the same conclusion, ambiguity may be harmless. If they diverge, Piper should expose or resolve it before acting. This yields a useful concept: \[ \text{ambiguity sensitivity} = P(\text{decision changes across plausible formalizations}) \] High-sensitivity ambiguity deserves attention. --- # 28. Confidence The solver’s confidence and the formalizer’s confidence must not be merged. For supported decidable cases: - solver confidence in the formal result may effectively be treated as exact; - confidence that the *formalization matches the user’s meaning* is a separate quantity. A useful answer record therefore has: ```text formalization_confidence: 0.83 solver_status: SAT verification_status: witness_checked ``` Do not report “100% confidence” merely because Z3 returned SAT. The uncertainty lives upstream. --- # 29. Relationship to Piper’s Other Cognitive Components Logic should become a service used by other cognitive organs. ## Attention Attention decides that exact constraints matter enough to inspect. ## Memory Memory supplies current facts and must avoid stale premises entering the formal world. ## Planning Planning proposes action sequences; Logic checks feasibility and constrained subproblems. ## Causal reasoning Causal reasoning supplies causal structure; Logic can verify algebraic or structural constraints but does not substitute for causal semantics. ## Counterfactual reasoning Counterfactual machinery may use formal constraints after an intervention but owns the intervention semantics. ## Error detection Logic can prove that two state claims conflict. ## Uncertainty Uncertainty should distinguish formal certainty conditional on premises from uncertainty about premises and formalization. ## Transfer A logic pattern learned in one domain can be reused elsewhere if the structural constraints are the same. This is another reason not to bury Z3 inside a “puzzle lab.” It should be a reusable exact-reasoning service. --- # 30. Minimum Engineering Changes The first implementation should be small. ## Phase 0 — Instrument truth 1. Have `logiclab` report actual Z3 runtime version. 2. Add durable call logging. 3. Count seven-day usage. 4. Add task/result/status fields. 5. Verify that calls are visible to the audit system. No behavioral claim should be changed yet. ## Phase 1 — Routing rule Add the Logic Gate with explicit task classes: - `FORMAL_EXACT` - `QUANT_EXACT` - `CODE_CHECK` - `SEMANTIC_OPEN` - `HYBRID` The route decision should be logged before execution. ## Phase 2 — Structured formalization Require: - entities; - domains; - constraints; - source links; - query; - assumptions. Do not accept solver code without an associated constraint map for benchmarked tasks. ## Phase 3 — Validation Add: - parse/type check; - source/constraint count sanity; - witness replay; - simple formalization round-trip; - explicit `UNKNOWN` and failure handling. ## Phase 4 — Repair Implement bounded solver-guided repair. ## Phase 5 — Benchmark Freeze `LOGIC-v1`, run all baseline arms, and record the first real score. ## Phase 6 — Live-use audit Measure real solver-routing precision and recall weekly. --- # 31. Acceptance Criteria for Logic v1 Piper should not promote Logic from “unmeasured” merely because the benchmark exists. Suggested initial acceptance bar: ### Formal benchmark - final correctness: ≥ 90% on supported sealed formal tasks; - Z3-route recall: ≥ 90%; - Z3-route precision: ≥ 90%; - semantic formalization accuracy: ≥ 90%; - verified-wrong rate: < 1%; - unsupported/ambiguous cases handled correctly: ≥ 90%. ### Live behavior Over a rolling seven-day audit: - at least 90% of high-confidence solver-shaped sampled tasks route through `logiclab`; - no repeated class of solver-opportunity miss after a known regression has been fixed; - “verified” label never appears without a recorded verification path. These are starting thresholds, not final targets. --- # 32. Benchmark Retirement and Progression Following the rest of Piper’s cognition program, the benchmark should not become a permanent memorized obstacle. When Piper beats the frozen baseline by the chosen retirement margin across repeated sealed runs, retire or harden the suite. A progression could be: ## `LOGIC-v1` - clean formal tasks; - moderate paraphrase; - finite domains; - short-to-medium rule chains. ## `LOGIC-v2` - stronger ambiguity; - longer documents; - conflicting natural-language descriptions; - multiple equivalent formalizations; - mixed hard/soft constraints; - partial observability. ## `LOGIC-v3` - formal reasoning embedded inside real agent work; - stale premises; - tool failures; - solver timeouts; - adversarial distractors; - requirements distributed across files/messages; - optimization with policy constraints. The long-term target is not puzzle solving. It is exact reasoning inside messy agentic work. --- # 33. Ablations Ablation is necessary to prove which part provides the gain. Run the following variants: 1. full Logic Gate; 2. no router — model chooses ad hoc; 3. router + Z3, no formalization validation; 4. router + Z3, no repair loop; 5. router + Z3, no witness/result check; 6. LLM-only; 7. forced Z3 on every task; 8. oracle routing; 9. oracle formalization. The expected result is informative: - LLM-only should degrade with combinatorial complexity; - forced-Z3 should fail on inappropriate/ambiguous semantic tasks; - no-validation should expose silent mistranslations; - oracle routing should show how much loss comes from detection; - oracle formalization should approximate the exact-system ceiling. If the full architecture does not beat the simpler variants, remove the extra machinery. --- # 34. A Stronger Research Question The component can be summarized by one falsifiable question: > **Does a gated neuro-symbolic architecture—where Piper detects formal structure, formalizes natural language, validates that formalization, and delegates inference to Z3—produce higher exact correctness and lower confidently-wrong rates than Piper’s native reasoning, without over-routing non-formal tasks?** This is much stronger than: > “Can Piper solve logic puzzles?” It tests the cognitive architecture, not just the model. --- # 35. Recommended First Experiment A compact experiment can establish whether the design is worth building fully. ## Dataset 200 sealed items: - 40 routing; - 40 rule-chain deduction; - 40 CSP/scheduling; - 40 formalization traps; - 40 boundary/non-Z3 items. ## Arms - Current Piper; - Current Piper + explicit “use Z3 when useful” instruction; - Logic Gate + structured formalization + Z3; - oracle formalization + Z3. ## Primary outcomes - exact answer accuracy; - route precision/recall; - verified-wrong rate; - semantic formalization accuracy; - latency; - tokens/cost. ## Decision rule Keep the Logic Gate if it materially improves exact correctness and reduces confident wrong answers without causing an unacceptable false-positive solver-routing rate. This small experiment can precede the full 420-item suite. --- # 36. What I Would Change in Piper’s Current Self-Description The current description overstates behavior. A replacement should describe the architecture and the measured state separately. ## Proposed post-implementation description > **Logic** > > Formal or rule-bound problems are routed through an exact-tool gate rather than solved from prose when a faithful symbolic representation is available. Finite constraints, satisfiability, scheduling feasibility, and rule entailment go through `logiclab` and Z3; probability and statistics go through `probkit`; deterministic code checks go through `code-check`. For solver-shaped problems I first build a traceable constraint representation, validate it, and then use the solver result rather than my own search. The main residual risk is semantic: a solver can be perfectly right about a problem I formalized incorrectly, so formalization fidelity is scored separately from solver correctness. > > **Measured state:** [insert `LOGIC-v1` score after baseline]. > **Live use:** [insert seven-day routing precision/recall and call counts]. Before the router is implemented and measured, the more accurate current wording is: > Exact logic machinery exists, but automatic routing to it is not yet established. `probkit` and `code-check` are used in practice; solver-backed formal logic remains unmeasured. --- # 37. Engineering Principle The most important principle for this component is: > **Do not make the LLM better at being a theorem prover when Piper already owns a theorem prover. Make Piper better at knowing when to use it, telling it the right problem, and checking that the answer still refers to the original problem.** That is the cognitive upgrade. The solver already knows how to search. The missing cognition is: - recognition; - representation; - delegation; - verification; - restraint. --- # 38. Final Recommendation Component 6 should be rebuilt conceptually around **solver-gated exact reasoning**, not around “logic puzzle ability.” The present architecture has three useful deterministic organs, but only two are visibly operational in real work. The Z3 path should be elevated from an occasional puzzle-lab utility into a first-class exact-reasoning service with an explicit router. The recommended order is: 1. fix instrumentation and runtime version reporting; 2. implement the Logic Gate; 3. require traceable structured formalization; 4. add semantic checks and bounded repair; 5. freeze and run `LOGIC-v1`; 6. measure live routing separately from benchmark competence; 7. use Z3 as a critic for other Piper components; 8. keep probability and code-check metrics visible but outside the core formal Logic score. The key expected finding is that Piper’s main weakness will not be Z3 itself. It will be the semantic boundary immediately before Z3: recognizing formal structure and encoding the intended meaning without omission, reversal, or invented assumptions. That is exactly where the benchmark should concentrate. --- # 39. Proposed Dashboard Entry ```text 6 Logic Applying formal or rule-based relationships. Latest — not scored Baseline — pending LOGIC-v1 Live use — formal solver routing not yet established Piper — what it is Logic is solver-gated exact reasoning. When a task can be faithfully expressed as formal constraints, I should not search for the answer in prose: I map the entities and rules into a traceable formal representation, validate that representation, and send it to logiclab/Z3. Probability and statistics route to probkit instead, and deterministic code checks route to code-check. The solver owns the consequences of the formal model; I own the dangerous part, which is deciding what the words mean and whether the formal model actually matches them. Piper — the parts that do it logic-gate [proposed] logiclab v1.0 Z3 [runtime version logged automatically] probkit v0.2.0 code-check v1.0.1 Reviewer Claude, 2026-09-30 Good for probability, absent for formal logic in live behavior. The installed solver architecture is sensible, but no active routing policy was causing normal work to reach it. Test suite LOGIC-v1: sealed routing, formalization, rule-chain, entailment, CSP, scheduling, satisfiability, ambiguity and boundary cases. Score exact correctness, solver routing, formalization fidelity, and correct handling of unknown/unsupported cases. Track probability separately. Live-use audit measures whether solver-shaped real work actually reaches logiclab. ``` --- # References 1. Ye, X., Chen, Q., Dillig, I., & Durrett, G. **SatLM: Satisfiability-Aided Language Models Using Declarative Prompting.** arXiv:2305.09656, 2023. 2. Pan, L., Albalak, A., Wang, X., & Wang, W. Y. **Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning.** arXiv:2305.12295, 2023. 3. Olausson, T. X., Gu, A., Lipkin, B., Zhang, C. E., Solar-Lezama, A., Tenenbaum, J. B., & Levy, R. **LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers.** arXiv:2310.15164, 2023. 4. Poesia, G., Gandhi, K., Zelikman, E., & Goodman, N. D. **Certified Deductive Reasoning with Language Models.** arXiv:2306.04031, 2023. 5. Tafjord, O., Dalvi Mishra, B., & Clark, P. **ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language.** arXiv:2012.13048, 2020. 6. Han, S. et al. **FOLIO: Natural Language Reasoning with First-Order Logic.** arXiv:2209.00840, 2022. 7. Lin, B. Y., Le Bras, R., Richardson, K., Sabharwal, A., Poovendran, R., Clark, P., & Choi, Y. **ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning.** arXiv:2502.01100, 2025. 8. Prasetya, I. S. W. B., Kifetew, F., & Prandi, D. **Talk is Cheap, Logic is Hard: Benchmarking LLMs on Post-Condition Formalization.** arXiv:2603.17193, 2026. 9. Huang, S., Jiang, Z., Jiang, Y., Wu, L.-I., Li, J., & Li, G. **Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis.** arXiv:2607.19795, 2026. 10. Barrett, C., Fontaine, P., & Tinelli, C. **The SMT-LIB Standard, Version 2.7.** SMT-LIB Initiative, 2026. 11. de Moura, L., & Bjørner, N. **Z3: An Efficient SMT Solver.** Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. 12. Z3 Project. **Z3 5.1.0 release.** August 2026. --- ## One-line thesis **Piper’s Logic component should not be “an LLM that reasons more carefully”; it should be a measured semantic front-end that knows when to hand exact structure to a solver, proves that it handed over the right structure, and refuses to call the result verified unless the entire path is traceable.**