ifc-0068

4.7.3 The training loop

4.7.3 The training loop

Let \(\mathcal E_{\mathrm{train}}\), \(\mathcal E_{\mathrm{val}}\), and \(\mathcal E_{\mathrm{adm}}\) be disjoint problem sets. Training rollouts produce traces for proposing edits. Validation accepts or rejects edits. The admission set remains locked until the skill document has been frozen. A benchmark may expose admission outcomes only after the training run is over; using those same cases for another update creates a new benchmark version.

For a skill document \(m\), define a validation profile

\[ Q_{\mathrm{val}}(m)= \bigl(q_{\mathrm{type}},q_{\mathrm{loc}},q_{\mathrm{proposal}}, q_{\mathrm{precheck}},q_{\mathrm{abstain}}, -q_{\mathrm{cost}}\bigr). \]

The components measure type safety, obstruction localization, proposal quality, internal precheck success, calibrated abstention, and resource use. They remain visible separately. A declared preorder \(\succ _{\mathcal G}\) first enforces hard gates \(\mathcal G\)—including false-extension and regression limits—and only then compares eligible profiles. A bounded edit \(m\to m'\) is accepted exactly when

\[ \mathcal G(m')=1 \quad \text{and}\quad Q_{\mathrm{val}}(m')\succ _{\mathcal G}Q_{\mathrm{val}}(m). \]

This generalizes SkillOpt’s strict held-out improvement rule without hiding scientific validity inside a weighted sum.

Training DIAL-SkillOpt

  1. Initialize frozen discovery agent \(F\), typed skill document \(m_0\), optimizer \(G\), rejected-edit buffer \(B\), and disjoint task splits.

  2. For epochs \(k=0,\ldots ,K-1\):

  3. Run \(F[m_k]\) on \(\mathcal E_{\mathrm{train}}\); record DIAL states, flows, mixed witnesses, proposals, abstentions, and resource use.

  4. Let \(G\) propose bounded add/delete/replace edits using the traces, current validation profile, and \(B\).

  5. Type-check each candidate and evaluate it on \(\mathcal E_{\mathrm{val}}\) with matched budgets and fresh seeds.

  6. Accept the best candidate satisfying the hard gates and strict profile-improvement rule; place rejected edits and counterexamples in \(B\).

  7. Apply a slow meta-update to the edit strategy without changing the frozen discovery agent or reading \(\mathcal E_{\mathrm{adm}}\).

  8. Freeze \(m_*\), then evaluate it once on \(\mathcal E_{\mathrm{adm}}\) using independent proof, simulator, or empirical certificates.

  9. Publish \(m_*\), all versions, traces, split hashes, admission vector, and failures.

When a fixed local skill basis admits continuous coefficients \(w\), an inner optimizer may use a geometry-aware step such as

\[ w_{k+1}=w_k+\eta \, G(w_k)^{-1}\nabla _w\widetilde U_{\mathrm{val}}, \]

where \(G\) is a declared metric and \(\widetilde U_{\mathrm{val}}\) is a validation surrogate. This is legitimate for motion inside the maintained skill geometry. Bounded Markdown edits, new skill types, and finite sketch extensions remain discrete typed operations; the equation does not make them ordinary gradient steps.

. The optimizer may inspect training traces, validation profiles, rejected edits, and provisional checks. It may not query the locked admission cases, alter their simulators or proof obligations, or treat its own confidence as a certificate. The final report separates proposal success, admission success, false extension, calibrated abstention, transfer, and cost.