Mech Reasoner

Mech Reasoner is a benchmark toolkit for qualitative mechanistic reasoning. It validates electrical, mechanical, and thermal mechanism catalogs; generates open-answer JSON tasks; evaluates structured model answers; and plots accuracy by task complexity.

The benchmark includes necessity, plausibility, state_consistency, transition, functional_recovery, and trace_faithfulness. Generated tasks are divided into four complexity levels (D1 through D4) using each task family's declared leveling protocol. All generation requires simulation-validated artifacts in the current strict catalog schema. The transition family supplies one complete initial episode and an exact successor horizon, then asks for every distinct component-state transition witnessed by an episode-graph edge whose source depth is below that horizon. Its complexity is C_H = sum_{depth(v) < H} B(v) D(v): boundary causes times declared outgoing component transitions at every expanded source. Difficulty is assigned only from this raw scalar using frozen, task-family-global bands: D1 is C_H < 7, D2 is 7 <= C_H < 16, D3 is 16 <= C_H < 70, and D4 is C_H >= 70. These cutpoints freeze the workload thresholds calibrated from the v1.0.0 transition candidate census; evaluator outcomes do not participate in task assignment. Generation remains capped at horizon two to avoid expensive deep expansion and the observed horizon-three saturation effect. There is no synthetic graph, declared-transition fallback, or within-mechanism relabeling. A mechanism-band cell is emitted only when the requested quota (four in the production protocol) has exact nonempty support; four deterministic order-only prompt variants cannot fill the quota, and unsupported cells remain empty. Per-catalog benchmark cells never borrow tasks from another mechanism.

The necessity family is the universal dual over the same exact episode semantics. Given one complete initial episode and horizon H, each claim asks whether three facts about an in-scope edge's source force a disjunction of two facts about its target. N means every admissible edge whose source depth is below H satisfies the implication; U requires one exact counterexample edge. Generated claims have witnessed antecedents, ambiguous target variables, and no single-disjunct shortcut. Every unnecessary claim has exactly one exact counterexample edge, preventing larger graphs from making existential violations easier through redundant witnesses. Its source is always in the deepest expanded layer (H-1), and every necessary claim also matches at least one edge from that layer, preventing root-local shortcuts. Their fixed 32-claim surface is leveled by 32 |E_H| + |V_H| + |C_H|, the exact edge-claim product plus reachable episode and cause bookkeeping.

The plausibility family is bounded existential model checking over complete episode histories. Each task supplies one complete initial episode and 32 candidate narratives. A narrative is plausible only when one exact path of length H jointly satisfies all checkpoint observations; facts and checkpoints within a narrative cannot use independent interpretation witnesses. The fixed 16-plausible/16-implausible answer surface reports observation load L = sum_{t=1}^H |O_t|: the number of checkpoint facts that must be maintained jointly along one candidate narrative. Exact path and fact-membership work is retained as diagnostic metadata rather than folded into the primary metric. One-step negatives are projection traps. At deeper horizons the generator prefers path-switch traps whose checkpoints are all locally supported but have no shared path.

Plausibility discovery uses one cumulative mechanism/cell work protocol. (family, mechanism, horizon) ledgers charge exact relation pairs, paired decision states, and paired branches once; H1 is shared by D1-D2, H2 adds D3, and H3 adds D4. Separate (family, mechanism, D-level) ledgers bound unique candidate-construction attempts. Root probes and both ledgers are checkpointed, so process restarts resume the same allowance rather than creating a renewable multi-pass budget. Wall-clock limits are watchdogs only: a timed-out catalog is incomplete until it resumes to a task quota or deterministic budget boundary. Worker count changes throughput but never the recorded allowance.

The repository is organized around:

• catalog/: mechanism definitions used to generate benchmark tasks.
• src/catalog_generation/: catalog schema and loading support.
• src/simulator/: qualitative sign solver.
• src/task_generation/: benchmark task generation.
• src/evaluation/: model evaluation.
• src/analysis/: aggregate tables and plots.
• benchmark/: versioned generated tasks, solutions, evaluation records, and plots.

Requirements

