Paper deep dive

LLM-Driven Heuristic Synthesis for Industrial Process Control: Lessons from Hot Steel Rolling

Nima H. Siboni, Seyedreza Kiamousavi, Emad Scharifi

Year: 2026Venue: arXiv preprintArea: cs.AIType: PreprintEmbeddings: 54

Intelligence

Status: succeeded | Model: anthropic/claude-sonnet-4.6 | Prompt: intel-v1 | Confidence: 94%

Last extracted: 3/24/2026, 3:34:02 AM

Summary

This paper presents an LLM-driven heuristic synthesis framework for hot steel rolling process control, where a language model (Gemini 2.5 Pro) iteratively proposes and refines human-readable Python controllers using feedback from a physics-based simulator (PyRoll). Key contributions include: (1) an auditable controller-synthesis pipeline with formal safety/monotonicity verification via Z3 SMT, and (2) a Luby-style universal restart budget allocation strategy that achieves near-optimal performance in 160 iterations versus 730 iterations for ad-hoc runs. The best LLM-generated heuristic achieves 30% improvement over a hand-coded baseline, with significant gains in temperature and grain size control.

Entities (27)

Emad Scharifi · person · 99%Gemini-2.5-pro · ai-model · 99%Hot Steel Rolling · application-domain · 99%Nima H. Siboni · person · 99%Seyedreza Kiamousavi · person · 99%Google DeepMind · organization · 98%Institute of Metal Forming, RWTH Aachen · organization · 98%Juna.ai · organization · 98%LLM-Driven Heuristic Synthesis Framework · method · 98%Luby-Style Universal Restarts · algorithmstrategy · 98%PyRoll · softwaresimulator · 98%Z3 SMT Solver · software-tool · 97%Automated Audit Pipeline · methodcomponent · 96%FlatRollingEnv · software-component · 95%Gymnasium · software-framework · 95%Height Reduction Control · control-variable · 95%Interpass Time Control · control-variable · 95%Rolling Velocity Control · control-variable · 95%S355 Steel · material · 95%Greedy Portfolio Construction · method · 93%Thermomechanical Controlled Processing (TMCP) · domain-concept · 93%Decoupled Controller Architecture · methodarchitecture · 92%Luby et al. 1993 · publication · 92%Liu et al. 2024 · publication · 90%Romera-Paredes et al. 2024 · publication · 90%Weiner et al. 2023 · publication · 90%Ye et al. 2024 · publication · 90%

Relation Signals (21)

Nima H. Siboni → affiliatedwith → Juna.ai

confidence 99% · Nima H. Siboni ∗1 , Juna.ai, Kastanienallee 32, 10435 Berlin

Seyedreza Kiamousavi → affiliatedwith → Institute of Metal Forming, RWTH Aachen

confidence 99% · Seyedreza Kiamousavi 2 , Institute of Metal Forming, RWTH Aachen

Emad Scharifi → affiliatedwith → Institute of Metal Forming, RWTH Aachen

confidence 99% · Emad Scharifi 2 , Institute of Metal Forming, RWTH Aachen

LLM-Driven Heuristic Synthesis Framework → appliedto → Hot Steel Rolling

confidence 99% · We study an LLM-driven heuristic synthesis framework for hot steel rolling

Gemini-2.5-pro → developedby → Google DeepMind

confidence 99% · Gemini 2.5 Pro [Google DeepMind, 2025]

LLM-Driven Heuristic Synthesis Framework → uses → Gemini-2.5-pro

confidence 99% · We use Gemini 2.5 Pro [Google DeepMind, 2025] via the Google Generative AI API with function calling.

LLM-Driven Heuristic Synthesis Framework → uses → PyRoll

confidence 98% · The environment, FlatRollingEnv, wraps the PyRoll physics simulator [Weiner et al., 2023]

FlatRollingEnv → wraps → PyRoll

confidence 98% · The environment, FlatRollingEnv, wraps the PyRoll physics simulator [Weiner et al., 2023] in a Gymnasium-compatible interface

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Industrial process control demands policies that are interpretable and auditable, requirements that black-box neural policies struggle to meet. We study an LLM-driven heuristic synthesis framework for hot steel rolling, in which a language model iteratively proposes and refines human-readable Python controllers using rich behavioral feedback from a physics-based simulator. The framework combines structured strategic ideation, executable code generation, and per-component feedback across diverse operating conditions to search over control logic for height reduction, interpass time, and rolling velocity. Our first contribution is an auditable controller-synthesis pipeline for industrial process control. The generated controllers are explicit programs accessible to expert review, and we pair them with an automated audit pipeline that formally verifies key safety and monotonicity properties for the best synthesized heuristic. Our second contribution is a principled budget allocation strategy for LLM-driven heuristic search: we show that Luby-style universal restarts -- originally developed for randomized algorithms -- transfer directly to this setting, eliminating the need for problem-specific budget tuning. A single 160-iteration Luby campaign approaches the hindsight-optimal budget allocation derived from 52 ad-hoc runs totalling 730 iterations.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

53,885 characters extracted from source content.

Expand or collapse full text

