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

Vishvesh Bhat; Asad Aali; Muhammad Ahmed Mohsin

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

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

Panel of Figure 1 — 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\,d$ on the training tasks, and keeps the best program (§ 3.4 ).

Subset	Format	Tasks	Train	Held aside	Kept traces
Retail	$\tau^{2}$ retail format, multi-turn tool matching	142	119	23	128
Telecom	$\tau^{2}$ telecom format, troubleshooting	178	122	56	178
Tool-search	LiveMCPBench format, tool search	233	183	50	233
Total		553	424	129	539

Table 1: The training set and the kept teacher traces.

	$\tau^{2}$ -Bench
System	Retail	Telecom	LiveMCP	Avg
Vanilla (chain-of-thought prompting)
Nemotron 3.5 Lightning	75.4	47.4	42.5	55.1
Nemotron 3 Nano	64.0	36.8	45.3	48.7
Nemotron 3 Super	79.8	51.8	34.4	55.3
SFT on the kept teacher traces

Table 2: Accuracy (%) by benchmark (pass@1 per run on

\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 .

			Student		Granite-4.2-8B
Student	Arm	Tasks	Output	Input	Calls	Output	Input
Nemotron 3.5 Lightning	Vanilla	278	2,323	45,907	–	–	–
	SFT	278	1,646	37,704	–	–	–
	GEPA	278	2,356	45,137	–	–	–
	ReAct	228	10,700	176,800	100	29,100	492,000
	Sample-and-judge	228	25,700	532,700	99	29,500	634,000

Table 3: Tokens per task, mean over the

\tau^{2}

-Bench evaluation runs, counted with each model’s own tokenizer. Vanilla, SFT, and GEPA rows pool the

\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 only	$7.7\times 10^{17}$	$7.7\times 10^{17}$	$3.1\times 10^{18}$
SFT, full sweep (24 runs)	$1.6\times 10^{19}$	$1.6\times 10^{19}$	$6.4\times 10^{19}$
PLVR search, Granite scoring, all three blocks	$3.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

Cluster	Kind	Size	Domains	#	Primitives
reason9	reason	24	telecom	14	Alternatives 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
message0	message	236	tool-search, retail, telecom	12	Audit, 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
reason17	reason	41	retail	12	Does 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
reason5	reason	117	tool-search, telecom	11	Alternatives 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
call5	call	128	tool-search	9	Device action arguments, Fill the parameters, Parts, Pick the function, Search phrases, Servers for the task, Split into requests, Widen tools, Write the reply
reason11	reason	102	telecom	8	Fill 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

Id	Rule	What the expert does
M01	Read before use	Reads a source before doing anything with its contents
M02	Complete answer	The final answer includes everything the task asked for
M03	Stop after answering	Takes no further action after the final answer
M04	Inputs before calculating	Retrieves all input values, then computes locally
M05	No tools for simple logic	Never searches for a tool to do arithmetic, parsing or filtering
M06	Gather before writing	Finishes all data gathering before writing an output

Appendix

Table 7

Rule	What the expert does
Identify first	Looks up the user before anything else
Target details first	Reads the target record’s details before target-specific work
Confirm the fix at the end	Runs the task’s success check to confirm the fix
Grant each permission	Grants each required permission separately
Clear the blocking state first	Clears a state that blocks everything else before other troubleshooting
Check detailed status	Reads detailed state on connectivity problems

Appendix

Table 8

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

ABACUS: Program-Guided Multistep Reasoning over Frozen Judgment Models
Oct 19, 2026Yuhao Wang, Zelin ZangStructured Reasoning in Language Models Efficient Language Model Reasoning
Westlake University · Hong Kong Institute of Science & Innovation, CAS · Tsientang Institute for Advanced Study
Instruction Retrieval at Inference Time for Small Language Models
Oct 15, 2025Kenan Alkiek, David Jurgens, Vinod VydiswaranKnowledge Augmentation for Language Models Small Language Models
School of Information University of Michigan Ann Arbor, MI 48109, USA
Training Language Models to Use Prolog as a Tool
Dec 8, 2025Niklas Mellgren, Peter Schneider-Kamp, Lukas Galke PoechReward Hacking Logical Reasoning
University of Southern Denmark

Oct 19, 2026J/K move · Enter open · S save

ABACUS: Program-Guided Multistep Reasoning over Frozen Judgment Models

Yuhao Wang, Zelin Zang

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

Structured Reasoning in Language Models Efficient Language Model Reasoning LLM-Based Program Synthesis Language Model Reasoning Evaluation

Open paper AskPDF arXiv

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.

Abstract

LLM Tool Use

Explore similar work

ABACUS: Program-Guided Multistep Reasoning over Frozen Judgment Models

Instruction Retrieval at Inference Time for Small Language Models

Training Language Models to Use Prolog as a Tool