• Python 3.13 or newer.
• uv for dependency and environment management.
• Git LFS for versioned JSONL records, PNG assets, generated simulation traces, and oversized benchmark metadata.
• Docker and Modelica Standard Library 4.1.0 only for physical validation.

Installation

After cloning, initialize Git LFS and materialize every tracked large-file object before running analyses or building the paper:

git lfs install
git lfs pull
git lfs fsck

The repository's .gitattributes routes *.jsonl, *.png, catalog simulation trace CSVs, and the explicitly listed oversized JSON/YAML metadata files through Git LFS. git lfs fsck fails when a checkout contains a missing or corrupt object; plain-text LFS pointer files must not be used as benchmark records or figures.

Install dependencies with uv:

uv sync

Install development tools:

uv sync --group dev

Quickstart

Validate the mechanism catalog:

uv run python -m src.main validate-catalog --catalog-dir catalog

Generate the nominal benchmark target of 1,728 tasks (4 tasks × 18 mechanisms × 4 levels × 6 families):

uv run python -m src.main generate --catalog-dir catalog

Keep valid tasks from cells that cannot fill all four requested tasks:

uv run python -m src.main generate \
  --catalog-dir catalog \
  --output-dir benchmark/v1.0.2 \
  --benchmark-version v1.0.2 \
  --tasks-per-level 4 \
  --allow-partial-cells

Partial output never changes the candidate-selection scope or borrows tasks from another mechanism or difficulty.

Generation protocol and timeouts

The builder schedules 432 independent quota cells, one for each (task family, mechanism, difficulty level) tuple. It runs D1 across the catalog before D2, then D3 and D4, so later levels reuse the family candidate checkpoints populated by earlier levels. --jobs controls concurrent cell subprocesses; every family subprocess uses one internal worker, preventing nested process pools from oversubscribing the machine.

--timeout-seconds is a cumulative budget for each cell, not a family-wide or whole-benchmark deadline. Every cell stores its budget, consumed time, attempt count, and status in runs/<family>/<mechanism>/<level>/cell_state.json. Restarting generation reuses completed cells and does not renew an exhausted budget. A subprocess gets up to 30 seconds beyond its remaining generation budget to flush atomic checkpoints and output. Candidate checkpoints are shared per family, and all subprocesses use the same content-addressed simulator_cache root.

Optional JSON can override the default by family/D-level or by exact cell:

{
  "default": 180,
  "families": {
    "plausibility": {"D3": 300, "D4": 480},
    "transition": 360
  },
  "cells": {
    "plausibility/electrical_example/D4": 720
  }
}

uv run python -m src.main generate \
  --catalog-dir catalog \
  --timeout-seconds 180 \
  --timeout-config generation-timeouts.json \
  --jobs 4 \
  --allow-partial-cells

The aggregate task files and manifest are rebuilt after each D-level breadth round. Individual cell outputs remain the durable resume unit. To retry only timed-out or failed cells and grant each one more cumulative time:

uv run python -m src.main generate \
  --catalog-dir catalog \
  --retry-failed \
  --retry-timeout-extension-seconds 180

Unless an output option is supplied, commands use the versioned benchmark directory selected by DEFAULT_OUTPUT_VERSION in src/task_generation/build_benchmark.py.

Evaluate ten generated tasks with Azure OpenAI. Evaluation concurrency is 20 by default and should remain 20 for benchmark runs:

export AZURE_BASE_URL="https://<resource>.openai.azure.com"
export AZURE_KEY="<api-key>"
export DEPLOYMENT="<deployment-name>"

uv run python -m src.main evaluate \
  --evaluator azure \
  --model-profile gpt-5.5 \
  --concurrency 20 \
  --limit 10

Plot evaluation accuracy:

uv run python -m src.main plot

To generate, evaluate, and plot in one command:

uv run python -m src.main run --catalog-dir catalog --concurrency 20

Pass --task-family <name> to generate, evaluate, or plot one task family. To store generated tasks separately from evaluations and plots, use --task-output-dir and --analysis-output-dir:

uv run python -m src.main generate \
  --catalog-dir catalog \
  --task-output-dir task_outputs
uv run python -m src.main evaluate \
  --task-output-dir task_outputs \
  --analysis-output-dir analysis_outputs \
  --concurrency 20
