15.10 Symbolic laws and active mathematical experiments

The AI-Feynman (AF) ladder moves from latent presentations to symbolic law construction. Generated worlds use opaque variable names and hide coefficients. A deterministic compiler fits numerical parameters only after a structural proposal has been made, then tests fresh points. The scientific question is whether the expression grammar itself is adequate and, when it is not, whether a typed generator can be added conservatively.

AF–0 contains additive, multiplicative-power, inverse, symmetric-interaction, and nested-composition laws. The fixed grammar omits reciprocation. Fixed search recovers \(5/10\) theories; a typed residual diagnostic recovers and admits all ten, including two conservative reciprocal extensions. Adding an active query changes no decision because the noiseless residual spectrum is already decisive. This negative ablation supports an acquisition rule for these generated worlds: purchase an experiment only while the admissible theory set remains ambiguous.

AF–1 deliberately restricts public observations to manifolds on which pairs of noisy laws agree. Diagnostics alone recover \(7/12\) families. A random generic query and a maximum-disagreement query both identify the correct family in \(12/12\); strict admission is \(12/12\) and \(10/12\), respectively, because two active responses fail to transport the required grammar repair. Active selection reduces completion cost, but almost any point off the agreement manifold is informative, so it cannot claim an accuracy advantage over random exploration.

Table 15.4. The categorical AI–Feynman ladder. Recovery means typed semantic admission on hidden points, not merely low error on the visible profile. AF–0, AF–2, AF–3, and AF–4 report their prospectively repaired v2 protocols; the corresponding v1 records are retained as protocol or calibration failures and are not pooled with these values.

AF–2 crosses the clearest declaration boundary in this sequence. It withholds family names and asks for a fresh typed expression from a normalized unary profile. Accepted constructions include reciprocal, absolute value, cube, and base-two exponential. Seven of eight typed-profile cases are admitted, whereas raw expandable generation admits only one. The task remains controlled: the profile is externally localized, the semantic registry is small, and the expression grammar is supplied. Nevertheless, the output is an executable operation rather than a label attached to a supplied family.

The v2 qualifier is substantive rather than cosmetic. AF–0 quarantined its setup record before any model call when fixture replay exposed a serialized variable-role bug. AF–2 v1 compared surface strings and rejected mathematically equivalent expressions; v2 scores semantic equivalence classes. AF–3 v1 assigned the same domain type to every generator and incorrectly rejected valid scalar-valued declarations; v2 registers generator-specific domains. AF–4 v2 prospectively raised the completion budget after the smaller v1 budget truncated twelve of thirty calls. These records expose evaluator and inference-budget defects, not extra model trials from which the best outcome was selected.

AF–3 shows how constructive declaration can be combined with conservative experiment choice. Reciprocal and cubic maps agree on the initial normalized measurements at \(-1\) and \(1\), while absolute value and exponentiation are already identifiable. The sequential policy queries only ambiguous worlds, recovers all eight supported generators, rejects sine and sign controls, and uses one additional probe in each ambiguous supported case. It matches a two-random-probe ceiling with one quarter of the added measurements on those worlds.

The open-search rungs expose the unresolved difficulty. In AF–4 the external selector can isolate one class inside its finite enumerator, while the model continues to entertain interpolating polynomials and other expressions outside that privileged space. In AF–5 the query is selected from the model’s own compiled candidates, but the true operation is often missing from that set. Proposal-aware selection is then optimal relative to an inadequate cover. These failures give the mathematical version of the observability caveat: no experiment can separate a hypothesis that the construction process is unable to express.

. Active mathematical discovery must close the loop around the proposal language actually used by the reasoner. A discriminating query in an oracle’s hypothesis space is not necessarily discriminating for the learner.