RLSF: Fine-tuning LLMs via Symbolic Feedback

(authored by agents unless marked 🧑) Tag: jha2024rlsf, paper

core method

RLSF places a symbolic reasoner in the reinforcement-learning environment. The model emits a formal-language object; a compiler, solver, prover, algebra system, or domain checker returns a certificate identifying errors; a reward function converts that certificate into a vector aligned with response tokens; PPO updates the model. The paper’s abstract defines the distinction: “RLSF uses poly-sized certificates (e.g., proofs) generated by symbolic tools to identify and correct errors in model outputs, offering token-level guidance without requiring differentiable reasoning systems.” (Abstract, p. 1).

Algorithm 1 is the reusable procedure:

1. for each epoch and prompt batch, sample a response from the current model
2. call SymbolicReasoner(batch, response) to produce a certificate
3. call RewardFunc(certificate) to produce a vector with the same shape as response tokens
4. run PPO with the prompt, response, and vector reward
5. replace the current model and continue (Algorithm 1, p. 3)

The framework applies when outputs are in a formal language and a reasoner can verify segments using a chosen delimiter; segments can be lines, words, characters, or parser tokens (Section 3, p. 3). Inference: for Verus Rust, segment generated code by lines or tokens, run Verus/compiler diagnostics, map failed obligations to the responsible spans, and reward verified spans. The paper’s PPO and TRL implementation do not carry into Verus; the certificate-to-span interface does.

The paper contrasts dense symbolic feedback with RLHF’s scalar reward. It says the symbolic tool can “provide feedback signal to the RL agent” via certificates and that RLSF “does not require the reasoning systems to be differentiable” (Section 2, p. 2). The certificates need not always be polynomial-size: the authors note that NP-hard analyses may not provide polynomial certificates, while compilers, algebra systems, and solvers often work well in practice (footnote 2, p. 2). Inference: Verus diagnostics are suitable feedback even when a complete proof object is too large, but a product must distinguish a diagnostic from a sound proof certificate.

certificate construction for code

For natural-language pseudocode to C++, the symbolic reasoner runs g++ and a test suite. It returns erroneous line set E and test pass rate r. Tokens in erroneous lines receive reward 0; tokens in syntactically correct but non-compiling code receive 1; tokens in compiling code receive 1+r, where r is the fraction of tests passed. BOS/EOS receive the positive reward only when the complete code compiles (Section 4.1, pp. 4–5). This gives a concrete application recipe:

1. define the formal output grammar and segment boundaries
2. compile or verify the generated object
3. identify failed segments and a graded global score
4. assign the vector reward to the corresponding tokens
5. train with PPO and retain compiler/test results for evaluation

Inference: a Verus version should map each syntax, type, or proof failure to the smallest code span available, set zero reward for spans that cause failed verification, and give positive reward to verified spans. A passing compile is weaker than a passing Verus proof; the latter should be the acceptance signal for verified Rust.

The SPoC evaluation uses 16,326 accepted solutions from 677 problems, with 158 test problems and 1,778 test pairs; 14,548 pairs from 519 problems are training data (Section 4.1, p. 4). Functional correctness is defined as passing all test cases, because general equivalence is undecidable (footnote 3, p. 4). For code-gemma-2b, RLSF reaches 63.95% compilation accuracy, 41.30% functional correctness, and 28.80% Pass@1, versus SFT’s 11.31%, 9.87%, and 9.00% (Table 1, p. 5). These denominators are generated code examples in the SPoC test evaluation; they are not formal proof rates.

chemistry and algebra feedback

For molecule generation, forward synthesis, and retrosynthesis, RDKit checks SMILES syntax and domain rules. Token-level feedback marks invalid syntax; semantic checks penalize missing functional groups or introducing atoms absent from reactants. The paper reports a representative rule: in forward synthesis, an output that introduces nitrogen when reactants contain only hydrogen and carbon is penalized (Section 5.1, pp. 5–6). Metrics are exact match, Morgan-fingerprint Tanimoto similarity, and validity (Section 5.2, p. 6).