uv run python -m src.main plot --analysis-output-dir analysis_outputs

Generation writes task JSON files, solutions.jsonl, manifest.json, and selection_summary.csv under benchmark/<version>/. Evaluation records are stored by model and task family under benchmark/<version>/analysis/evaluations/; plotting writes per-family CSV, LaTeX, and PNG summaries under the same analysis/ directory. Plotting validates every evaluation against the active task keys in solutions.jsonl and stops if the evaluation directory contains superseded, unknown, or duplicate records.

Prompt-only symbolic baseline

The deterministic non-oracle baseline reconstructs a symbolic problem from the rendered prompt and runs the exact qualitative solver. Its inference API accepts only the prompt string: it does not receive catalog objects, generator caches, task metadata, or gold answers. Run prediction and scoring as separate phases to preserve that boundary:

uv run python -m src.baselines.prompt_symbolic_cli predict \
  --task-output-dir benchmark/v1.0.0

uv run python -m src.baselines.prompt_symbolic_cli score \
  --task-output-dir benchmark/v1.0.0

predict reads only files below tasks/ and incrementally writes analysis/prompt_symbolic_baseline/predictions.jsonl. score subsequently opens solutions.jsonl, writes normal evaluation records under analysis/evaluations/, and produces analysis/prompt_symbolic_baseline/summary.json. The summary reports prompt parse success, solver success conditional on parsing, exact-match accuracy, runtime, and per-family breakdowns. Use the run command as a convenience when the two phases do not need to be launched separately, and use --retry-failures to revisit recorded parser or solver failures. Prediction is checkpointed after every prompt. --time-budget-seconds sets a process-isolated whole-prompt deadline, while --shard-count and --shard-index allow deterministic parallel shards. Failed checkpoints carry a hash of the inference configuration and are retried automatically after solver settings or the inference implementation changes.

This baseline measures how much of the benchmark can be solved by extracting the visible structured representation and performing exhaustive symbolic bookkeeping. It therefore separates representation parsing and exact execution from LLM-style free-form mechanistic inference. It is intentionally release-surface-specific; an unrecognized prompt grammar is recorded as a parse failure instead of consulting private benchmark state.

Modelica-derived exact gold reverification

The fail-closed Modelica MDD verifier binds every task to its validated catalog certificate, compiler-derived structural.json, pinned OpenModelica/MSL versions, exact-solver source hashes, rendered prompt hash, and canonical answer. Prediction reads only each task's content field and the validated catalog; it does not read solutions.jsonl, top-level task metrics, task-generation caches, or evaluation records:

uv run python -m src.verification.modelica_bdd_cli predict \
  --task-output-dir benchmark/v1.0.0 \
  --catalog-dir catalog

Freeze predictions before opening gold. The separate scoring phase requires the prediction and solution key sets to match exactly and writes per-task verdicts plus a release summary:

uv run python -m src.verification.modelica_bdd_cli score \
  --task-output-dir benchmark/v1.0.0

When a release already contains the complete frozen gold-blind prompt_symbolic_baseline/predictions.jsonl, its prior exact executions can be revalidated without rebuilding memory-intensive episode graphs:

uv run python -m src.verification.modelica_bdd_cli import \
  --task-output-dir benchmark/v1.0.0 \
  --catalog-dir catalog

Import verifies all task keys, public prompt hashes, solved statuses, mechanism identities, exact diagnostics, catalog/compiler bindings, and obligation counts before issuing revalidated_prior_exact_execution certificates. The summary reports fresh and imported execution provenance separately. Scoring streams the large solution JSONL one row at a time to keep memory bounded.

The exact finite backend uses reduced ordered multi-valued decision diagrams for intrastate relations and exact bounded episode relations for temporal families. It proves satisfiability/nonemptiness or emptiness within the released bounded qualitative semantics. Transition verification includes every declared candidate transition as an obligation, including candidates excluded from gold. Unsupported inputs, catalog hash failures, and exhausted budgets produce inconclusive; they never count as verified.

For parallel runs, write one predictions file per shard and merge only nonconflicting certificates:

uv run python -m src.verification.modelica_bdd_cli merge \
  --predictions benchmark/v1.0.0/analysis/modelica_bdd_verifier/predictions.jsonl \
  --prediction-input /path/to/shard-0.jsonl \
  --prediction-input /path/to/shard-1.jsonl

This is an independent gold-access path, not a clean-room reimplementation of the qualitative semantics: it shares the released exact solver. It therefore verifies that frozen labels follow from the public bounded semantics and Modelica-derived catalog snapshot. It does not prove that the qualitative abstraction is complete for every continuous trajectory of the source Modelica model.

Aggregate generation also enforces normalized-prompt question uniqueness. Prompt identity is the exact rendered content after removing the opaque Task id: line, with task family retained as a namespace. If two such prompts have the same gold answer, the lowest D-level and then lexicographically first task id is retained; different gold answers make assembly fail. The audit mapping and prompt hashes are written to semantic_deduplication.json. In v1.0.0 this removed 21 repeated necessity records from 1,146 generated task-id records, leaving 1,125 unique question instances. The paired historical model outputs are archived under analysis/repeated_inference/ and are excluded from scores.

Generation-time labels and analysis-time bins are intentionally distinct. Generated tasks retain their family-specific D1--D4 labels in complexity_level. Analysis derives a separate family-relative mechanistic complexity bin, B1--B4, from the persisted scalar metric and writes it as analysis_bin. In every task family, unique retained tasks are partitioned into deterministic near-equal-count bins without splitting equal-complexity ties. Analysis never treats a task's generation-time D-label as its analysis bin.

State-consistency uses an answer-independent constraint-check metric. For every candidate/case judgment it counts the active state restrictions, active confluences, and case restrictions: C = sum_{i,k}(L_i + R_i + A_k). State coordinates, signed terms, connected-variable width, and solver-probe counters are not stored. Generation-time D-level assignment is driven only by this raw metric, using frozen family-global half-open bands: D1 [0, 4096), D2 [4096, 8192), D3 [8192, 16384), and D4 [16384, infinity). Generation varies candidate-panel and case-set sizes to discover tasks in those bands. A mechanism-level band is emitted only when it contains the full requested quota of semantically distinct tasks; unsupported cells are recorded rather than filled with reordered or weakened variants. Persisted complexity values remain in these native metric units.

All evaluator providers use one capability-adaptive benchmark protocol: low reasoning effort when that control is supported, temperature zero when available, JSON mode when available, a 600s request timeout, and concurrency 20 by default. The output budget is 20,000 tokens or the evaluator's declared maximum, whichever is lower. No separate reasoning-token budget is sent. Eligible models must support at least 80,000 input tokens. Rate-limit responses wait and retry automatically; every other infrastructure failure is recorded and retried only when --retry-errors is passed explicitly.

If an Azure deployment has an arbitrary name, identify its backing model with --model-profile so its capabilities can be validated without changing the deployment name sent to Azure:

uv run python -m src.main evaluate \
  --evaluator azure \
  --model production-reasoner \
  --model-profile gpt-5.5

For transition calibration, generate at most one hardest exact task per eligible catalog mechanism, or exactly ten profiled tasks from each globally supported, strictly increasing opportunity-count interval:

uv run python -m src.task_generation.transition.generate \
  --catalog-dir catalog \
  --output-dir transition-hard \
  --selection-mode hard_distinct \
  --task-count 10

uv run python -m src.task_generation.transition.generate \
  --catalog-dir catalog \
  --output-dir transition-levels \
  --tasks-per-level 10 \
  --scenario-roots-per-catalog 40

Hard-distinct generation fails if the catalog cannot supply the requested number of different mechanisms. Pass --allow-shortfall only when an explicitly recorded, smaller capability sample is acceptable. Transition complexity is the number of (source episode, boundary cause, outgoing declared component-state transition) successor opportunities. The release generator uses frozen, family-global raw-metric bands D1 [0, 7), D2 [7, 16), D3 [16, 70), and D4 [70, infinity). A scenario's horizon or answer does not change its band. Within a band, D1--D2 prefer H1 and D3--D4 prefer H2 when the mechanism has enough support. Only exact scenarios with at least one admissible component-state transition are eligible for release tasks; four deterministic order-only prompt variants amortize each exact graph across one complete cell. Empty H1 scenarios remain only as root-local probes, and a time-bounded set of up to twice the per-cell task quota is promoted as H2 fallbacks when a mechanism has no witnessed H1 root. Unsupported mechanism/level cells remain empty. Release assembly emits either four tasks or zero tasks for each mechanism/level cell. absolute_metric_bands is the default selection mode.

