NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect

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

purpose and claims

NeuroProlog combines language-model generation of Prolog with execution feedback and multi-task fine-tuning. “At inference, an execution-guided decoding pipeline with a five-class error taxonomy enables zero-shot iterative program repair without correction-specific training.” The authors train on a 200-entry mathematical knowledge base (KB), 310 problem-solving examples based on the KB, and 7,476 GSM8K-Prolog entries, then evaluate four models from 3B to 32B parameters on GSM8K (n=1,319) and a 239-problem numeric subset of MATH-500. They report final GSM8K accuracy, executability, initial success, correction rate, and average iterations.

The result is configuration-dependent. GPT-OSS-20B Cocktail FT reaches 88.34% GSM8K accuracy, from 84.91% base and 86.12% Prolog FT; the denominator is the 1,319-question GSM8K test set. Qwen2.5-Coder-32B Cocktail FT reaches 85.52% versus 80.29% base, while its initial execution falls from 96.4% to 90.7% and correction rises from 17.0% to 92.7%. Qwen3-8B is a counterexample: Cocktail accuracy 64.51% versus base 66.79%, with correction falling 70.7% to 24.1%. The text gives p = 0.08 for Qwen3-8B’s accuracy decrease (“Fine-tuning boosts initial success by 9× but sharply reduces correction, lowering overall accuracy (p = 0.08)”), so the drop is not significant at 0.05 in the paper’s own words; Table II marks Qwen3-8B Prolog FT with † (p<0.05) and leaves Cocktail FT unmarked. “Qwen3-8B is the only model where fine-tuning decreases accuracy, revealing a generation–correction trade-off.”

technique 1: build executable symbolic supervision

Use this when natural-language answers need a checkable intermediate representation. Construct each KB entry with a [KNOWLEDGE] instruction, a natural-language formula or inference rule, worked examples, and executable Prolog output. The output must include module imports, comments, type-safe predicates, helper predicates, compositional reasoning, and a standardized solve/1 interface. The paper’s KB has 200 entries spanning 11+ domains; mixed topics are 96 entries (48.0%), basic statistics 22 (11.0%), ratio/proportion and percentage 17 each (8.5%).

Construct the SOLVE set with [SOLVE] instructions, a word problem and numeric constraints, and a complete program whose solve(Result) produces the answer. Combine 310 new examples with 7,476 GSM8K-Prolog entries. Every entry is validated by SWI-Prolog parsing, execution tests for solve/1, and semantic review by domain experts and researchers. “A critical design choice distinguishes our KB from conventional code datasets: every Prolog predicate includes natural language comments that explain its mathematical semantics, enabling the model to bridge informal and formal reasoning.”

Verus form (Inference:). The analogous Verus corpus would pair a specification prompt with a Rust/Verus function, requires, ensures, and proof obligations, plus executable examples. Comments can explain predicate meaning, but comments are not evidence; verification must discharge assert and ensures. A spec fn can encode mathematical semantics, while an executable function returns the result. Prolog’s dynamic runtime diagnostics do not carry over directly; Verus failures are proof obligations or Rust execution errors.

technique 2: cocktail multi-task fine-tuning

Use this when a model must learn both reusable symbolic concepts and their application. Define D_KB with 200 KB pairs and D_SOLVE with 7,786 problem-solving pairs (310 plus 7,476). Optimize the weighted objective L_cocktail = λ_KB L_KB + λ_SOLVE L_SOLVE with λ_KB + λ_SOLVE = 1; each loss is causal-language-model likelihood. Train LoRA adapters in attention layers while freezing pretrained weights, without quantization. Use three epochs, cosine learning rate with 8% warmup, gradient clipping at 1.0, bfloat16, and effective batch size 32–64. Prefix examples with [KNOWLEDGE] or [SOLVE] so generation is task-conditional. LoRA rank, learning rate, and regularization are tuned per model scale; both fine-tuned configurations use identical LoRA hyperparameters and epochs. The paper does not state the value of λ_KB in the text read.

The paper hypothesizes three transfers: KB predicates become reusable SOLVE blocks, SOLVE usage reinforces KB semantics, and joint Prolog/CLP(Q) supervision induces shared type-safe representations. Verified answers are used only during evaluation to identify logically incorrect executable programs, not training. Evaluate with greedy decoding (temperature 0), the same three configurations (Base, Prolog FT, Cocktail FT), and McNemar tests against the same-model base.

Evidence: Cocktail improves GSM8K over base by +5.23 percentage points for Qwen-32B (80.29→85.52, p<0.01), +3.43 for GPT-OSS-20B (84.91→88.34, p<0.01), and +5.54 for Llama-3B (21.53→27.07, p<0.05). These are percentages over n=1,319, not percentages of repairs. Table IV compares Prolog FT to Cocktail FT and reports gains from +0.38 to +5.24 points across four models. MATH-500 uses n=239 and “No MATH-500 data was observed during training.” Table III (Cocktail FT versus Base) shows gains for three of four models (Qwen 40.17→42.68, GPT-OSS 49.37→51.46, Llama 9.10→10.04) and a drop for Qwen3 (30.96→21.34); the text separately says KB+SOLVE beats single-task Prolog FT on three of four models. Table III carries no significance marks. Inference: the +0.94 to +2.51 point gains on 239 problems are small and untested, so the conclusion’s “generalization to unseen problems” is weakly supported.

