SAID Laboratory · research system · v0.2
A neural instinct for structure. Classical solvers for values. An exact checker for truth.
MARC represents a problem as a constraint graph and learns the one decision classical methods cannot make: what to add to it. The right auxiliary variable, substitution, or defining relation turns an unsolvable graph into a solvable one. Everything downstream is delegated: values to classical solvers, acceptance to an exact symbolic checker.
Solving a constraint problem splits cleanly. We bet on the wrong half first, measured it honestly, and moved the learning to the half where classical methods have nothing.
Smooth, gradient-rich, and covered by sixty years of numerical analysis. Levenberg–Marquardt with restarts saturates our hard nonlinear families. A learned proposal ties or loses to plain random restart once solutions are coupled.
Which auxiliary quantity to introduce. Which substitution linearizes the system. No gradient exists over this space, enumeration grows combinatorially, and a solver cannot decide to invent d = x − y. A learned prior amortizes exactly this choice.
We ran the controls that could kill our own first idea, and they did. The negatives are reported with confidence intervals and kept in every paper we write: they are the motivation, measured.
The earlier high-dimensional win was a separability artifact. The "learned proposal beats classical search" route is closed.
With restarts, LM saturates the nonlinear suites. Raw solve rate can never be the claim; cost and representation can.
Deterministic descent always traps; Langevin noise escapes. Real and CI-backed, but it argues for noise in search, not for a learned denoiser.
The one learned component that beat random-slot and no-context controls. Regenerating at scale under a contamination-proof seed protocol before any number is cited.
House law: every rate ships with N and a Wilson interval, every comparison with a corrected significance test, and structure-selection numbers exist only if the run's own artifact proves its seeds were clean. We caught one contaminated result ourselves, withdrew it, and rebuilt the protocol so the eval refuses to repeat the mistake.
A fixed graph with no consistent assignment. The policy proposes one auxiliary: a node flips from absent to active with its defining relation. A classical solver then fills the values and the checker accepts. That flip is the entire thesis.
Every rung keeps the same end-to-end bar: a proposal counts only if the augmented graph actually solves and passes the checker. Until the last rung, the honest term is menu-based structure selection. "Invention" names the destination, not the current claim.
Pick the correct augmentation from K procedurally generated candidates: exactly one is solvable by certified construction, and hard negatives share the right structure with the wrong constant.
The policy's value head supplies the defining constant itself. The candidate space becomes continuous; the menu only provides insertion structure.
Choose the insertion set and defining relation independently; instantiate several auxiliaries at once. The slot schema already supports it.
Emit the defining expression itself: invention proper. The prize, out of scope until the rungs below it hold.
refine, lm, exact, random are labeled on every table and never presented as system results.paper/PROVENANCE.md.