Transition discovery is resumable. Each exact (catalog, initial-root, horizon) result is checkpointed as soon as it is known, and every partial mechanism snapshot is immediately assembly-readable. The benchmark builder performs a bounded multi-mechanism campaign, prioritizes mechanisms closest to completing another fixed-band cell, and stops when at least 100 complete-cell task slots are supported, or when three passes per mechanism have completed. Because a mechanism contributes at most 16 tasks, this target necessarily represents at least seven mechanisms without requiring every represented mechanism to support all four absolute bands. It then assembles all four D-level cells from each immutable mechanism snapshot, so D-level cells do not repeat simulation and later discoveries can backfill earlier cells. It uses benchmark/<version>/candidate_cache/transition automatically and preserves the append-only snapshots across ordinary retries; --force deliberately clears them. Cache keys cover the catalog, validation certificate, graph limits, generation code, and horizon. Wall-clock watchdog changes resume the same semantic search rather than invalidating completed work.

Before exact expansion, the generator cheaply ranks a bounded, deterministic 16-root batch by source-guard satisfaction and alignment between declared transition coordinates and nearest directed boundary events. It takes one root from every ready declared-transition obligation before repeated readiness/event strata. Exact H1 expansion is the positive-witness probe; only witnessed H1 roots are normally promoted to H2. Incomplete retries retain only unfinished roots, while completed batches advance to fresh deterministic roots. Transition episode expansion remains in memory and uses the root/horizon checkpoints instead of rewriting the shared whole-session episode cache. The shared simulator implementation and every other task-family generator are unchanged.

To replace only the v1.0.0 transition family in place, keep partial semantic cells and force only that family's run/cache state:

uv run python -m src.main generate \
  --task-family transition \
  --catalog-dir catalog \
  --output-dir benchmark/v1.0.0 \
  --benchmark-version v1.0.0 \
  --tasks-per-level 4 \
  --allow-partial-cells \
  --force

Family-targeted generation preserves every other task, solution, and run summary. Stale transition evaluations are moved under analysis/superseded_family_regeneration/, and the rebuilt manifest records the targeted replacement. Cells with one to three eligible scenarios are kept when --allow-partial-cells is set instead of discarding the entire cell.

Long discovery and fast deterministic assembly can also be run as separate phases. Both commands must use identical generation arguments:

uv run python -m src.task_generation.transition.generate \
  --catalog-dir catalog \
  --output-dir transition-discovery \
  --candidate-cache-dir transition-cache \
  --tasks-per-level 4 \
  --scenario-roots-per-catalog 40 \
  --max-horizon 2 \
  --time-budget-seconds 600 \
  --discovery-only

uv run python -m src.task_generation.transition.generate \
  --catalog-dir catalog \
  --output-dir transition-levels \
  --candidate-cache-dir transition-cache \
  --tasks-per-level 4 \
  --scenario-roots-per-catalog 40 \
  --max-horizon 2 \
  --time-budget-seconds 600 \
  --assembly-only

The checkpoint directory contains Python pickle files and must therefore be treated as trusted local build state, not as an externally supplied artifact.

Evaluation providers

Environment variables may be exported in the shell or placed in .env.

Azure OpenAI

Set AZURE_BASE_URL and AZURE_KEY. Set DEPLOYMENT, or pass a deployment name with --model:

uv run python -m src.main evaluate \
  --evaluator azure \
  --model gpt-5.5 \
  --concurrency 20

The llama evaluator uses the same Azure credentials and defaults to the Llama-4-Maverick-17B-128E-Instruct-FP8 deployment:

uv run python -m src.main evaluate --evaluator llama --concurrency 20

OpenAI

Set OPENAI_API_KEY. The default model is gpt-5.5; override it with --model:

uv run python -m src.main evaluate --evaluator openai --concurrency 20

DeepSeek on Azure

