cs.AIOct 13, 2026

Compiling Expert Procedures into Verified Programs: When a Small Model Is Enough

Authors: Vishvesh Bhat, Asad Aali, Muhammad Ahmed Mohsin

Organizations: CoreThink AI · Stanford University

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

In procedural tool-use domains, how much of the gap between base models is procedure rather than capability? We build an explicit program from a teacher's traces and run it in front of unchanged small models, including an 8B model. The construction, PLVR , takes the reasoning traces of a teacher, Kimi-K3, clusters their segments to locate recurring operations, has a frontier model author one typed primitive per operation, each run by a small frozen model and assembles the program by A* search over a mined rule library, under a reference-action objective. At inference the program takes one of two forms: for troubleshooting and tool search it produces the chain of thought the student would otherwise generate for itself, and the student acts on it; for multi-turn tool matching the student proposes each action and the program checks, repairs, or retries it before it goes out. On the official tau2-Bench Retail and Telecom test sets and on LiveMCPBench, with three Nemotron base models and the same program for each, the answer depends on the domain. On Telecom, Granite-4.2-8B as the student goes from 43.0% to 91.2% under the program, and every Nemotron student reaches 93.3-94.4%, against at most 58.2% for fine-tuning on the same traces, prompt optimisation of the student, or two token-matched baselines. With Granite-4.2-8B as the student, the program is within 2 to 3 points of the Nemotron students on Telecom and within 3 on Retail, and 3 to 13 points below them on LiveMCPBench: where the domain is procedural an 8B student is enough, and on tool search the student still matters. On Retail and LiveMCPBench the program is competitive with the best baseline. The spread between base models shrinks from about 7 points to about 2, averaged over the suites, with no weights changed.

Figures & tables

Figure 1: Trace-guided program construction. (A) Each kept teacher trace is cut into segments typed as reason, call, message, or question. (B) Segments are clustered within kind; each cluster’s behaviours become primitives, each a single call to frozen Granite-4.2-8B with a typed input, an output schema, a deterministic verifier, and a fallback (§ 3.2 ). (C) From the same traces, code alone reads off the expert actions, and a program is scored by the distance between the actions it takes and the expert’s (§ 3.3 ). (D) A ∗ adds rules from a library mined from the traces, minimising f=∣P∣+100 df=|P|+100\,d on the training tasks, and keeps the best program (§ 3.4 ).
SubsetFormatTasksTrainHeld asideKept traces
Retailτ2\tau^{2} retail format, multi-turn tool matching14211923128
Telecomτ2\tau^{2} telecom format, troubleshooting17812256178
Tool-searchLiveMCPBench format, tool search23318350233
Total 553424129539
Table 1: The training set and the kept teacher traces.
 τ2\tau^{2} -Bench  
SystemRetailTelecomLiveMCPAvg
Vanilla (chain-of-thought prompting)
Nemotron 3.5 Lightning75.447.442.555.1
Nemotron 3 Nano64.036.845.348.7
Nemotron 3 Super79.851.834.455.3
SFT on the kept teacher traces
Table 2: Accuracy (%) by benchmark (pass@1 per run on τ2\tau^{2} -Bench): Retail 114 tasks, Telecom 114, LiveMCPBench 95. The program’s Telecom cells are means over three runs; all other cells, including the Granite-as-student row, are one run. The best arm per student and column is in bold. Averages are arithmetic means of the displayed cells. The SFT row is the one fine-tune per model of § 4.3 , trained on the kept teacher traces. GEPA rows optimise the student’s own prompt with no program. ReAct and sample-and-judge rows spend the program’s token budget on Granite-4.2-8B without the program (§ 4.3 ). PLVR rows run the final program of § 3.4 .
   StudentGranite-4.2-8B
StudentArmTasksOutputInputCallsOutputInput
Nemotron 3.5 LightningVanilla2782,32345,907–––
 SFT2781,64637,704–––
 GEPA2782,35645,137–––
 ReAct22810,700176,80010029,100492,000
 Sample-and-judge22825,700532,7009929,500634,000