Verus form (Inference:). Multi-task training can generate Rust/Verus skeletons for a specification task and proof task, but Verus itself does not implement LoRA or Prolog. The verifier remains the external oracle: candidate code must compile and satisfy requires/ensures; generated proof text is accepted only after verification. The paper’s causal objective and model-scale effects do not establish Verus proof success.

technique 3: execution-guided repair with a five-class taxonomy

Use this when generated programs can be executed and diagnostics identify actionable failures. Given question q, generate P0 with fθ and run SWI-Prolog σ. On success with the correct answer, terminate. On success with a wrong answer, classify LOGICAL_ERROR (Logical, WRONG_ANSWER: the program executes but gives a different answer than the reference). On an error with a diagnostic, classify via the taxonomy: Syntax (malformed tokens/brackets), Type (arithmetic on non-numeric terms), Domain (runtime violations such as division by zero or negative factorial), or Instantiation (variables used before binding). The paper calls this a four-phase pipeline (Fig. 2). Its error-distribution figure (Fig. 5) uses finer labels such as SYNTAX_OPERATOR, UNDEF_PREDICATE, UNEXPECTED_EOF, EXEC_EXCEPTION and UNKNOWN, not only the five classes. Build a repair prompt containing q, the failed program, the error type, and fix instructions; generate P_i+1 and repeat at most k=3 iterations.

Measure executability (fraction with at least one valid execution), initial success (attempt-one solved), correction rate (initial failures eventually repaired), final accuracy (correct after ≤3 iterations), and average iterations. The paper reports that execution-guided repair gives Qwen-32B Cocktail 92.7% correction and reduces final failures from 39 to 9 versus the base model (the paper’s “77% reduction”). Inference: 39 and 9 match the 1,319-question run’s non-executable programs (100%−97.04% and 100%−99.32% executability), not wrong answers; wrong answers are far more numerous (final accuracy 85.52%). At 32B, base errors are 87.2% TYPE_ERROR and only 12% are repaired; after Cocktail, 55.6% are DOMAIN_ERROR and 96% are repaired. At 8B the inverse occurs: Qwen3-8B base errors are 89.4% SYNTAX_OPERATOR_EXPECTED, and after Cocktail the dominant error is 69.5% TYPE_ERROR with only 5% fixability. The paper reads this as a capacity threshold of about 10B parameters. Inference: with one model per scale from different families (Qwen2.5-Coder, GPT-OSS, Qwen3, Llama), model family and scale are confounded, so the threshold is a hypothesis; the paper lists controlled 1B–70B scaling as future work.

Verus form (Inference:). Replace SWI-Prolog execution with Verus verification and Rust tests. Classify diagnostics into parse/type errors, failed preconditions, failed postconditions, invariant failures, and wrong executable outputs. Feed the diagnostic and source back to the model, regenerate, and rerun verus. Use requires, ensures, loop invariant, assert, and proof fn only in proof context. A proof function cannot be called at runtime, and external_body would remove the very obligation being measured (Inference:).

what is proved, trusted, and relevant to VL

The reported gains are empirical benchmark results, not proofs of mathematical or software correctness. Inference: trusted components include SWI-Prolog, CLP(Q), curated KB semantics, domain review, GSM8K answer labels, model checkpoints, LoRA training, and the execution harness. The MATH-500 subset excludes imaginary-number, symbolic-equation, and geometric-construction problems because of CLP(Q) scope. The paper itself lists future comparison with SMT solvers and Lean, larger KBs, and 1B–70B scale studies. Inference: VL can reuse executable feedback and typed error taxonomies, but must treat specification and oracle quality as attack surfaces. Inference: an agent-written verified Rust product is threatened by a model learning to satisfy a malformed contract or by diagnostics that omit environmental and concurrency errors; Verus proof success alone does not validate the intended requirement. Inference: existing execution-guided program repair and symbolic supervision should be integrated rather than reimplemented as a Prolog clone.

techniques for the catalog

• executable symbolic dataset: pair natural-language concepts with commented, type-safe Prolog predicates and tested solve/1 programs
• cocktail fine-tuning: jointly train KB and problem-solving tasks with weighted causal losses and task prefixes
• execution-guided repair: execute generated code, classify five error types, prompt targeted fixes, and iterate up to three times
• diagnostic metrics: report executability, initial success, correction rate, final accuracy, and average iterations with explicit denominators Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The base model achieves 66.79% by compensating for poor initial generation (7.7% initial execution) through strong iterative repair (70.7% correction).”): read the whole paper text (arXiv:2603.02504v3) and checked every quotation, the dataset sizes and domain counts, the training protocol, Eq. 1, the pipeline and taxonomy description, Tables II to V, the MATH-500 numbers, and the limitations list against the study; changed the “newly constructed” wording, completed a truncated quotation, added the p = 0.08 caveat for Qwen3-8B, the per-scale LoRA tuning, the MATH-500 comparison and significance caveats, the pipeline outcome and taxonomy description, the reading of the 39 versus 9 failures as non-executable programs, the 8B base-error figure, and marked own conclusions “Inference:”; did not check the PDF figures beyond the extracted text, the cited references, or the released dataset and code; the arXiv link is the one on the paper text (arXiv:2603.02504).

Last edited: 2026-10-17