Set AZURE_RESOURCE_BASE_URL and AZURE_RESOURCE_KEY. The default deployment is DeepSeek-V3-0324. Models such as DeepSeek-R1 that do not expose reasoning effort control run with their native reasoning behavior:

uv run python -m src.main evaluate --evaluator deepseek --concurrency 20

OpenRouter

Set OPENROUTER_API_KEY (or OPENROUTER_TOKEN). The default model is qwen/qwen3-30b-a3b-thinking-2507:

uv run python -m src.main evaluate \
  --evaluator openrouter \
  --model qwen/qwen3-30b-a3b-thinking-2507 \
  --concurrency 20

Compiler-driven conversion and physical validation

The catalog is derived from compiler structure rather than regular expressions over Modelica source. The pinned toolchain is OpenModelica 1.26.9 with MSL 4.1.0. A shared catalog/component-library.yaml defines reusable generic types from Modelica class, inheritance, component, and equation APIs. Each type holds only local variables, local state partitions, guarded component-local transition records, function-free local laws, terminals, dynamic properties, and typed class-wide assumptions. Numeric parameters remain instance bindings.

Reviewed MSL profiles give named states to ten electrical, thermal, translational, and rotational type variants. Examples include REVERSE_CURRENT/ZERO_CURRENT/FORWARD_CURRENT, COOLING/THERMAL_REST/HEATING, and MOVING_NEGATIVE/REST/MOVING_POSITIVE. The states partition one exact compiler-bound coordinate. Adjacent transitions name their source and target states, the boundary-event coordinate, signed derivative guards, and profile provenance. Unprofiled smooth classes retain one unconditional state.

Each model.yaml therefore contains component instances, operating contexts, and connection sets rather than a second set of authored system laws. Assembly alpha-renames the generic laws and derives physical compatibility and conservation laws from the declared material, conduits, terminals, and topology; directed signals derive their one-driver compatibility laws. Source time profiles live in operating contexts and never become structural component functions. Unsupported connector profiles, component functions, modes, or cross-component residues fail closed and leave the existing catalog untouched.

Every item retains compiler model-instance.json, flattened XML DAE, deterministic structural.json, compiler-resolved simulation options, a validation manifest, and one CSV artifact per executed validation experiment. structural.json is the sole deterministic structural-extraction artifact. The certificate hashes the shared library and all item artifacts, requires complete structural accounting and passed trace soundness, and records observed mode, transition, qualitative-cell, and exact episode coverage. It records honestly whether interpretation realizability or a fully materialized episode graph was proven. Every declared mode, transition, and qualitative cell receives one conservative disposition: witnessed, proven_unreachable, outside_fixed_instance, or unresolved. Exact graph absence is used only when it proves unreachability; fixed parameter bindings and permanent context restrictions identify alternatives outside the certified instance.

The solver, causal account, trace validator, and task generators consume the assembled device. Exact episode graphs are materialized only for small devices; larger devices use the same topology-local transition rules on demand to keep conversion within the reviewed work budget. A cross-state edge is accepted only when every changed component matches a declared transition, its endpoint guards, and its selected event coordinate. Modelica traces validate the named state at every retained sample and reject observed changes with no guarded declaration path. The bounded trace portfolio certifies only declarations it observes; it does not claim exhaustive transition coverage.

Validation uses the model's declared start/stop time, tolerance, and output interval by default. --start-time, --stop-time, --tolerance, and either --number-of-intervals or --interval provide explicit audited overrides. The default bounded portfolio contains four experiments and --maximum-experiments accepts one through eight. The planner starts with the nominal run. When the configured window truncates a declared periodic source, it adds one sign-complete source-cycle run whose uniform output grid lands exactly on source zero crossings and extrema. It then varies independent compiler-fixed initial coordinates one at a time and fills any remaining budget with tolerance/output-grid robustness runs. It never forms a Cartesian product or perturbs fixed mechanism parameters. OpenModelica compiles each fixed mechanism once and reuses the executable for the complete portfolio. Perturbed-start traces are checked against every declared law and operating restriction except the nominal initial restriction; the manifest records the exact override. Coverage-seeking source-cycle traces retain law, context, state, and guarded-transition checks without claiming exact episode-node witnesses at isolated numerical landmarks. After validation, a deterministic greedy set-cover pass records the smallest observed-coverage witness subset while retaining every executed trace as robustness evidence.

