Systems resource management tasks rely primarily on hand-designed heuristics. However, growing hardware heterogeneity and workload diversity require heuristics specialized to particular deployment instances, making manual design expensive and difficult to scale. In this paper, we explore how to synthesize systems heuristics using LLMs. The main challenge is ensuring that generated heuristics execute safely, integrate correctly with the surrounding system, and still achieve strong performance. We propose Vulcan, a framework that identifies LLM-friendly interfaces that isolate core decision logic from the rest of the implementation. With Vulcan, LLM-generated code is restricted to simple stateless decision functions, while trusted runtime abstractions provide rich derived statistics for meaningful policy exploration without system-integration bugs. To ensure execution safety, LLMs synthesize heuristics in a restricted language, Anvil, that guarantees important properties by construction. We evaluate Vulcan across three well-studied domains and demonstrate up to 4.9× higher savings for spot-VM scheduling, up to 2× lower miss ratios for cache eviction, and up to 14% higher application performance for tiered-memory systems, while ensuring execution safety throughout.
Figures & tables
Figure 1 . Count of CloudPhysics traces where each heuristic performs best (max. object hit rate). Tiny, small, and large imply cache sizes of 0.1%, 1%, and 10% of trace footprint. Heatmap showing, for each cache size, the number of CloudPhysics traces on which each cache-eviction algorithm achieves the highest object hit rate. Rows correspond to tiny, small, and large caches, equal to 0.1%, 1%, and 10% of the trace footprint, respectively; columns correspond to ARC, QDLP, LIRS, TwoQ, S3-FIFO, and other algorithms. The winning algorithm varies substantially across traces and cache sizes: ARC performs best most often for tiny caches, while LIRS performs best most often for large caches, and no single eviction policy is best across all instances.
Figure 2 . Illustration of three design alternatives. Unconstrained LLM edits result in execution safety and systems integration concerns ( §2.2.1 ); overly constrained synthesis fails to achieve good performance ( §2.2.2 ). Vulcan attempts to satisfy all three. Radar chart comparing three approaches to LLM-based heuristic synthesis across performance, execution safety, and systems integration. Unconstrained LLM edits score highly on performance but poorly on execution safety and systems integration; an LLM with a narrow interface scores highly on execution safety and systems integration but poorly on performance; Vulcan is designed to achieve high performance while also preserving execution safety and systems integration.
Figure 3 . Overview of Vulcan . Users provide task-specific inputs – a template, a prompt, and an evaluator. Vulcan uses a code-generation framework to produce a safe and performant heuristic. Overview of the \systemworkflow. The user provides a heuristic template, evaluator, and natural-language prompt. The template uses \libsysteminterfaces, operators, and listeners. A code-generation framework uses these inputs to synthesize candidate heuristics in the \dslDSL, which checks their safety. Candidate heuristics are evaluated iteratively, and Vulcan returns the final heuristic to the user.
Figure 4 . Typical components of systems heuristics (using memory tiering as an example). Vulcan impacts the colored parts; icons show the division of responsibility among developers, libVulcan , and LLMs. Diagram showing the division of responsibility in a memory-tiering heuristic. At the top, the high-level memory-tiering task is decomposed into memory allocation, page placement, and page migration; page migration is expanded into five components connected in sequence. The uncolored components – task decomposition, triggers, raw-signal collection, and the migration mechanism – are developer-managed. The colored components are those modified by \system: the feature store is managed by \libsystem, while the decision logic is synthesized by the code-generation framework. Icons beside each component indicate the responsible party: developer, \libsystem, or code-generation framework.
Policy
Description
Type
Congestion control ( Ha et al., 2008 )
Decide the number of unacknowledged bytes in flight ( cwnd ).
Value : compute the cwnd .
DVFS control ( Pillai and Shin, 2001 )
Decide cpu_freq to balance performance & power.
Value : compute the frequency.
Cluster autoscaling ( Kubernetes, [n. d.] )
Decide n_replicas to provision for a given service.
Value : compute replicas per service.
Hardware prefetching ( Michaud, 2016 )
Choose an offset from the current access to prefetch data.
Value : compute the offset value.
Cache eviction ( Song et al., 2020 )
Select which cached object(s) to evict.
Rank : all cached objects.
CPU scheduling ( Pabla, 2009 )
Select which thread to schedule next.
Rank : all runnable threads.
Table 1 . Examples of systems resource management tasks and the type of task ( Value or Rank ) they fall into.
Listener
Query API(s)
State and data structures
Complexity
Update
Query
Space
Average()
get_avg
sum , count
O(1)
O(1)
O(1)
MinMax()
get_min , get_max
min , max
O(1)
O(1)
O(1)
RollingWindow(N)
get_kth , get_avg
ring buffer, sum
O(1)
O(1)
O(N)
EWMA( {α0,α1,…αM} )
get_ewma (α)
current EWMA value for each α
O(1)
O(1)
O(1)
RollingPercentile(N)
get_percentile
ring buffer, ordered multiset ( Ami Tavory and Vladimir Dreizin and Benjamin Kosnik, [n. d.] )
O(logN)
O(logN)
O(N)
Table 2 . Listeners provided by libVulcan . The table shows the state each listener maintains, with update/query/space complexities. The first six rows show listeners for temporal aggregates, while the bottom two show listeners for aggregates across the object population.
ID
Property
P1
Memory safety. No out-of-bounds access, use-after-free, or double-frees .
P2
Leak freedom. No unbounded memory growth over time.
P3
Termination. Must not run indefinitely; LLM scoring functions are guaranteed to eventually terminate.
Table 3 . Execution-safety properties guaranteed by Anvil .
Use case
Baselines
Metric
Evaluator
Spot VM scheduling (single)
Greedy, Uniform Progress ( Wu et al., 2024 ) , ADRS ( Cheng et al., 2025 )
Avg. USD saved
Simulator, 5% sample
Spot VM scheduling (multi)
Round-robin uniform progress, ADRS ( Cheng et al., 2025 )
Avg. USD saved
Simulator, 5% sample
Cache eviction
Nine state-of-the-art algorithms
Object miss-ratio reduction (MRR)
Simulator, 1M requests
Memory tiering
ARMS ( Yadalam et al., 2025 )
Goodput, latency
Emulator, per-workload
Table 4 . Summary of use cases, baselines, evaluation metrics, and evaluators.
Figure 5 . Comparison of schedulers for the single-region spot VM setting . (a) Mean savings; higher is better. (b) Big losses/gains exceed 10;smalllosses/gainsarebelow10. Two panels compare schedulers for the single-region spot-VM setting. The first reports average USD savings per scenario relative to the greedy baseline: $1.46 for UP, $4.31 for ADRS, $2.72 for Vulcan-NL, and $7.12 for Vulcan. The second reports the distribution of savings for UP and Vulcan across four categories. UP has 22% big losses, 30% small losses, 25% small gains, and 24% big gains; Vulcan has 1% big losses, 36% small losses, 39% small gains, and 24% big gains. Vulcan therefore achieves substantially higher average savings while nearly eliminating big losses relative to UP.
Figure 6 . Vulcan vs. unconstrained search (ADRS). Lines: best-performing-heuristic so far; dots: individual candidates. Plot comparing Vulcan and unconstrained ADRS over 100 synthesis iterations. The horizontal axis is iteration number and the vertical axis is heuristic cost, where lower is better. Faint points show the costs of individual candidates and step lines show the best cost found so far. The two methods make similar progress during roughly the first 20 iterations, reaching best costs near 95 on the Y axis. Vulcan then improves more quickly, dropping to about 92 by iteration 25 and about 90 by iteration 60, while ADRS remains around 94 until roughly iteration 60 and finishes near 92. Vulcan therefore reaches its best solutions earlier and ends with a lower best cost than ADRS.
Use case
Tokens (millions)
API cost
Time
Input
Output
Spot VM (single)
2.2
0.20
$11
2.5 h
Spot VM (multi)
1.0
0.12
$5
1.2 h
Cache eviction †
0.7–2.0
0.15–0.50
$5–15
2.4–4.4 h
Memory tiering †
1.6–2.2
0.23–0.36
$10–14
1.9–3.0 h
Table 5 . Cost of heuristic synthesis with Vulcan .
Figure 7 . Average workload cost per scenario (lower is better). Grouped bar chart comparing average workload cost for UP-RR, ADRS, and Vulcan across six multi-region scheduling scenarios (S1–S6), plus the average across all scenarios; lower cost is better. In S1 and S4, all three methods are close, at roughly $140 per workload. In S2, Vulcan is lowest at about $50, compared with roughly $55 for ADRS and $60 for UP-RR. In S3, ADRS is lowest at about $60, followed by Vulcan at about $68 and UP-RR at about $80. In S5 and S6, Vulcan and ADRS are both near $50–55, substantially below UP-RR at roughly $90 and $60, respectively. Averaged across all scenarios, Vulcan and ADRS are both around $85, while UP-RR is around $95.
Feature type
Attributes
Per-object ( fi )
Access count, last access timestamp, insertion timestamp, size (bytes)
Global ( X )
Current time, recently evicted object IDs (ghost list).
Table 6 . Raw signals for cache-eviction scoring.
Figure 8 . Performance of instance-specialized heuristics versus baselines for two classes of instances. Additional results appear in Appendix B . Two scatter plots compare miss-ratio reduction relative to FIFO for Vulcan, Vulcan without listeners, and nine baseline cache-eviction algorithms across eight workload traces; farther right indicates a larger reduction in miss ratio and therefore better performance. The top-to-bottom trace order is WikiMedia CDN, Twitter KV2, Twitter KV1, Tencent Object, Meta Block, Meta KV, Meta CDN, and MSR Block. The first plot uses a large cache equal to 10% of the trace footprint, while the second uses a small cache equal to 0.1%. For the large-cache setting, Vulcan is best on Meta Block, approximately matches the best baseline on Meta CDN, and is close to the best result on MSR Block. For the small-cache setting, Vulcan approximately matches the best baseline on Tencent Object and is close to the best result on MSR Block. Across traces, the identity of the best-performing algorithm varies substantially.
Algorithm
Execution time vs. FIFO
LRU
1.0 × (0.5–2.1 × )
SIEVE ( Zhang et al., 2024 )
1.1 × (0.6–2.0 × )
LeCaR ( Vietri et al., 2018 )
1.8 × (0.8–3.0 × )
S3-FIFO ( Yang et al., 2023b )
2.1 × (1.4–3.8 × )
GDSF ( Cherkasova, 1998 )
3.9 × (2.5–7.1 × )
Cacheus ( Rodriguez et al., 2021 )
4.1 × (2.3–7.9 × )
Table 7 . Computational cost of eviction heuristics. Average (and range) of execution time to run a set of traces (scenarios) in a single-threaded simulator. Higher = more expensive.
Figure 9 . Performance of the Vulcan -synthesized heuristic compared with the no-op seed heuristic. Bar chart comparing the no-op seed heuristic and the Vulcan-synthesized heuristic across GapBC, GapPR, GUPS, and Silo, with performance normalized to ARMS; the dashed horizontal line at 1.0 represents ARMS performance. The no-op seed achieves approximately 0.68, 0.76, 0.95, and 0.65 times ARMS performance on GapBC, GapPR, GUPS, and Silo, respectively. The synthesized heuristic achieves approximately 1.00, 1.02, 1.14, and 1.01 times ARMS performance, respectively. Error bars show variability across runs.
Figure 10 . Generalization of Vulcan -synthesized heuristics. Heatmap showing how three Vulcan-synthesized heuristics generalize across four workloads, with each cell reporting performance normalized to ARMS. Columns are GapBC, GapPR, GUPS, and Silo. Vulcan-GapBC achieves 0.96, 1.01, 1.02, and 1.02 times ARMS performance, respectively. Vulcan-GUPS achieves 1.00, 1.02, 1.14, and 1.01 times ARMS performance. Vulcan-Silo achieves 0.96, 1.02, 1.02, and 1.01 times ARMS performance. Thus, the synthesized heuristics generally match or exceed ARMS, with the largest improvement, 1.14 times, occurring for Vulcan-GUPS on GUPS.
Metric
Spot VM
Spot VM
Cache
Memory
(single)
(multi)
eviction
tiering
Raw signals
8
11
6
3
Template (LoC)
62
104
74
72
Table 8 . Developer effort to set up templates.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 11 . Evolutionary search with a simple agent vs. Claude Code. The dotted line represents the start of a new iteration; every iteration is seeded with samples of the best-performing programs so far to help guide the search. Side-by-side workflow diagrams comparing basic evolutionary search with a Claude Code agent. In basic evolution, a prompt is sent to Claude to generate a heuristic, which is built and evaluated; build or runtime errors are returned to Claude for correction, while successful heuristic scores are stored and used to seed later iterations. In the Claude Code workflow, the prompt is given to a Claude Code agent that can repeatedly inspect and modify the codebase and invoke tools including evaluation, Bash, and grep before producing a heuristic. The resulting heuristic is then built and evaluated, and its score is stored for use in subsequent iterations. Dotted boundaries indicate individual evolutionary iterations.
Figure 12 . Performance of instance-specialized heuristics versus baselines for two classes of instances. Two scatter plots compare miss-ratio reduction relative to FIFO for Vulcan, Vulcan without listeners, and nine baseline cache-eviction algorithms across eight workload traces where all cached objects have the same size; farther right indicates a larger reduction in miss ratio and therefore better performance. The first plot uses a large cache equal to 10% of the trace footprint, while the second uses a small cache equal to 0.1%. For the large-cache setting, improvements vary substantially by trace: several methods achieve reductions above 0.2 on WikiMedia and Twitter workloads, while gains are much smaller on Meta CDN and MSR Block. For the small-cache setting, most methods cluster near zero on several traces, but larger improvements appear on Twitter KV2, Meta KV, and WikiMedia CDN. As in the different-object-size experiments, the best-performing algorithm varies across traces and cache sizes.
LLMs have shown impressive success in program synthesis, discovering programs that surpass prior solutions. However, these approaches rely on simple numeric scores to signal program quality, such as the value of the solution or the number of passed tests. Because a score offers no guidance on why a program failed, the system must generate and evaluate many candidates hoping some succeed, increasing LLM inference and evaluation costs. We study a different approach: property-guided LLM program synthesis. Instead of scoring programs after evaluation, we check whether a candidate satisfies a formally defined property. When the property is violated, we stop the evaluation early and provide the LLM with a concrete counterexample showing exactly how the program failed. This feedback drastically reduces both the number of program generations and the evaluation cost, and can guide the LLM to generate stronger programs. We evaluate this approach on PDDL planning domains, asking the LLM to synthesize direct heuristic functions: every state reachable by strictly improving transitions has a strictly improving successor. A heuristic with this property leads hill-climbing algorithm directly to a goal state. A counterexample-guided repair loop generates one candidate program, checks the property over a training set, and returns the first case that violates the property. We evaluate our approach on ten planning domains with an out-of-distribution test set. The synthesized heuristics are effectively direct on virtually all test tasks, and compared to the best prior generation method our approach generates seven times fewer programs per domain on average, solves more tasks without using search, and requires several orders of magnitude less computation to evaluate candidates. Whenever a problem admits a verifiable property, property-guided LLM synthesis can reduce cost and improve program quality.
André G. Pereira, Augusto B. Corrêa, Jendrik Seipp
Federal University of Rio Grande do Sul · Brazil · University of Oxford +3
Verification is becoming central to both reinforcement-learning-based training and inference-time control of large language models (LLMs). Yet current verifiers face a fundamental trade-off: LLM-based verifiers are expressive but hard to control and prone to error, while deterministic executable verifiers are reliable and interpretable but often limited in capability. We study the following question: given a development set of LLM outputs and labels for a target objective, such as correctness, can we automatically induce a minimal set of Python verifiers whose joint satisfaction closely matches that objective? We propose AutoPyVerifier, a framework that uses an LLM to synthesize candidate verifier functions and then refines them through search over a directed acyclic graph (DAG). By navigating the DAG, AutoPyVerifier systematically explores the space of deterministic executable verifiers and selects a compact verifier set whose joint satisfaction best approximates the target objective. Across mathematical reasoning, coding, function calling, and instruction-following benchmarks for several state-of-the-art LLMs, AutoPyVerifier improves target-objective prediction by up to 55.0 F1 points over the initial LLM-generated verifier sets. Additional analyses show that the most useful verification targets vary by benchmark and model, and that the DAG-based search shifts the learned verifier sets toward more structural and semantically grounded checks. We further show that exposing the discovered verifier set to an LLM as an external tool improves downstream accuracy by up to 17.0 points. We release our code
LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)ânotoriously difficult to formalise for verificationâit becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.