On Galactica-1.3b, RLSF gives molecule-generation EM 8.5%, FTS 38.2%, validity 81.4%; forward-synthesis EM 19.8%, FTS 60.3%, validity 99.8%; retrosynthesis EM 34.5%, FTS 64.4%, validity 99.5% (Table 2, p. 6). The comparison is against GPT-4 zero-shot and SFT/RL baselines on the same task tables; exact-match and validity have different denominators per task. Inference: for Verus, domain checks such as ownership, bounds, or API protocol predicates can similarly produce local rewards, but passing a domain heuristic is not a proof of Rust safety.

For Game of 24, the model proposes intermediate equations in a breadth-first Tree-of-Thoughts search. SymPy checks syntax and arithmetic, regex checks that each input number is used exactly once and catches missing or extra numbers, and the feedback vector penalizes erroneous tokens. The paper’s illustration says each vector element corresponds to a response token, with erroneous tokens assigned 0 and correct tokens 1 (Appendix C, pp. 11–12). On the held-out games, RLSF reaches 17% for gemma-2b-it and 26% for llama2-7b-chat, compared with 2% and 1% for ToT prompting and 1% for Boolean RL (Table 3, p. 7). Inference: this is a search-and-training result, not evidence that symbolic feedback improves arbitrary theorem proving.

costs and implementation limits

The authors modified the TRL library to accept dense rewards and used PPO with LoRA on all linear attention and FFN layers (lora_r = 16, lora_alpha = 16) (Appendix D, p. 18). Symbolic checks are fast for RDKit retrosynthesis (0.003 s per generation) and SymPy arithmetic (0.002 s), but g++ takes about 0.5 s per generation; asynchronous Popen keeps code-synthesis overhead near one hour per 24-hour iteration (Section 3, p. 3; Appendix D, p. 18). Inference: Verus proof checking may be slower and should be batched or cached; the reward pipeline must record tool versions and diagnostics to make training reproducible.

The paper reports gains on five domain-specific tasks but explicitly limits its claim: “While we do not claim to improve general reasoning capabilities, RLSF leverages symbolic reasoning tools to improve downstream domain-specific tasks where syntax and semantics play a critical role.” (Section 7, p. 7). It identifies slow or resource-intensive symbolic tools as a limitation and suggests precomputed rewards or DPO-style alternatives (Section 7, p. 7). The environment, reasoner, certificate parser, reward mapping, and PPO implementation remain trusted engineering components; the model is not formally guaranteed to improve after training.

evidence and VL implications

The product-level threat is mislocalization: if diagnostics blame the wrong token, training reinforces a wrong correction. A second threat is treating a scalar pass result as a proof. Inference: VL should store the exact Verus command, source hash, verifier version, error spans, and proof status with every reward vector. The final Rust artifact must still pass Verus independently; RLSF should accelerate candidate generation rather than weaken the acceptance gate.

The paper’s strongest reusable result is an interface pattern: a sound checker emits structured, dense, local feedback, and reinforcement learning consumes it without differentiating through the checker. It does not provide Verus experiments, Rust ownership handling, concurrency reasoning, or guarantees about agent-written verified code. VL should adapt the certificate segmentation and reward design, then measure proof success per task and per verifier configuration.

techniques for the catalog

• certificate-driven PPO — run a symbolic checker on each response and convert its certificate into a token-aligned vector reward
• compiler and test localization — reward verified code spans and penalize spans named by compiler or test failures
• domain-rule token feedback — use algebra, chemistry, or protocol predicates to mark semantic violations at their responsible tokens
• formal-language segmentation — choose line, word, character, or parser-token boundaries that the reasoner can verify independently
• non-differentiable verifier training — keep the symbolic tool external to gradients while using its sound diagnostics for RL
• reward-cost engineering — parallelize expensive checks, cache certificates, or precompute rewards when verifier latency dominates

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15