Table 3: Tokens per task, mean over the τ2\tau^{2} -Bench evaluation runs, counted with each model’s own tokenizer. Vanilla, SFT, and GEPA rows pool the τ2\tau^{2} runs they were measured on (task counts shown); PLVR , ReAct, and sample-and-judge rows pool Retail and Telecom (228 tasks). For PLVR the student’s tokens and Granite-4.2-8B’s tokens (summed over the primitive calls in a task) are shown separately; for ReAct and sample-and-judge the Granite columns are the loop or the sampling and judging, and output includes reasoning tokens; their student columns are the student’s own calls under the loop or across the five samples. The program’s student output count is from Telecom, where it was counted exactly.
 Lightning (3B)Nano (3B)Super (12B)
SFT, selected run only7.7×10177.7\times 10^{17}7.7×10177.7\times 10^{17}3.1×10183.1\times 10^{18}
SFT, full sweep (24 runs)1.6×10191.6\times 10^{19}1.6×10191.6\times 10^{19}6.4×10196.4\times 10^{19}
PLVR search, Granite scoring, all three blocks3.0×10193.0\times 10^{19} (once)
PLVR rule mining (Claude Sonnet 4.5)16 calls, 287k prompt and 47k completion tokens (once; FLOPs not counted)
Table 4: Cost of producing each arm, in FLOPs. Fine-tuning is per student; the search is run once and its program is used by every student. The selected-run figure is the one fine-tune of Table 2 ; the sweep is all 24 runs that selection drew on.
Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

ClusterKindSizeDomains#Primitives
reason9reason24telecom14Alternatives when blocked, Can the question be answered, Device reply, Does the condition hold now, Is the condition met, Is the rule a condition, Is the rule about this action, Order requests, Plan steps, Price terms, Requests covered by the same call, Split into requests, User’s own premise or condition, Where a value comes from
message0message236tool-search, retail, telecom12Audit, Classify one request, Does the condition hold now, Is the condition true by the quote alone, Is the rule about this action, Order requests, Plan steps, Reply to a confirmation, Requests covered by the same call, Split into requests, Where a value comes from, Write the reply
reason17reason41retail12Does the condition hold now, Is the condition met, Is the condition true by the quote alone, Is the problem fixed, Is the request achieved, Is the rule about this action, Order requests, Plan steps, Reply to a confirmation, Requests covered by the same call, User’s own premise or condition, Where a value comes from
reason5reason117tool-search, telecom11Alternatives when blocked, Can the question be answered, Functions a policy section governs, Is the condition true by the quote alone, Is the rule about this action, Is the setting already as wanted, Plan steps, Price terms, Question for a missing parameter, User’s own premise or condition, Widen tools
call5call128tool-search9Device action arguments, Fill the parameters, Parts, Pick the function, Search phrases, Servers for the task, Split into requests, Widen tools, Write the reply
reason11reason102telecom8Fill the parameters, Functions a policy section governs, Is the rule about this action, Order requests, Plan steps, Question for a missing parameter, Requests covered by the same call, User’s own premise or condition
Appendix
Table 6
IdRuleWhat the expert does
M01Read before useReads a source before doing anything with its contents
M02Complete answerThe final answer includes everything the task asked for
M03Stop after answeringTakes no further action after the final answer
M04Inputs before calculatingRetrieves all input values, then computes locally
M05No tools for simple logicNever searches for a tool to do arithmetic, parsing or filtering
M06Gather before writingFinishes all data gathering before writing an output
Appendix
Table 7
RuleWhat the expert does
Identify firstLooks up the user before anything else
Target details firstReads the target record’s details before target-specific work
Confirm the fix at the endRuns the task’s success check to confirm the fix
Grant each permissionGrants each required permission separately
Clear the blocking state firstClears a state that blocks everything else before other troubleshooting
Check detailed statusReads detailed state on connectivity problems
Appendix
Table 8
More in this topic

LLM Tool Use

Large language model tool use studies how models select, call, and coordinate external tools to extend their reasoning and take actions.

See all 295 papers

Explore similar work

CardsList
Oct 19, 2026

ABACUS: Program-Guided Multistep Reasoning over Frozen Judgment Models