In the released catalog, all 72 planned experiments execute. They witness 252/309 component modes, 76/328 declared transitions, and 3,365/5,375 qualitative cells. Closure additionally proves 28 transitions and 60 cells unreachable under exact episode semantics and classifies 339 cells as outside the fixed instances; 57 modes, 224 transitions, and 1,611 cells remain explicitly unresolved. The greedy behavioral witness subsets contain 43 of the 72 executed traces.

Generate the atomic gold-label attribution from the retained CSV traces and release solutions without rerunning OpenModelica:

uv run python -m src.analysis.gold_validation \
  --paper-table paper/figures/gold_validation_summary.tex

The command writes gold_validation_attribution.jsonl (one row per atomic decision), gold_validation_items.jsonl, and JSON/CSV/LaTeX summaries under benchmark/v1.0.0/analysis/gold_validation/. A joint numerical witness requires one trace to realize the complete qualitative interpretation, path, or edge. Marginal mode/cell observations remain local evidence, and universal, absence-based, or deterministic replay decisions remain simulator-only.

Run the gold-independent behavioral-concordance audit over the same certified OpenModelica trace portfolio:

uv run python -m src.analysis.behavioral_concordance run \
  --paper-table paper/aaai27/figures/behavioral_concordance_summary.tex

The command is separated into extract, predict, and score phases. The first phase freezes distinct composite component-state configurations and component transition shapes from the persisted numerical CSVs. When the crisp projection snaps a nonzero value to a point landmark, it also freezes the point cell and the cell containing the raw value as candidates; this step does not consult the qualitative solver, launch OpenModelica, or read benchmark tasks or solutions. Production trace-conformance diagnostics are retained as metadata but do not filter those numerical phenomena. The second phase loads only that frozen query artifact and asks whether each state has a nonempty exact MDD relation and whether each transition shape has a declared directed path. If a crisp state is empty, it lazily checks the finite raw-side component-state candidates, stopping at the first exact compatibility witness under a 4,096-assignment cap. It clears the solver cache after every exact solve, never enumerates qualitative interpretations, never constructs the episode graph, and records explicit decision-state, branch, propagation, scope, and boundary-assignment limits. The final phase joins the two frozen artifacts by stable phenomenon id.

For v1.0.0, 72 experiments across all 18 mechanisms yield 186 distinct composite-state configurations and 155 component-transition shapes. There are 184 direct state agreements and 155/155 direct transition-shape agreements. The two remaining crisp state vectors are boundary-compatible: at 0.001 s in mechanics_branched_three_mass, the raw positive velocities admit leaf1/leaf2.MOVING_POSITIVE; at 0.735/0.757 s in mechanics_damper, the raw positive velocity admits mass1.MOVING_POSITIVE. Exact MDD solves accept both raw-side vectors after four candidate assignments in total. The audit therefore reports 339/341 direct agreements, two boundary-compatible observations, zero contradictions, and zero inconclusive cases (100% compatibility on the bounded portfolio).

This study supplies quantitative, task/gold-independent evidence for converter-level behavioral concordance on the bounded portfolio. It does not prove that all continuous Modelica trajectories are represented, validate unobserved qualitative behavior, or independently establish every benchmark label: the numerical-to-qualitative projection and the released catalog remain shared boundary assumptions.

Convert and validate the eighteen admitted catalog targets:

uv run python -m src.modelica_to_qualitative \
  --selected all \
  --modelica-root ModelicaStandardLibrary_v4.1.0 \
  --catalog-dir catalog

Twelve targets are stock MSL 4.1 examples: one electrical (Resistor), seven translational (SignConvention, Accelerate, Damper, InitialConditions, Oscillator, WhyArrows, and CompareBrakingForce), three rotational (FirstGrounded, First, and CompareBrakingTorque), and one thermal (TwoMasses). Six repository-authored Modelica compositions reuse only already-supported MSL component classes: an electrothermal resistor ladder, an electrothermal parallel network, a three-node thermal chain, a branched thermal star, a branched three-mass spring--damper system, and a grounded geared dual-inertia rotational system.