LLM-Driven Heuristic Synthesis for Industrial Process Control: Lessons from Hot Steel Rolling Nima H. Siboni ∗1 , Seyedreza Kiamousavi 2 , and Emad Scharifi 2 1 Juna.ai, Kastanienallee 32, 10435 Berlin , nima@juna.ai 2 Institute of Metal Forming, RWTH Aachen, Intzestr. 10, 52072 Aachen , Seyedreza.kiamousavi,emad.scharifi@ibf.rwth-aachen.de ∗ Corresponding author Abstract Industrial process control demands policies that are inter- pretable and auditable, requirements that black-box neural policies struggle to meet. We study an LLM-driven heuristic synthesis framework for hot steel rolling, in which a language model iteratively proposes and refines human-readable Python controllers using rich behavioral feedback from a physics- based simulator. The framework combines structured strategic ideation, executable code generation, and per-component feed- back across diverse operating conditions to search over control logic for height reduction, interpass time, and rolling veloc- ity. Our first contribution is an auditable controller-synthesis pipeline for industrial process control. The generated con- trollers are explicit programs accessible to expert review, and we pair them with an automated audit pipeline that formally verifies key safety and monotonicity properties for the best synthesized heuristic. Our second contribution is a principled budget allocation strategy for LLM-driven heuristic search: we show that Luby-style universal restarts—originally developed for randomized algorithms—transfer directly to this setting, eliminating the need for problem-specific budget tuning. A single 160-iteration Luby campaign approaches the hindsight- optimal budget allocation derived from 52 ad-hoc runs totalling 730 iterations. 1 Introduction Hot steel rolling is a multi-pass sequential decision problem in which a heated slab is progressively reduced in thickness through a series of rolling passes. At each pass, the operator must choose a height reduction, an interpass waiting time, and a rolling velocity—balancing competing objectives including dimensional accuracy, metallurgical quality (grain size, temper- ature), equipment constraints, and process efficiency. Industrial pass schedules are traditionally designed by experienced engi- neers using empirical rules and iterative simulation, limiting adaptability to new product specifications. Reinforcement learning (RL) can learn effective policies for such problems, but the resulting neural networks are opaque: a domain expert cannot inspect why a particular action was chosen, making deployment in safety-critical settings difficult. One-shot code generation by large language models (LLMs) offers interpretability but lacks the iterative refinement needed for complex multi-objective control. Recent work on LLM-driven heuristic search [Romera- Paredes et al., 2024, Liu et al., 2024, Ye et al., 2024] has shown that iterative code generation can discover effective strategies in combinatorial domains. We present a case study applying this paradigm to industrial process control, where interpretability and safety auditability are first-class require- ments. The main contribution is a case study with practical design lessons about auditable heuristic synthesis and restart budgeting, rather than a comprehensive benchmark against all alternative control methods. Our contributions are: 1.A search loop with rich behavioral feedback—per- component reward decompositions across diverse operating conditions—rather than scalar fitness, enabling rapid con- vergence to competent control policies. 2.A budget allocation analysis across 52 independent runs on a physics-based hot rolling simulator, showing that splitting a fixed budget into several short runs outperforms a single long run, and a Luby-style universal restart strategy that operationalises this finding without requiring retrospective analysis. 3.A five-layer automated audit pipeline that checks each generated heuristic against domain-grounded safety, mono- tonicity, responsiveness, and consistency specifications— formally proving key safety properties via Z3 SMT and verifying the remainder through property-based testing— bridging the gap between human-readable code and deployment-oriented verification evidence. 2 Method 2.1 Problem Formulation We formulate hot rolling pass schedule design as an episodic control problem. The environment, FlatRollingEnv, wraps the PyRoll physics simulator [Weiner et al., 2023] in a Gymnasium-compatible interface [Towers et al., 2024]. The 1 arXiv:2603.20537v1 [cs.AI] 20 Mar 2026 state is a 10-dimensional vector comprising the current and target thickness, grain size, and temperature, plus rolling force, torque, height reduction (HR) limit, and step count. The action space has three components: height reduction (0–50 m in 0.1 m steps, 501 levels), interpass time (1–120 s, 121 levels), and rolling velocity (7 discrete levels). Episodes terminate when the target thickness is reached or after 25 passes. Each candidate heuristic is a deterministic Python function: def heuristic(info: dict, action_mask: dict) -> list[int] receiving the physical state and a validity mask that constrains actions to physically feasible values. Heuristics execute in a sandboxed environment restricted to numpy and math. The reward function has five components per step: (1) a step penalty (−5.0) encouraging efficiency, (2) a grain size progress bonus with asymmetric penalties for undershooting, (3) a height reduction efficiency bonus (0–10) rewarding use of equipment capacity, and terminal bonuses for (4) grain size accuracy (0–25) and (5) temperature accuracy (0–25). Performance during search is measured as the mean total reward across 8 search feedback scenarios spanning four axes of variation: thickness targets, grain size targets, equipment limits, and temperature targets. These same scenarios provide the per-component behavioral feedback that guides the LLM’s refinement at each iteration. 2.2 Search Algorithm The search proceeds over푁outer iterations, each consisting of four phases (Figure 1 shows the resulting reward trajectories across runs): Phase 1: Strategic Ideation. The LLM generates푘=3 distinct strategy proposals in natural language, each addressing reduction scheduling, interpass timing, velocity strategy, grain size management, and the roughing-to-finishing transition. This separation of strategic reasoning from code prevents premature commitment to implementation details. Phase 2: Idea Selection. The LLM selects the most promising strategy with a justification grounded in the multi- objective reward structure. Phase 3: Implementation. The LLM implements the se- lected strategy as executable Python via a tool-calling interface. Failed compilations or runtime crashes trigger up to 3 repair attempts. Phase 4: Evaluation and Feedback. The heuristic is executed across all 8 scenarios. For each scenario, the system returns the total reward, step count, completion status, final state errors, per-component reward breakdowns, and action mask violations. This rich behavioral feedback—rather than a single scalar fitness—enables the LLM to diagnose which reward components underperform and in which operating conditions. Adaptive mode selection. The framework employs three modes: Exploration (no incumbent best—generate from scratch, informed by the top-푁best and last-푀recent heuristics), Refinement (incumbent exists, stagnation below threshold—propose targeted single-variable modifications to Table 1: Search configuration. ParameterValue LLM modelGemini 2.5 Pro Temperature0.7 Outer iterations per run1–30 Independent runs52 Ideas per iteration3 Repair attempts per heuristic3 Evaluation scenarios8 Max episode length25 passes Stagnation threshold6 iterations Conversation compactionmax 25, keep 10 the weakest reward component), and Radical Exploration (stag- nation exceeds threshold—demand fundamentally different strategies). When the conversation exceeds a length threshold, older messages are replaced by an LLM-generated summary (produced by the same Gemini 2.5 Pro model) that preserves strategies attempted, their results, key errors, and learnings; the most recent messages are retained verbatim. 2.3 LLM Configuration We use Gemini 2.5 Pro [Google DeepMind, 2025] via the Google Generative AI API with function calling. The sys- tem prompt includes the complete environment and reward function source code alongside structured domain knowl- edge on S355 steel hot rolling metallurgy. Two tools are exposed:read_filefor inspecting source code and suggest_a_heuristicfor submitting candidate implemen- tations. 3 Experimental Setup We conduct 52 independent search runs with the configuration in Table 1, totalling 730 iterations (mean 14.0 per run, range 1–30). For the budget allocation analysis, we use all available data. The 8 search feedback scenarios span four axes of variation: (1) two thickness specifications (80→12 m and 120→8 m), (2) two grain size targets (10휇m and 15휇m), (3) two equipment limits (HR limit 20 m and 50 m), and (4) two temperature targets (±50 K from nominal). A heuristic’s primary metric during search is the mean reward across these 8 scenarios; the secondary metric is the completion rate (fraction of scenarios reaching target thickness). For generalization evaluation, we additionally test on a held-out grid of 81 scenarios constructed from the full combinatorial product of these axes (§4.5). A typical 30-iteration run completes in approximately 38 min- utes of wall time and consumes 5.7M input tokens and 139K out- put tokens. 2 4 Results 4.1 Baseline Heuristic To contextualise the search results, we define a hand-coded baseline heuristic that captures straightforward domain reason- ing without any LLM involvement. The baseline uses three simple rules: (1) height reduction: apply 80% of the per-pass HR limit until close to the target thickness, then use the remain- ing thickness to determine the final reduction; (2) interpass time: fixed at 10 s regardless of conditions; (3) rolling velocity: a coarse six-level lookup on the temperature error (speed up when too cold, slow down when too hot), with no grain size or force awareness. This baseline achieves a mean reward of 41.0 on the 8 search feedback scenarios (100% completion) and 46.7 on the 81-case held-out grid. Its thickness precision is strong (0.04 m mean error), but it has no grain size control (7.8휇m mean error—the final grain size is effectively constant regardless of target) and only coarse temperature management (38.8 K mean error). It also incurs 4 constraint violations (3 force, 1 torque) across the 81 test cases. By comparison, the best heuristic discovered by the LLM search achieves 55.5 on the 8 search scenarios and 60.9 on the held-out grid—a 30% improvement over the baseline. The improvement is concentrated in temperature control (7.7 K vs. 38.8 K mean error) and grain size management (6.3휇m vs. 7.8휇m), where the LLM-generated heuristic employs propor- tional controllers and strain-based scheduling that the baseline lacks. We note that this baseline is deliberately simple; a more carefully engineered hand-coded controller could narrow the gap, and the comparison primarily illustrates the type of reasoning the search discovers rather than claiming a definitive advantage over all possible baselines. 4.2 Convergence Behavior Figure 1 shows the best-so-far reward trajectory across all 52 runs. The median converges to approximately 40 within the first 5 iterations, with rapid initial improvement followed by diminishing returns. The interquartile range tightens over iterations, indicating that most runs converge to a similar performance band despite exploring different strategies. Figure 2 reveals that 50% of runs find their best heuristic by iteration 4 (mean: iteration 8). This early convergence supports the budget allocation argument in §4.3: most value is extracted in the first few iterations. The best single heuristic across all 52 runs achieves a mean reward of 55.5, discovered via a counterintuitive decoupled controller architecture in which height reduction controls thick- ness, rolling velocity controls temperature, and interpass time controls grain size. This mapping contradicts standard metallur- gical reasoning (which assigns temperature control to interpass time) and was discovered by only one run. We observe a strong tendency for the LLM to converge on domain-conventional strategies—in particular, Thermomechanical Controlled Pro- cessing (TMCP) paradigms—which we refer to as mode col- lapse to familiar architectures. In one 30-iteration run, all four 051015202530 Iteration 80 60 40 20 0 20 40 60 Best mean reward so far n=48n=32n=25n=18n=13n=12n=11 Search convergence (49 runs) 10th-90th pctl IQR (25th-75th) Median Mean Figure 1: Best-so-far reward across 52 independent runs. The red line shows the median, the dark band the IQR (25th– 75th percentile), and the light band the 10th–90th percentile. Individual traces shown in light blue. Labels indicate how many runs reached each iteration. 0510152025 Iteration at which best heuristic was found 0 2 4 6 8 Number of runs 50th pctl = 490th pctl = 21 Mean = 7.8 Iterations to best heuristic (49 runs) 0.0 0.2 0.4 0.6 0.8 1.0 Cumulative fraction of runs Count Empirical CDF Figure 2: Distribution of the iteration at which each run discovers its best heuristic. The 50th percentile is at iteration 4; the mean is at iteration 8. radical departures prompted by stagnation crashed with deeply negative rewards, suggesting that escaping these attractors remains a challenge for the current prompting strategy. 4.3 Budget Allocation A key practical question is how to allocate a fixed compute budget: run one long search or many short ones? Comparing the expected marginal gain from continuing a run versus restarting fresh (Figure 3), restarting yields substantially higher marginal gain during the first few iterations, as each fresh start explores a new region of the strategy space. The two curves converge around iteration 4, after which both strategies offer diminishing returns—consistent with the early convergence observed in Figure 1. Figure 3 formalises this using the empirical best-so-far distri- butions from the same 52 runs. For each candidate run length퐿, we extract the best-so-far reward at iteration퐿−1across all eligible runs and construct its empirical CDF퐹 퐿 . A budget 3 Figure 3: Expected best reward (median) as a function of total iteration budget for uniform strategies (퐿=1, 5, 10, 20) and the optimal mixed allocation. Labels on the optimal mix curve show the allocation chosen. Diversified restarts consistently outperform both single long runs and many short ones. of푇iterations allocated as푘independent runs of length퐿 yields a global-best CDF of퐹 푘 퐿 (assuming independence); the expected reward is the median of this distribution. We compare uniform strategies (all runs of length퐿 ∈ 1, 5, 10, 20) against an optimal mixed allocation[푙 1 ,푙 2 ,...]with Í 푙 푖 = 푇 , whose CDF is Î 푖 퐹 푙 푖 . The mixed strategy consistently outperforms any uniform strategy. For example, at budget푇=20, the opti- mal mix (10+10) outperforms a single run of 20 by allocating iterations to independent explorations of the strategy space. This finding—diversified restarts outperform single long runs or many short ones—is a central practical recommenda- tion. Each run needs enough iterations to reach a reasonable local optimum (pure퐿=1breadth underperforms), but not so many that budget is wasted on diminishing returns (pure퐿=20 depth also underperforms). The sweet spot is runs of 5–10 iterations: long enough to converge, short enough to afford multiple independent explorations of the strategy space. 4.4 Luby-Style Universal Restarts The budget allocation analysis above is retrospective: it requires running many independent searches first and analysing the empirical distributions after. A practitioner starting a new problem cannot know the optimal mix in advance. Luby- style universal restarts [Luby et al., 1993] offer a principled alternative: the restart schedule[1, 1, 2, 1, 1, 2, 4,...](scaled by a unit푢) is provably within a constant factor of the optimal fixed-cutoff strategy for any unknown runtime distribution— requiring no problem-specific tuning. We implement a Luby restart runner that executes 15 sub-runs with unit푢=5, yielding the schedule [5, 5, 10, 5, 5, 10, 20, 5, 5, 10, 5, 5, 10, 20, 40]for a total of 160 iterations per campaign. Each sub-run is a fresh search with conversation reset; the top 3 heuristics discovered so far can optionally be seeded into subsequent runs as informational context (the LLM sees them but is not constrained to refine Table 2: Luby restart campaigns vs. ad-hoc independent runs. “Best” is the global best reward on the 8 search feedback scenarios. “Med.” is the median best-per-run. “Wall” is total wall-clock time. StrategyRuns Iters Best Med. Wall Ad-hoc (52 runs) 52 730 55.5 33.5 ∼36 h Luby (unseeded)15 160 51.6 35.1 4.1 h Luby (seeded)15 160 48.3 41.7 4.1 h R1 (5) R2 (5) R3 (10) R4 (5) R5 (5) R6 (10) R7 (20) R8 (5) R9 (5) R10 (10) R11 (5) R12 (5) R13 (10) R14 (20) R15 (40) Sub-run (iterations) 20 10 0 10 20 30 40 50 Reward it 3 it 1 it 7 it 4 it 4 it 9 it 16 it 0 it 3 it 9 it 4 it 4 it 6 it 4 it 23 Restart vs depth: first iteration and subsequent rewards Later iterations First iteration Figure 4: Per-sub-run decomposition of an unseeded Luby campaign (unit푢=5, 15 sub-runs, 160 total iterations). Hollow bars show the first-iteration reward; dots show all subsequent iterations. Labels mark the iteration that achieved each sub- run’s best reward. Depth consistently improves over the restart baseline, but sub-run 8 shows that fresh restarts can also strike gold immediately. them). Table 2 compares two Luby campaigns against the 52-run ad-hoc baseline. Figure 4 shows the per-sub-run breakdown. For each of the 15 sub-runs, the hollow bar marks the reward obtained on the very first iteration (the “restart” contribution), while the dots show all subsequent iteration rewards (the “depth” contribution). Labels indicate which iteration achieved the sub-run’s best reward. In 14 of 15 sub-runs, the best reward comes from a later iteration—typically between iterations 3 and 9—demonstrating that depth within each sub-run is essential. The sole exception is sub-run 8, where the first iteration immediately produced a reward of 50.0, illustrating the complementary value of fresh restarts: a lucky initialisation can outperform extended refinement. Budget-matched comparison. The optimal mix analysis in §4.3 is retrospective: computing it required 52 independent ad-hoc runs totalling 730 iterations to build reliable empirical CDFs. A practitioner starting a new problem has no such data. Figure 5 compares the Luby campaign’s actual cumulative best- so-far against the ad-hoc optimal mix curve. Despite using only 160 iterations in a single automated session, the Luby trajectory approaches the optimal mix—which itself required 4 020406080100120140160 Total iteration budget 15 20 25 30 35 40 45 50 Expected best reward (median) Budget-matched comparison: Luby vs ad-hoc strategies Ad-hoc optimal mix Luby restarts (best=51.6) Figure 5: Budget-matched comparison. The black curve shows the expected best reward (median) under the optimal mixed allocation, computed retrospectively from 52 ad-hoc runs (730 total iterations). The green staircase shows the actual cumulative best achieved by a single unseeded Luby campaign (160 iterations). The Luby schedule approaches the hindsight-optimal strategy without requiring prior data. 4.5× as many iterations and hindsight analysis to identify. The best ad-hoc outlier (55.5) was not matched by the Luby campaign, consistent with the high variance of LLM-driven search: exceptional results require either many independent trials or fortunate initialisation. However, Luby restarts provide a reliable, automated path to near-top-decile performance without the cost of running 50+ independent searches or the need for retrospective budget analysis. 4.5Inference Strategies: From Pool to Deploy- ment Multiple search runs produce a pool of diverse heuristics. A key advantage of heuristic policies over neural networks is that each candidate is a lightweight Python function: evaluating it on the physics simulator takes milliseconds per episode, and verifying it against safety specifications takes under 5 seconds (§4.8). This makes it practical to evaluate the entire pool on each new job specification, filter out candidates with audit failures, and select the best result—the simulator serves as ground truth, eliminating the need for a learned classifier. We apply greedy portfolio construction to both the ad-hoc pool and the Luby pool (Figure 6): starting from an empty set, at each step퐾we add the heuristic that maximises the oracle reward—defined as the mean, over all test cases, of the maximum reward achieved by any portfolio member on that test case. This selects for complementary specialists: the second heuristic chosen is not the one with the second-highest individual mean, but the one that best covers scenarios where the first heuristic underperforms. The ad-hoc pool contains 18 heuristics from the single run that produced the global best heuristic (19 iterations); the Luby pool contains 156 heuristics from all 15 sub-runs of the unseeded campaign. Both are evaluated on the same 81-case held-out grid (thickness, grain 12345678910111213141516171819202122232425 Portfolio size (K) 54 56 58 60 62 64 Mean oracle reward K=4 K=6 Greedy portfolio: ad-hoc vs Luby Ad-hoc (50 runs) (18 heur.) Luby restarts (156 heur.) Figure 6: Greedy portfolio construction: ad-hoc (18 heuristics) vs. Luby (156 heuristics), evaluated on 81 held-out test cases. Both curves exhibit sharp diminishing returns. The ad-hoc pool starts higher (single best 60.9 vs. 54.5) but the Luby pool converges to a comparable oracle (64.5 vs. 65.1). Dashed lines mark the 퐾 at which 90% of the full-pool gain is captured. size, HR limit, and temperature variations). For the ad-hoc pool, the single best heuristic achieves 60.9 and the full oracle reaches 65.1—a portfolio of퐾=4captures 90% of the gain. The Luby pool starts lower (single best 54.5) because its heuristics are drawn from many short sub-runs, but it converges rapidly: by퐾=5it reaches 63.3 (90% of its 10.0-point gain), and the full oracle of 64.5 is within 1% of the ad-hoc oracle despite requiring4.5×fewer total search iterations to generate. This means that even if evaluating many candidates per job is undesirable, a pruned portfolio of 3–5 heuristics provides near-oracle performance at minimal computational cost. Evaluation sets and reported metrics. To clarify compa- rability: the reward of 55.5 (best heuristic across all 52 runs) and 57.4 (best-of-푁across runs) are measured on the 8 search feedback scenarios used during the search loop. The reward of 60.9 (best single heuristic) and 65.1 (oracle portfolio) are mea- sured on the separate 81-case held-out grid, which was never used during search. The higher absolute values on the 81-case grid reflect the inclusion of easier scenario combinations in the full combinatorial product; the two sets are not directly comparable. The mode collapse discussed in §4.1 becomes an advantage at the pool level: because different runs converge to different local optima, the resulting heuristics specialise on complementary subsets of the operating space, making the portfolio more diverse than any single run’s trajectory. 4.6 Interpretability of the Search Process Unlike black-box optimization, the LLM search produces a complete reasoning trace: at every iteration, the model artic- ulates its strategy in natural language before generating code. 5 Table 3: Strategy evolution over a 20-iteration search. The LLM’s natural language reasoning reveals how it diagnoses weaknesses, manages trade-offs, and synthesizes solutions. Reward is the mean across 8 scenarios. Iter LLM’s stated strategyReward 0 “Adaptive Two-Phase: bulk reduction23.5 then precision finishing” 1 “Fix catastrophic temperature failure:28.1 every scenario loses∼2.0 pts” 3 “Proactive heat conservation via33.8 interpass time modulation” 8 “Temperature excels but core reduction35.2 strategy has systemic flaws” 10 “Radical departure: the conflict between24.3 thermal and metallurgical efficiency requires a fundamentally new approach” 14 “Fuse strain-based HR with re-tuned38.0 thermal response—hybrid synthesis” Table 3 shows a representative excerpt from a 20-iteration run, illustrating how the LLM’s understanding deepens through interaction with the evaluation feedback. Three patterns emerge. First, the LLM explicitly diagnoses weaknesses using the per-component feedback (iteration 1: “every scenario loses∼2.0 pts on temperature”). Second, it discovers trade-offs between objectives (iteration 8: thermal efficiency vs. reduction strategy) and eventually synthesizes solutions that balance them (iteration 14). Third, radical departures prompted by stagnation (iteration 10) often regress before enabling later breakthroughs—the hybrid at iteration 14 combines insights from both the conservative and radical branches. This process-level interpretability is a distinctive advantage: a domain expert can audit not only what the final policy does but why specific design choices were made, tracing each decision back to a diagnosed weakness and a reasoned response. 4.7 Interpretability of the Generated Policy Each generated policy is a readable Python function with explicit control logic. Listing 1 shows a condensed excerpt from the best-performing heuristic (reward 55.5). The code reveals three layers of metallurgical reasoning: 1. Hybrid height reduction (lines 2–13): A schedule detec- tor distinguishes low-reduction scenarios (conservative 50% split to avoid equipment penalties) from bulk-reduction sce- narios (strain-based targets with grain-size-aware schedul- ing). 2. Proportional temperature control (lines 15–20): Inter- pass time computed as a proportional controller on temper- ature error, with a 25 K deadband and linear scaling up to 40 s of cooling. 3. Force-aware velocity (lines 22–26): Rolling velocity adapts to force as a fraction of the equipment limit, reducing speed when force exceeds 70% capacity. 1 # --- Height Reduction Logic --- 2 remaining = current_thickness - target_thickness 3 if remaining < max_hr_m: 4# CONSERVATIVE: split into two passes 5target_hr = remaining * 0.5 6 else: 7# AGGRESSIVE: strain-based reduction 8if grain_size > target_grain * 2.0: 9strain = 0.8 # heavy refinement 10elif grain_size > target_grain: 11strain = 0.4 # moderate refinement 12else: 13strain = 0.1 # preservation 14target_hr = thickness * (1 - exp(-strain)) 15 16 # --- Interpass Time (Temperature Control) --- 17 temp_error = temperature - target_temperature 18 if temp_error > 25.0: 19frac = clip((temp_error - 25) / 125, 0, 1) 20interpass = 5.0 + frac * 35.0 # 5-40s 21 else: 22interpass = 1 # minimal wait 23 24 # --- Rolling Velocity (Force Management) --- 25 force_limit = 4_000_000 26 if force > force_limit * 0.70: 27velocity = 2 # slow for safety 28 elif force < force_limit * 0.25: 29velocity = 6 # fast for throughput 30 else: 31velocity = 5 # default Listing 1: Condensed excerpt from the best heuristic (reward 55.5). Helper functions and variable unpacking omitted. A domain expert can inspect each decision, verify it against metallurgical principles, and modify specific thresholds before deployment—none of which is possible with a neural network policy. However, manual inspection does not scale: a search run produces dozens of candidates, and even for a single heuristic, the number of input combinations is effectively infinite. This motivates the automated audit described next. 4.8 Automated Safety Auditing Deploying LLM-generated code in safety-critical industrial settings requires more than interpretability: the code must be systematically verified against domain specifications. Inspired by the formalized specification approach of SpecVerify [Wang et al., 2025], we developed a five-layer automated audit pipeline that verifies each candidate heuristic: 1.AST structural & security checks (29 checks, 8 categories): validates function signature, sandbox compliance, action mask usage, bounds clipping, division safety, and return path completeness. 2. Interval analysis: propagates input value ranges through the heuristic’s arithmetic to statically verify that all three outputs remain within action bounds. 3.Domain specifications: 11 formal requirements (SPEC- 001–011) covering safety (no overshoot, HR-limit respect), monotonicity, responsiveness, and consistency properties. 4.Z3 SMT verification: proves specs hold for all valid inputs by translating the heuristic AST to Z3 constraints. Safety specs use scalar mask decomposition; monotonicity specs use a two-translation technique that creates two independent symbolic evaluations of the heuristic and proves relational 6 Table 4: Audit results for the best heuristic (reward 55.5). Five analysis layers produce 65 checks with 0 errors. Z3 proves safety specifications for all valid inputs; remaining specs verified via randomized property testing. LayerChecks Pass Notes AST (8 categories)29 27/29 2 warn Interval analysis9 8/9 1 warn Z3 SMT prover10 9/10 5 proved∀, 4 deferred Property testing17 17/17 207 inputs, 0 failures Total: 65 checks61/65 0 errors properties between their outputs. 5.Property-based testing: randomized testing (207 inputs including 7 edge cases) verifies specs that Z3 cannot handle due to complex numpy operations, and catches runtime exceptions. Table 4 shows the audit results for the best heuristic (re- ward 55.5). The pipeline executes 65 checks with zero errors. Z3 formally proves 5 specifications for all valid inputs, including three safety properties (no-overshoot, HR-limit respect, non- negative reduction), HR–thickness monotonicity, and interpass– grain monotonicity. For the monotonicity specs, the verifier translates the heuristic’s Python AST to Z3 constraints twice with different symbolic inputs to compare outputs—a two- translation technique that enables proving relational properties of the generated code. One spec (SPEC-006, velocity de- creases with force) yields a Z3 counterexample at a degenerate boundary (force near zero), though property-based testing con- firms the property holds across realistic operating ranges. The remaining 4 specs, involving responsiveness or epsilon-delta continuity reasoning, are deferred to property-based testing with zero failures. The audit pipeline runs in under 5 seconds per heuristic and can be integrated into the search loop as a post-evaluation filter, automatically rejecting candidates that fail safety specifications before they enter the pool. Figure 7 shows how audit results evolve across the 18 it- erations of the best ad-hoc run. Structural integrity, security, action mask compliance, bounds, and return paths pass con- sistently across all iterations—these categories are effectively enforced by the sandbox and prompt constraints. Division safety and domain specification compliance show intermittent warnings, but no iteration produces an error. Notably, warn- ing counts do not correlate with reward: the best iteration 8 (reward 55.5) has 3 warnings, while iteration 15 (reward 12.6) has 7 warnings. This confirms that the audit captures safety properties orthogonal to reward, making it a complementary signal for deployment decisions. 5 Discussion What works. The structured 4-phase loop with rich be- havioral feedback is effective: the LLM consistently gener- ates competent policies within a few iterations, and the per- 20 40 Reward 55.5 3.5 Audit evolution across search iterations 0124578910111213141516171819 Iteration Structural Security Action mask Bounds Division safety Info usage Return paths Domain specs PPPPPPPPPPPPPWPPPP PPPPPWWWWWWWWWWWWW PPPPPWWWWWWWWPWWWW P WWWWWPPWWPWPWWWPWW P P PPWPWPPPPPWPPPPWPP All passedWarnings onlyHas errors Figure 7: Traffic-light heatmap of per-category audit results across 18 iterations of the best ad-hoc run (the same run used for portfolio construction in §4.5). Green = all checks passed, amber = warnings only, red = errors. All iterations achieve zero errors; warnings appear intermittently in division safety and domain specification categories. scenario reward decomposition enables targeted refinement. The generated heuristics embed recognizable metallurgical reasoning—grain-size-aware strain scheduling, proportional temperature controllers, force-adaptive velocity—despite re- ceiving this knowledge only through the system prompt. The interpretability of the outputs is a qualitative advantage over RL in safety-critical industrial settings, and the automated audit pipeline (§4.8) strengthens this with quantitative verification evidence: Z3 formally proves key safety and monotonicity properties for all valid inputs, while property-based testing covers specifications involving constructs beyond Z3’s reach. What fails. Three limitations emerged. First, radical ex- ploration is unreliable: all four radical departures in one 30-iteration run produced architectures that crashed catas- trophically (rewards−79to−88), suggesting that the current “try something completely different” prompt lacks sufficient guidance. Second, conversation compaction causes amnesia: effective micro-modifications (e.g., strain-aware roughing, pro- portional temperature control) were rediscovered multiple times within the same run, indicating that the compaction mechanism fails to preserve actionable insights. Third, mode collapse to familiar architectures limits exploration diversity within a single run—the LLM gravitates toward domain-conventional reasoning (TMCP-style controllers) and struggles to discover unconventional-but-effective mappings like the decoupled con- troller. Memory strategy. To address conversation amnesia, we com- pared two memory strategies: compaction (the default, which summarises old messages when the context grows too large) and synthesis (which resets the conversation each iteration and provides the LLM with a structured knowledge document main- 7 02468101214161820 Iteration 80 60 40 20 0 20 40 60 Best mean reward so far n=35 n=23 n=17 n=11 n=9 n=16 n=12 n=11 n=9 n=4 Compaction (n=36) Synthesis (n=16) Figure 8: Best-so-far reward by memory strategy. Synthesis resets the conversation each iteration and provides the LLM with a structured∼800-word knowledge summary synthesised by a narrator; Compaction preserves the full conversation and summarises old messages when the context grows too large. Solid lines show medians; shaded bands show IQR. Run counts decrease at higher iterations as shorter runs drop out. The synthesis strategy shows higher median reward in early iterations, though sample sizes are modest (16 vs. 36 runs) and the two groups were run sequentially, so this comparison should be interpreted cautiously. tained by a narrator agent). Figure 8 shows that synthesis runs achieve higher median reward throughout, with the gap most pronounced in the first 5 iterations. The best overall heuristic (reward 55.5) came from a synthesis run. However, we caution that sample sizes are modest (16 synthesis vs. 36 compaction runs) and the two groups were run sequentially rather than interleaved, so confounds such as prompt refinements between batches cannot be ruled out. More controlled experiments are needed to establish a robust conclusion. Practical recommendations. Based on our analysis: (1) allo- cate budget to many short runs (5–10 iterations) rather than few long ones—or use Luby-style restarts (§4.4) to automate this allocation without problem-specific tuning, (2) use best-of-푁 selection across runs (which achieved a reward of 57.4 in our experiments), (3) invest in structured memory mechanisms to mitigate conversation amnesia, and (4) run the automated audit on all deployment candidates—the pipeline takes under 5 seconds per heuristic and catches safety violations that reward alone cannot detect (§4.8). 6 Related Work LLM-driven heuristic and code generation. Fun- Search [Romera-Paredes et al., 2024] uses LLMs with an evolutionary algorithm to discover mathematical functions at a scale of∼1M evaluations. Evolution of Heuristics (EoH) [Liu et al., 2024] maintains (thought, code) pairs and uses the LLM as a crossover/mutation operator. ReEvo [Ye et al., 2024] adds a reflective mechanism with separate generator and critic LLM roles. Concurrent work by Guo et al. [2026] demon- strates LLM-driven policy evolution on LunarLander using population-based search with behavioral feedback; our work differs in using a single-trajectory search with adaptive modes (refinement, radical exploration) rather than a population, and focuses on a complex industrial domain with multi-objective rewards. MLES [Hu et al., 2025] enriches the evolutionary loop with visual feedback from rollout videos; we pursue a complementary direction, using structured per-component re- ward decompositions as feedback. Vulcan [Dwivedula et al., 2025] applies LLM-driven heuristic search to systems prob- lems (cache eviction, memory tiering), demonstrating that the approach generalises beyond RL benchmarks to applied domains. While these works focus on the search algorithm or a single-run evaluation, our case study contributes an empirical budget allocation analysis across 52 independent runs on a realistic industrial simulator, showing that diversified restarts outperform single long runs in this setting—a practical finding that may generalise to other LLM-driven search settings. Hot rolling optimization. Traditional approaches use ge- netic algorithms [Carreon et al., 2019], mathematical program- ming, or expert systems for pass schedule design. Recent work applies RL to simplified rolling models [Idzik et al., 2024], but typically with analytical rather than physics-based simulators. Our environment uses PyRoll [Weiner et al., 2023] for physi- cally grounded state transitions including realistic force/torque calculations and microstructural evolution. 7 Conclusion We presented a case study applying LLM-driven heuristic search to hot steel rolling, demonstrating that this paradigm can produce auditable control policies in a realistic industrial simulator. Across 52 independent runs, the framework reliably produces competent policies within the first few iterations. A budget allocation analysis shows that splitting a fixed budget into several short runs outperforms a single long run, as most value is extracted early and fresh starts explore diverse strategy regions. The generated heuristics are human-readable Python functions embedding explicit metallurgical reasoning, and the automated audit pipeline provides deployment assurance by formally proving key safety properties via Z3 for all valid inputs and verifying the remaining specifications through property- based testing. Future work includes structured architectural mutations to counteract mode collapse, persistent cross-run memory to mitigate conversation amnesia, extending the Z3 ver- ifier to cover array-dependent specifications currently deferred to property testing, and integrating the audit as an in-loop filter that rejects unsafe candidates before evaluation. We validated Luby-style universal restarts [Luby et al., 1993] as a principled restart strategy (§4.4): a single 160-iteration Luby campaign approaches the hindsight-optimal budget allocation derived from 52 ad-hoc runs totalling 730 iterations, achieving near- top-decile performance without prior data or manual tuning. Extending this to adaptive schedules that adjust the unit size online based on observed convergence rates is a promising direction. Code and data are available at Siboni [2026]. 8 References B. Romera-Paredes, M. Barekatain, A. Novikov, et al. Mathe- matical discoveries from program search with large language models. Nature, 625:468–475, 2024. F. Liu, C. Xialiang, Z. Zhuangdi, et al. Evolution of heuristics: Towards efficient automatic algorithm design using large language model. In Proc. ICML, 2024. H. Ye, J. Wang, Z. Cao, F. Song, and G. Chen. ReEvo: Large language models as hyper-heuristics with reflective evolution. In Proc. NeurIPS, 2024. P. Guo, C. Li, Y. Feng, and C. Zhang. Code evolution for control: Synthesizing policies via LLM-driven evolutionary search. arXiv preprint arXiv:2601.06845, 2026. Q. Hu, X. Tong, M. Yuan, F. Liu, Z. Lu, and Q. Zhang. Discovering interpretable programmatic policies via mul- timodal LLM-assisted evolutionary search. arXiv preprint arXiv:2508.05433, 2025. R. Dwivedula, D. Saxena, S. Yadalam, D. Kim, and A. Akella. Vulcan: Instance-optimal systems heuristics through LLM- driven search. arXiv preprint arXiv:2512.25065, 2025. M. Weiner, C. Schmidtchen, and R. Kawalla. PyRoll — an open- source rolling framework. In Proc. International Conference on the Technology of Plasticity, 2023. M. Towers, A. Kwiatkowski, J. Terry, et al. Gymnasium: A standard interface for reinforcement learning environments. arXiv preprint arXiv:2407.17032, 2024. Google DeepMind. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv preprint arXiv:2507.06261, 2025. C. A. H. Carreon, J. E. M. Tolama, G. C. Valdez, et al. Multi- objective optimization of the hot rolling scheduling of steel using a genetic algorithm. MRS Advances, 4:3373–3380, 2019. C. Idzik, A. Kramer, G. Hirt, and J. Lohmar. Coupling of an analytical rolling model and reinforcement learning to design pass schedules: towards properties controlled hot rolling. Journal of Intelligent Manufacturing, 35:1469–1490, 2024. W. Wang, M. Farrell, L. Cordeiro, and L. Zhao. Supporting software formal verification with large language models: An experimental study. In Proc. IEEE International Require- ments Engineering Conference (RE), 2025. M. Luby, A. Sinclair, and D. Zuckerman. Optimal speedup of Las Vegas algorithms. Information Processing Letters, 47(4):173–180, 1993. N. H. Siboni. PSO: LLM-driven heuristic synthesis for pro- cess scheduling and optimisation.https://github.com/ nima-siboni/pso, 2026. A Domain Specification Catalog Table 5 lists all 11 domain specifications verified by the audit pipeline. Each specification encodes a physical requirement of the hot rolling process as a formal property that can be checked automatically. Specifications are grouped into four categories reflecting different aspects of controller correctness. Safety specifications (SPEC-001–003) are rated error sever- ity: violation means the controller could damage equipment or produce out-of-spec steel. No-overshoot (SPEC-001) ensures the height reduction never thins the slab below the target gauge— a fundamental constraint in rolling, since under-thick slabs cannot be corrected. HR-limit respect (SPEC-002) prevents exceeding the mill’s per-pass reduction capacity. Monotonicity specifications (SPEC-004–006) encode ex- pected physical relationships. SPEC-004 requires that a thicker slab (larger remaining reduction) triggers a proportionally larger height reduction—a controller that reduces less when the slab is further from target would be pathological. SPEC- 005 requires longer interpass waiting times when grain size is below target, since grain growth during the interpass period is the primary mechanism for achieving target microstructure. SPEC-006 requires that higher rolling force produces lower velocity, protecting the mill from overload. Responsiveness specifications (SPEC-007–009) verify that each output dimension actually responds to its relevant inputs. A controller that outputs a constant height reduction regardless of thickness (failing SPEC-007) would be degenerate. These are existential properties: we check that there exist input conditions producing different outputs. Consistency specifications (SPEC-010–011) verify deter- minism and continuity. SPEC-010 ensures no hidden stochastic- ity (which would make the controller unpredictable). SPEC-011 checks that small input perturbations do not cause discontinu- ous output jumps—important for smooth mill operation. Table 5: Complete domain specification catalog. Sever- ity: E = Error (safety-critical), W = Warning, I = Info. Method: Z3 = formally proved; H = property testing; 2T = two- translation (heuristic AST translated twice with different sym- bolic inputs). ID Category PropertySev. Meth. 001 SafetyHR≤ thickness− targetE Z3 002 SafetyHR/10≤ hr_limitE Z3 003 SafetyHR≥ 0E Z3 004 Monoton. Thicker⇒ larger HRW 2T 005 Monoton. Smaller grain⇒ longer waitI Z3 006 Monoton.Higher force⇒lower velocityI 2T/H 007 Respons. HR varies with thicknessW H 008 Respons.Interpass varies with temp/- grain W H 009 Respons.Velocity varies with force/tempI H 010 Consist.Deterministic outputE H 011 Consist.Continuous outputW H 9 The “Method” column shows the verification technique for the best heuristic (reward 55.5). Z3 formally proves 5 spec- ifications: three safety properties (SPEC-001–003) and two monotonicity properties (SPEC-004 via two-translation, SPEC- 005). SPEC-006 (velocity decreases with force) yields a Z3 counterexample at a degenerate boundary (force near zero), though property-based testing confirms the property holds across realistic operating ranges. The remaining 4 specs, in- volving responsiveness or epsilon-delta continuity reasoning, are deferred to property-based testing. B Verification Methodology Details B.1 AST-Based Static Analysis (Layer 1) The first audit layer performs 29 static checks organized into 8 categories, executed via AST visitors without running the heuristic. Table 6 summarizes the categories. Table 6: AST-based check categories. Each category targets a specific failure mode of LLM-generated code. CategoryChk What it catches Structural integrity4Wrong signature, missing re- turns, global state, class defini- tions Security / sandbox6Imports, exec/eval, file I/O, dun- der access, forbidden modules Action mask compliance3Mask not referenced, not checked, no fallback Bounds & clipping3Outputs outside[0, 500], [1, 120], [1, 6] Division safety2 Unguarded divisions, NaN/Inf risk Info dict usage4Missing critical keys, force un- awareness Return path complete.3Dead paths, wrong length, no fallback Control logic quality4Ignores thickness, constant out- puts Security checks deserve special attention because LLMs occasionally generate code that stores mutable state on the func- tion object (e.g.,heuristic.prev_hr = val) or accesses dunder attributes. The audit flags these via SEC-006 (allowed modules check), which requires all attribute-set targets to be whitelisted. In the best ad-hoc run (Figure 7), all 18 itera- tions pass security checks—no mutable state or dunder access patterns were observed. Other runs in our 52-run corpus do exhibit these patterns, confirming the check’s value. B.2 Interval Analysis (Layer 2) The interval analysis layer propagates input value ranges through the heuristic’s arithmetic to verify output bounds stat- ically—without executing the code. Starting from known input ranges (Table 7), the evaluator walks the AST and computes a closed interval[lo, hi]for every intermedi- ate variable. For example, givencurrent_thickness ∈ [5, 110] andtarget_thickness ∈ [5, 15], the ex- pressionremaining_reduction = current_thickness - target_thickness yields the interval [−10, 105]. Table 7: Input value ranges for interval analysis and Z3 con- straints. VariableMinMax Unit current_thickness5.0110.0 m target_thickness5.015.0 m hr_limit20.050.0 m stock_temperature8001523 K target_temperature 10731273 K current_grain_size5500 휇m target_grain_size525 휇m rolling_force −1004×10 6 N rolling_torque −100 1.3×10 5 N·m step_count025 — Interval arithmetic handles all standard operations: addition (intervals add), subtraction (lo subtracts hi), multiplication (product of all endpoint pairs), and division (with explicit zero- crossing detection). The evaluator also handlesnp.clip,min, max,int(),round(), and if/else branching (union of branch intervals). The output is three interval checks (RNG-001–003) verifying that the HR, interpass, and velocity outputs remain within their action bounds for all possible input combinations. B.3 Z3 Formal Verification (Layer 4) The Z3 verification layer translates the heuristic’s Python AST into Z3 SMT constraints and proves that domain specifications hold for all valid inputs—not just sampled ones. AST-to-Z3translation. Thetranslator (HeuristicZ3Translator) creates a symbolic Z3 variable for each of the 10 input keys (Table 7), with domain constraints bounding their ranges. It then walks the heuristic’s function body, translating each Python construct: •Arithmetic:+,−,×,÷, floor division, power→Z3 arith- metic • Comparisons: <,≤,>,≥,=,≠→ Z3 boolean expressions •Control flow:if/else →Z3If(cond, then, else) with branch merging •Calls:np.clip(x,lo,hi)→ If(x<lo, lo, If(x>hi, hi, x)) ; similarly formax,min,abs,int,round, math.ceil/floor • Dict access: info[’key’]→ corresponding Z3 variable Constructs that cannot be translated—notably numpy array op- erations such asnp.where,np.argmin, and array indexing— cause aZ3TranslationError. The translator handles this gracefully: failed assignments are excluded from the envi- ronment, and if a return value references an untranslatable variable, that output dimension is marked asNoneand the spec is deferred to property-based testing. Contiguous mask decomposition. The action mask for height reduction is a 501-element binary array wheremask[푖]= 10 1iff푖/10≤ min(hr_limit, 0.7×thickness, thickness− target). Because this mask is contiguous (all 1s up to some index, then all 0s), it can be decomposed to a single scalar max_valid_idx. This avoids reasoning about arrays entirely and enables Z3 to prove safety properties (SPEC-001–003) by showing that any action within the mask satisfies the constraint. Two-translation technique. Monotonicity and relational specifications require comparing the heuristic’s output under two different input conditions. The verifier creates two inde- pendent translator instances with prefixed variable names (e.g., a_current_thickness,b_current_thickness), trans- lates the heuristic AST twice, and builds a property comparing the two outputs: 1. Create translators 푇 푎 (prefix a_) and 푇 푏 (prefix b_). 2. Translate the function body with each, extracting return expressions. 3. Equalize all shared inputs: ∀푘≠ 푘 vary : 푎 푘 = 푏 푘 . 4. Add ordering constraint on the varied input: 푎 푘 vary > 푏 푘 vary . 5. Prove the output relationship: e.g.,out 푎 ≥ out 푏 for in- creasing monotonicity. Z3 then checks whether the negation of this property is satisfi- able. If unsatisfiable (UNSAT), the property is proved for all valid inputs. If satisfiable (SAT), Z3 provides a concrete coun- terexample. For SPEC-006 (velocity decreases with force), this technique proves the property in under 0.1s. For SPEC-004 (HR monotonicity), the technique succeeds on simpler heuris- tics but falls back to Hypothesis when the HR computation uses np.argmin—an untranslatable construct. If/else branch merging. A subtle correctness issue arises when one branch of an if/else translates successfully but the other does not (e.g., theif remaining_reduction < 0.1: hr_action = 0 branch succeeds, but the else branch fails because it usesnp.argmin). Naïvely using the one-sided value would produce a false proof. The translator handles this by tracking which variables existed before the branch point: variables introduced in only one branch (due to translation failure in the other) are excluded from the merged environment, correctly marking that output as untranslatable. B.4 Property-Based Testing (Layer 5) The final layer executes the heuristic with actual numpy opera- tions on 207 test inputs (200 random + 7 deterministic edge cases) and verifies all specs that Z3 could not handle. Edge cases. Seven edge cases encode domain expertise about which operating conditions are most likely to trigger failures: 1.Near target: thickness= 10.1m, target= 10.0m (tests minimal-reduction logic) 2. Maximum state: all inputs at upper bounds (tests saturation behavior) 3. Minimum state: all inputs at lower bounds (tests boundary handling) 4.Tight mask: remaining reduction= 0.5m (only a few valid HR actions) 5. Force sentinel: force= −100N (pre-first-pass sentinel value from environment) 6.Equal grain sizes: current=target (tests zero-error han- dling) 7.Equal temperatures: stock=target (tests zero-error han- dling) Random inputs. The 200 random inputs are sampled uni- formly from the ranges in Table 7, with the constraint that current_thickness ≥ target_thickness. For each in- put, a consistent action mask is generated from the physical constraints (HR limit, 70% thickness rule, minimum gauge). Per-input checks. Each test input runs 6 basic checks (PBT- 001–006): no exceptions, correct return type, HR/interpass/ve- locity within bounds, and mask compliance (the selected HR action must not be masked out). Additionally, all domain specs deferred from Z3 are verified by calling the spec’s check function with the test input. Z3-to-Hypothesis deferral. The Z3 layer produces a list of deferred spec IDs that it could not verify. These are passed to the property testing layer, which verifies them via execution. The deferral is transparent in the audit report: each deferred spec appears in both the Z3 section (marked “deferred to Hypothesis”) and the property testing section (marked “deferred from Z3”), ensuring complete traceability. 11

Instant research discovery