Judgment models answer semantic questions by scoring a finite set of candidate outcomes. Can reusable programs turn these local decisions into powerful multistep reasoning? We introduce \method, a framework that jointly constructs judgment schemas and composition programs for frozen judgment models. A generative teacher designs the procedure offline; the judgment model resolves local semantic questions online, and the saved program composes its decisions into an answer. We study three allocations of design effort between humans and the teacher, focusing on construction through a shared interface. We instantiate the framework with Kev. On three selected BIG-Bench Hard tasks, nine independently constructed programs solve all 450 executions of 150 development inputs. A separate deployment study freezes three programs after development-set reference-agreement refinement and evaluates them on 600 held-out questions. These programs achieve near-perfect 99.67% macro accuracy, versus 64.00% for direct Kev and 68.80% for final-answer-only Qwen3.5-4B. They attain comparable observed accuracy to Qwen's unrestricted response policy (99.07%) with an 8.43-fold online speedup: 0.255 versus 2.150 seconds per question. These results show how reusable programs can substantially expand the reasoning capability of a compact judgment model while keeping its parameters fixed.

Yuhao Wang, Zelin Zang

Westlake University · Hong Kong Institute of Science & Innovation, CAS · Tsientang Institute for Advanced Study

Structured Reasoning in Language ModelsEfficient Language Model ReasoningLLM-Based Program SynthesisLanguage Model Reasoning Evaluation
AskPDF
Oct 15, 2025

Instruction Retrieval at Inference Time for Small Language Models

The facts a language model stores are tied to its parameter count, so small models that fit on edge devices fail on expert problems, which need specialized knowledge and follow multi-step procedures. Fine-tuning for a specific domain or task writes the knowledge into the parameters but must be repeated for every model and domain, and a retrieved passage leaves the model to find the relevant fact and apply it on its own. We introduce instruction retrieval, which distills a teacher model's expertise into a corpus of instructions tailored so that a small model can follow. For each cluster of a domain's problems, the teacher writes one instruction with the background knowledge the cluster depends on, a procedure for that kind of problem, and the common mistakes made on it. This reusable corpus needs only to be built once per domain and requires no run-time teacher access. At inference, a frozen small model retrieves the instructions nearest its question and follows them, with no fine-tuning. Across medicine, law, and mathematics benchmarks, we demonstrate the corpus improves over zero-shot on every task and over few-shot prompting, self-consistency, and other retrieved text on medicine and law. On MedQA the corpus raises mean accuracy by 10.6 points, where retrieved textbook passages raise it by 3.9 and few-shot examples from the same teacher lower it. An error analysis shows that only the background knowledge fixes the questions a small model always gets wrong, and that the procedure and common mistakes fix only the questions where it wavers between options. Our results show that automatically retrieved inference-time procedural guidance and domain knowledge can yield substantial gains for small models.

Kenan Alkiek, David Jurgens, Vinod Vydiswaran

School of Information University of Michigan Ann Arbor, MI 48109, USA

Knowledge Augmentation for Language ModelsSmall Language ModelsKnowledge-Intensive QA
AskPDF
Dec 8, 2025

Training Language Models to Use Prolog as a Tool

Language models frequently produce plausible yet incorrect reasoning traces that are difficult to verify. We investigate fine-tuning models to use Prolog as an external symbolic reasoning tool, training Qwen2.5-3B-Instruct with Group Relative Policy Optimization (GRPO) on a cleaned version of GSM8K (which we release as gsm8k-prolog-prover). We systematically vary prompt structure, reward composition (execution, syntax, semantics, structure), and inference protocol (single-try, multiple-try, and two agentic modes). Our reinforcement learning approach outperforms supervised fine-tuning on GSM8K, and the resulting 3B model achieves zero-shot performance on MMLU-STEM and MMLU-Pro competitive with 7B few-shot baselines. Most importantly, we identify an accuracy--auditability trade-off: configurations tuned for correctness alone learn to delegate reasoning to natural language and use Prolog only for the final computation, while configurations rewarded for symbolic structure produce fully auditable programs at a cost in accuracy. We interpret this trade-off as a form of reward hacking and discuss its implications for deploying neurosymbolic systems in safety-critical domains. The source code for our experiments is available under https://github.com/aisilab/Prolog-as-a-Tool

Niklas Mellgren, Peter Schneider-Kamp, Lukas Galke Poech

University of Southern Denmark

Reward HackingLogical ReasoningRL for Language Model ReasoningSymbolic ReasoningLLM Tool UseSymbolic Reasoning in Language Models
AskPDF