The electrothermal models and Resistor use the audited operating window 0.01--0.49 s, so their validation traces remain within one continuous source regime. The two braking comparisons use 0--0.4 s with 1,000 intervals; this audited context ends before the stop-event discontinuities that require multiple operating contexts. Command-line time overrides take precedence over these per-job defaults. The configured profile targets a complete conversion and validation run within three minutes per item. Nine original targets are explicit converter limitations and are skipped rather than approximated:

• ParallelResonance and SeriesResonance: variable-frequency sinusoidal sources need phase-region states; a sign envelope admits histories outside the prescribed input.

• ShowVariableResistor: its mixed variable-resistance network exhausts the bounded intrastate solver before realizability can be established.

• EddyCurrentBrake: its nonlinear torque depends jointly on excitation, speed, and temperature; those physical coordinates cannot be replaced by arbitrary source histories.

• DemoPowerSupply: algorithmic initialization and piecewise source modes are outside the function-free local polynomial profile.

• RollingWheel: IdealRollingWheel has internal physical topology; recursive composite expansion is outside the bounded converter.

• ElasticBearing: exact episode construction exceeded the 175-second watchdog.

• translational Sensors: its power output needs stable second derivatives of a derived product, which the nominal trace cannot certify without numerical differentiation artifacts.

• thermal Motor: piecewise table-source jumps require multiple operating contexts and violate the single-context zero-time derivative check.

These limitations are inventory metadata, not model-name behavior templates; the generic converter reaches them through unsupported-structure or work-budget checks. Previously generated benchmark tasks, evaluations, and plots were invalidated by the schema and solver replacement and were not regenerated in this migration.

The non-catalog regression model Modelica.Thermal.HeatTransfer.Examples.ControlledTemperature, is expected to return inconclusive: it exposes a Boolean connector outside the reviewed real-signal connector profile. It remains a fail-closed integration-test fixture only and is never written to catalog/.

Convert one custom model:

uv run python -m src.modelica_to_qualitative \
  --source path/to/Model.mo \
  --model-name Package.Model \
  --catalog-id my_model \
  --modelica-root ModelicaStandardLibrary_v4.1.0 \
  --catalog-dir catalog

Exit status 0 means validation passed, 1 means a trace or compiler failure, and 2 means conversion was inconclusive (for example, an unavailable compiler or unsupported bounded-profile construct). Existing catalog artifacts are not replaced on failed or inconclusive runs.

Requirements

Simulation runs in Docker. Pull the OpenModelica image once:

docker pull openmodelica/openmodelica:v1.26.9-minimal

Download and unpack Modelica Standard Library 4.1.0 so its source tree has this layout (the library is not tracked by this repository):

ModelicaStandardLibrary_v4.1.0/
└── Modelica 4.1.0/
    ├── Electrical/
    ├── Mechanics/
    └── Thermal/

validate-catalog is the strict task-readiness gate: it loads the shared component library, assembles every model, verifies each sibling validation.json and its bound artifact hashes, and requires complete structural accounting and passed trace soundness.

uv run python -m src.main validate-catalog --catalog-dir catalog

Development

Format Python code with Black:

uv run black src tests scripts

Run Ruff checks:

uv run ruff check src tests scripts

Run the default test suite:

uv run pytest

Run the complete release checks with pre-commit. Gitleaks must be installed separately; on macOS it is available through Homebrew:

brew install gitleaks
uv run pre-commit install
uv run pre-commit run --all-files

License

First-party Mech Reasoner source, catalog compositions, benchmark records, manuscript source, and generated analysis artifacts are distributed under the GNU General Public License, version 3 only (GPL-3.0-only), unless a file's SPDX metadata states otherwise. See LICENSES/GPL-3.0-only.txt.

Third-party materials retain their own terms. The Modelica Standard Library and OpenModelica are external dependencies. The unmodified AAAI-27 author-kit style file is governed by the AAAI author-kit notice, and its generated BibTeX style declares the LaTeX Project Public License. Repository-level licensing annotations are maintained in REUSE.toml, with corresponding license texts under LICENSES/.

Check the complete first-party and third-party inventory with:

uv run reuse --no-multiprocessing lint