The research question
Can a solver teach a model a useful way to search?
A symbolic solver can find an answer by exploring thousands of possibilities. A language model has to produce a useful explanation and an answer within a small token budget. My idea was to bridge that gap: use a solver to obtain a feasible destination, construct a short trajectory leading to it, and teach that trajectory before asking the model to improve through reinforcement learning.
This page explains the design choices, the obstacles behind them, and how I would extend the approach. The solver, synthetic trace generator and curriculum training pipeline were implemented. Semantic rewards extracted from the traces were the proposed next phase. The experiments did not demonstrate a successful symbolic reasoning model.
01 · Find the bottleneck
A familiar equation with unfamiliar rules
The competition used a shared Nemotron-3-Nano-30B model and evaluated a submitted LoRA adapter on answer accuracy. Its published evaluation allowed an 8,192-token context and up to 7,680 generated tokens. The model had to end with a boxed answer. Competition overview and metric ↗
The data covered numeral conversion, unit conversion, gravity, ciphers, bit manipulation, numeric equations and symbolic equations. In our competition work, the other categories had become much more reliable. Symbolic equations remained the bottleneck, so we focused our effort there.
AC + BE = CH
BD + CE = EI
Infer the hidden rules, then encode the result.
Invented example for this explanation. Even “+” is just an operator glyph in the real task: it need not mean addition. Extra examples used in the interactive trajectory below constrain more symbols.
A candidate solution is a small program: a symbol-to-digit mapping, an operator-to-function mapping, and an encoding convention. With A=1, B=2, C=3, D=4, E=5, F=6, G=7, H=8, I=9 and ordinary addition, AB + CE becomes 12 + 35 = 47, encoded as DG. This is one feasible interpretation; a few examples may leave several interpretations possible.
02 · Design the learning pipeline
Two phases: teach a procedure, then reward useful progress
Known solutions provide supervised targets. Short, structured explanations provide a procedure to imitate.
1. Curriculum SFT
Start with fewer equations. Train on attempts, checks, repairs and the answer. Unlock larger problems while retaining replay.
2. Reinforcement learning
Sample the model’s own tagged trajectories. Verify the claims. Reward correct answers and valid progress; penalize false checks and repetition.
SFT is the warm-up: it gives the model examples of how to organize a candidate, test it and revise it. RL would then expose the model to its own mistakes and optimize the behaviors that an external checker can verify. Neither stage guarantees that the model learns general reasoning; that has to be measured on unseen puzzles.
03 · Obtain supervision
First, build something that can find a solution
We initially lacked reliable teaching solutions ourselves. Through trial and error, the approach became a constrained symbolic search, with a Python driver and a Rust search core. Instead of allowing arbitrary mathematics, we defined a manageable set of operation families, including addition, multiplication, differences, division, remainders, gcd, lcm and concatenation. Small offsets cover variations such as a × b + 1.
decode(AB) = b·d(A) + d(B)
Base 10, A=1, B=2 → 12
decode(AB) = d(A) + b·d(B)
Base 10, A=1, B=2 → 21
Here b is the numeral base and d maps a symbol to its digit. The research explored base choices; later configurations fixed base 10 for simplicity.
- Check simple structure. A demonstrated forward or reverse concatenation pattern can avoid arithmetic search entirely.
- Narrow the operation candidates. Inspect signs, repeated operands, result widths and symbol patterns. Operator-glyph statistics suggest a search order, while logical impossibility checks can eliminate candidates.
- Assign digits and prune. Enforce distinct digits for distinct symbols. As assignments become available, check constraints and abandon branches that cannot satisfy them. Backtrack and try another candidate or encoding.
- Collect feasible programs. Keep solutions consistent with the constraints, optionally collecting several. During data construction the known target answer can be included as a constraint; this makes the solver a supervision oracle, not an unbiased measure of test-time accuracy.
Why not teach the brute-force log? Exhaustive search is lengthy, contains many unhelpful dead ends and easily overwhelms the competition’s token budget. A successful search log also does not automatically provide a concise, learnable explanation. I wanted to retain the valid destination while controlling the teaching path.
04 · Work backward to teach forward
Synthetic trajectories from a fixed feasible solution
Choose one feasible target program. Starting from its digit mapping, make a small change—swap two assignments or reassign a symbol to an unused digit. Repeat for up to N perturbations. Then reverse the sequence: the teaching trajectory begins with a flawed hypothesis and reaches the fixed target through one repair at a time.
The intermediate hypotheses deliberately fail; what must be sound is the arithmetic used to check them and the final solution. The generator uses a forward check to describe a mismatch, then frames a repair as a hypothesis to test. Several trajectories can lead to the same target. These are constructed teaching explanations, not a claim about the actual search history or a model’s internal reasoning.
Follow a synthetic repair trajectory
For this toy example, addition and standard base-10 encoding are fixed. Move from the perturbed mapping toward the selected target.
| Example | Decoded check | Result |
|---|
What changes between attempts?
The target assigns A… I to 1…9. Construct backward by swapping A/B, then C/D, then E/F. Read forward, undo E/F, C/D, then A/B. The example equations are independently recomputed at each attempt. A repair may fix one equation and disturb another; only the final mapping must pass every check. The selected endpoint is known during construction.
Keep the text useful and short. Describe the mismatch rather than every searched branch. Reuse a concise operation vocabulary, skip unchanged checks where appropriate, and cap the number of repair attempts. The implementation estimates text length and reduces perturbations; exact tokenizer checks would be needed to guarantee the final response fits.
Do not disguise privileged information as deduction. The known endpoint helps construct the path, but a narrated claim should be justified by the visible examples. “Try this swap” is a proposal; “this digit must be 4” needs evidence. The project’s later revisions addressed this distinction and visibility of symbols absent from the prompt.
05 · Make the learning task progressive
Start small, retain useful experience, increase complexity
Long systems require more candidate checks, more cross-equation consistency and longer explanations. My curriculum starts with one shown equation plus one query—two equations in total—and progresses toward problems with three, four or five shown equations. Earlier examples remain in the mix while harder buckets are introduced.
+ query→2 examples
+ query→3 examples
+ query→4–5 examples
+ query
The implemented scheduler adapts competence-based curriculum learning. A square-root schedule unlocks buckets according to their cumulative dataset share. Before full difficulty, the sampler balances the unlocked buckets. The last phase focuses on the three–five-example distribution. A separate replay stream from the other puzzle categories stays active throughout.
What goes into a training batch?
Batch size 32: 8 replay slots and 24 symbolic slots. Shares are expected values; actual samples use seeded shuffled cycling. At step 175, one- and two-example buckets drop out of the symbolic mix.
The loss teaches the assistant’s trajectory and final answer while masking the prompt. To test the curriculum fairly, I would compare it with flat sampling under the same token budget, starting adapter and puzzle-level split. Augmentations of the same original puzzle must stay in the same split.
06 · Proposed next phase
Make reasoning steps inspectable—and reward what can be checked
After SFT, the model would generate its own trajectories in the learned format. Tags give a fixed reward function places to look: the proposed digit mapping, the equations checked, the detected failure, the suggested repair and the conclusion. The important step is independent verification, rather than trusting a model’s claim that it passed a check.
- 1Sample a group
Warmed-up policy generates several tagged attempts for one puzzle.
- 2Parse & verify
Recompute equations and compare states using a deterministic checker.
- 3Assign rewards
Combine answer accuracy, valid progress and bounded penalties.
- 4Update the policy
Use group-relative advantages in GRPO; sample again.
| Trace field | What to extract or verify | Status |
|---|---|---|
<digit_mapping_N> | A candidate assignment. Check valid digits and one-to-one symbol mapping. | Existing tag |
<digit_mapping_analysis_N> | Decoded operands, chosen operations and example checks. Recompute them. | Existing tag |
<digit_mapping_analysis_follow_up_N> | A repair hypothesis. Compare the before/after mappings and checks. | Existing tag |
<conclusion> | Final encoded answer and consistency with the selected program. | Existing tag |
<check eq="2"><repair> | Machine-readable operands, computed result, expected result and changed assignments. | Proposed extension |
<reject reason="…"><assumption> | A verifiable reason to discard a candidate; an explicit choice when the examples do not determine a unique rule. | Proposed extension |
<check eq="1">
mapping: A=2, B=1, C=3, D=4, F=6
operation: add; encoding: standard
computed: 21 + 34 = 55; expected: 46
verdict: fail
</check>
<repair>
hypothesis: swap A and B, then recheck all examples
</repair>Proposed structured extension, illustrated on the toy equation AB + CD = DF. The arithmetic is checkable; the verifier must still test whether the proposed swap improves the full constraint set.
| Signal | Reward or penalty | How to avoid a shortcut |
|---|---|---|
| Final answer | Reward matching the reference answer. | Keep this separate from merely finding a program consistent with the demonstrations. |
| Constraint consistency | Reward the fraction of all shown equations satisfied by a valid candidate. | Use one shared mapping and operation choice across checks; recompute every equation. |
| Useful repair | Reward net improvement in verified constraints. | Count novel states, cap the bonus and do not reward undo/redo cycles. |
| False verification | Penalize claiming that an incorrect computation passed. | A failed hypothesis honestly reported is allowed; fabricated success is not. |
| Repeated states & excess length | Penalize unproductive loops and budget overruns. | Do not pay for the number of tags; retain enough space for useful exploration and the answer. |
Credit an honest partial attempt
R = answer + 0.2·consistency + 0.1·progress − 0.2·false-check − 0.1·loop − 0.05·overrun
A design sketch: all components are bounded and recomputed by a verifier. It illustrates how two wrong answers can receive different feedback. These weights are not experimental results or a recommended optimum.
Even dense rewards can be uninformative if every rollout earns the same score. I would mix problem difficulty to keep both successes and failures in the group, keep a small SFT/replay stream during refinement, and monitor final-answer accuracy separately from process scores. A higher process reward is useful only if it transfers to better answers on unseen problems.
What I learned
A useful research direction, an unsuccessful model so far
The central lesson was that finding a feasible solution and teaching a language model to find one are different problems. A symbolic oracle supplied targets. Synthetic trajectories made them shorter and structured. A curriculum made the training distribution controllable. None of that was enough to demonstrate strong symbolic performance in the saved runs.
Best saved symbolic-equation diagnostic. These are public training puzzles, not a held-out benchmark. The saved evaluations predate the last generator revision; there is no verified final score for that revision or the proposed semantic RL phase.
View the saved diagnostic results and their limits
| Saved run label | Correct / 823 | Accuracy |
|---|---|---|
| Zero-example · unmasked basic | 3 | 0.36% |
| Zero-example · masked analysis | 3 | 0.36% |
| Zero-example · masked basic | 7 | 0.85% |
| Merged · unspecified configuration | 5 | 0.61% |
| Merged · mask-prefix · 250 steps | 1 | 0.12% |
| Merged · mask-prefix-initial · 400 steps | 29 | 3.52% |
Labels summarize saved filenames, not controlled comparisons. The best run included boxed answers in only 81 of 823 outputs, pointing to completion/format problems; missing token counts and finish reasons prevent assigning a single cause. The ~86% starting competition adapter documented in the repo is a different result and is not the outcome of this method.
Evidence and methodology · Aggregate results with source hashes
How I would continue
- Improve the SFT foundation. Audit each claim for visible evidence, preserve honest uncertainty, measure exact token lengths and train until the model reliably completes a checkable trajectory.
- Test transfer, not memorization. Hold out whole source puzzles and novel symbol mappings. Compare curriculum with flat sampling, and compare short synthetic repairs with answer-only or direct explanations under the same budget.
- Implement the process verifier. Start with mapping validity and arithmetic checks; add repair progress only after testing against false claims, repeated states and reward manipulation.
- Spend more effort on RL after a usable warm-up. Compare answer-only and process-aware rewards, track each category to detect forgetting, and retain changes only if final-answer generalization improves.
My hypothesis is that stronger SFT followed by carefully verified RL feedback could make better use of these trajectories. That remains an experiment to run. I am sharing the design because the route from a difficult problem to a testable training strategy is worth documenting, including where it failed.
Code & references
- Public research repository — solver, latest generator, training notebooks, original specifications and experiment evidence.
- NVIDIA Nemotron Model Reasoning Challenge — task, model and evaluation constraints.
- Equation Symbolic Solver by lkevincc0 — the public solver starting point that this work built on.
- Platanios et al. (2019), Competence-based Curriculum Learning for Neural Machine Translation — the schedule adapted for this experiment.
Research developed during the 2026 competition. This explainer presents the method and proposed extensions; simulations are illustrative and run locally in your browser.