PaperlayerView exact revision on arXiv

Source-linked AI summary

Learning to Formulate: Agentic Hardware-Software Co-Design of AI Infrastructure through Progressive Optimization and Verification

Yi Ding, Li Shang

arXiv:2610.39380v1cs.ARcs.AIcs.DC

TL;DR

Chip and software are often designed separately, leaving choices that pay off only when both change together outside the search; Formulaic has an agent formulate the problem and a solver optimize it, with verification and measurement checking the work. Across separate studies, Qwen3-8B layers ran 1.075× faster than SGLang; joint design cut worst-scenario cycles to 0.428 of reference versus 0.934 for software alone; five-step proof reuse sped checking 2.51×.

  • Problem

    Chip and software design often treat the other as fixed, leaving choices that pay off only when both change together outside the search.

    Source: §3 · p. 12

  • Method

    Formulaic has an agent propose and refine explicit formulations, a mathematical solver optimize within them, and verification and measurement check assumptions and results.

    Source: §1 · p. 2

  • Results

    Across separate studies, Qwen3-8B layers ran 1.075× faster than SGLang; joint design cut worst-scenario cycles to 0.428 of reference versus 0.934 for software alone; five-step proof reuse sped checking 2.51×.

    Source: §7 · p. 30

  • Takeaways & Limitations

    The separate studies show measurable benefits from fixed-chip template construction, joint chip–software design, and local proof reuse in their respective evaluations.

    Source: §7 · p. 30

    The hardware–software co-design workload is a published weighted GEMM list, not complete Transformer inference.

    Source: §5.5 · p. 27

Abstract

from arXiv · show

AI infrastructure, the chips and software that train and serve AI models, is designed in layers. Layers make the system manageable, but they also fix which choices an optimizer can consider. Gains that need the chip and its software to change together are excluded before optimization begins: the formulation leaves them out. Language-model agents make it possible to revisit these boundaries, but an agent's proposal cannot show by itself that a design is correct or optimal. We present Formulaic, a flow that divides the work. The agent writes the formulation, a mathematical solver optimizes within it, and verification and measurement check its assumptions and results. The agent refines the problem step by step, from the computation graph toward the chip. Each step is a template: a family of programs with the conditions under which they are correct. Wall relaxation searches the chip by pricing the hardware limits that bind the software. This paper takes a first step, through separate studies rather than one end-to-end run. On NVIDIA GB10, templates the agent wrote run complete Qwen3-8B layers $1.075\times$ faster than SGLang. In a simulated Ventus GPU study, joint design cuts the worst-scenario cycles of Qwen2.5-0.5B to 0.428 of the reference, against 0.934 for software alone. On a five-step GEMM refinement chain, reusing proofs makes checking $2.51\times$ faster.

1 Introduction

Formulaic uses language-model agents to refine explicit co-design formulations step by step, while solvers optimize them and verification and measurement test their assumptions and results. The introduction motivates this division of work and reports separate studies of software construction, hardware–software co-design, and verification reuse; a single end-to-end run remains future work.

Motivation

  • Layered design makes systems manageable but freezes interactions, excluding some cross-layer opportunities before optimization, while exposing every choice in a monolithic model makes it too large to solve usefully.The introduction frames the goal as an intermediate formulation that exposes consequential cross-layer choices while remaining tractable; it also notes that prior agent systems often lack an explicit optimization formulation for assessing correctness, optimality, and the reach of assumptions.Source: §1 · pp. 1–2

Formulaic

  • Formulaic has agents propose explicit formulations, solvers optimize within them, and verification and measurement check assumptions and consequences, returning failed formulations for repair.Each agent refinement is a template—a design pattern with conditions for correctness that bound the search, serve as proof preconditions, and indicate where reuse may be possible; proved templates and measurements are retained to seed later problems.Source: §1 · p. 2

Hardware–software co-optimization

  • Wall relaxation prices binding hardware limits by moving each wall one step, then buys the step with the greatest latency recovery per unit area and repeats.Progressive refinement descends from the computation graph to the microarchitecture, solving a small formulation over the decisions added at each step; each visited chip is paired with the best software in the model's menu.Source: §1 · p. 2

Results

  • 0.428 versus 0.934: joint chip–software design cuts Qwen2.5-0.5B worst-scenario cycles to 0.428 of the reference, compared with 0.934 for the best software-only design.The Ventus GPGPU study simulates 128-token prefill and extrapolates 512-token scenarios, with a 2.2× gain under the same area ceiling. In a separate complete instruction-simulation study, a 64×64 tile slower on the reference chip becomes part of the best design when registers, tensor shape, and cache change together.Source: §1 · pp. 2–3
  • 1.075× faster: agent-written templates run complete Qwen3-8B layers faster than SGLang on NVIDIA GB10, with the chip fixed.This is the geometric mean over eight scenarios; hybrid-MoE layer groups beat SGLang in seven of eight scenarios, and against a black-box coding agent given the same caps, the flow's program is faster at every input length (one run each).Source: §1 · p. 2
  • 2.51× faster checking: proof reuse accelerates verification of a five-step refinement chain, while real agent edits save 1.25× and local checks catch faults injected at every step.Source: §1 · p. 3

2 The Agentic Progressive Refinement Flow

Formulaic progressively refines hardware-software co-design: an agent defines bounded templates, a solver searches software and chip choices, and verification and measurement check the results. The flow can reopen coupled choices and carries verified templates with scoped performance evidence from software optimization into chip search.

2.1 Overview

  • The flow jointly designs software and a chip shared across workload scenarios, using an agent-written template, solver, verifier, and evaluator in a five-step loop.The workload contract defines required behavior independently of the optimization model; the loop returns measured costs to the agent for refinement.Source: §2.1 · p. 3

2.2 The template as a contract

  • A template is a contract whose search constraints must imply correctness preconditions, whose proof covers the whole family, and whose scope defines reuse.Conditions such as bottleneck dominance and decomposability guide ranking and pruning; if they fail, the design remains correct and the cost model or search branch is revised.Source: §2.2 · pp. 5, 7, 8

2.3 Iterative optimization through progressive refinement

  • Progressive refinement replaces coarse workload transactions with finer data transactions one step at a time, adding decisions and the conditions needed to verify them.This lets the optimizer and verifier handle only a few new decisions and conditions at each step rather than the whole stack.Source: §2.3 · p. 8

2.3.1 Refinement levels

  • The chip enters at refinement level 2 when capacity is needed, either as an open variable or through a software-versus-hardware mechanism choice.A chip-built mechanism is paid for once and serves every program that uses it, while software and hardware alternatives differ in area, instruction overhead, and allowed schedules.Source: §2.3.1 · pp. 9–10

2.3.2 One GEMM, five steps finer

  • Five GEMM templates refine a sum of products through partitioning, storage, scheduling, slot rotation, and resource configuration, with local proofs chaining back to the original computation.A lifetime constraint can serve both solver and verifier: it restricts the search and states the precondition needed to prove safe storage reuse.Source: §2.3.2 · pp. 10–11, Table 3 · p. 10

2.3.3 Solving one step at a time

  • The optimizer solves a sequence of small formulations, fixing earlier choices when independent, carrying them as variables when coupled, or reopening them when measurements reveal a cost.Progressive refinement does not guarantee tractability in general; for example, the reported tiling MILP has 93 variables and HiGHS solves it to proven optimality in under 0.2 s.Source: §2.3.3 · p. 11
  • Chosen-design loss is decomposed into template expressiveness, overly strong preconditions, solver gap, and cost-model error, with an upper bound of Lrep + ∆pre + δk + 2εk.The bound requires cost-model accuracy within εk for every design in the search space; sampled-design errors are only diagnostic, and a zero solver gap rules out only solver suboptimality.Source: §2.3.3 · p. 11
  • At 1.081 mm2, the balanced Ventus design achieves a 2.93× worst-scenario speedup over its reference when the tile, register capacity, tensor shape, and cache allocation are opened together.The study opened these choices by design; it does not claim the agent found the combination on its own. The result uses that study’s menus and reference chip, not Table 11’s.Source: §2.3.3 · p. 12

2.4 The evolving template population

  • The population stores templates with scope, proofs, produced designs and measurements, counterexamples, and descriptions of their algorithms, data reuse, placement, and resource needs.At each step, the agent selects templates whose scope covers the current problem, adapts or combines them, and returns those that pass verification.Source: §2.4 · p. 12
  • Only proved templates join the population; performance facts remain tied to their measured chip and workload, and structurally distinct templates are retained.This preserves options that perform poorly on today’s chip but may become useful after the chip changes.Source: §2.4 · p. 12
  • For a fixed chip, the flow gives software optimal within its templates and cost model, with proofs where the template carries one; the next section uses that solve to search the chip.The GB10 studies reuse agent-written templates on new inputs and models, while long-term population growth remains future work.Source: §2.4 · p. 12

3 Hardware–Software Co-Optimization by Wall Relaxation

Formulaic casts hardware–software co-design as minimizing latency over software programs legal for each chip, then searches hardware by pricing the resource constraints (“walls”) that shape software choices. Wall relaxation alternates software optimization with hardware purchases and measurement, but guarantees improvement only along its visited path under a fixed cost model.

3.1 One problem, coupled through walls

  • Walls express chip resources as software constraints; on GB10, capacity constraints alone exclude 61–64% of the 1,296-point tiling grid, and best designs tend to sit at a wall.Crossing a register-capacity wall can cause spills, while exceeding shared-memory capacity can prevent a launch; increasing capacity can make larger tiles legal without changing the cost of an already-admitted kernel.Source: §3.1 · p. 13
  • Because software choices are discrete, latency changes in stair steps: a wall can have a zero first-step price but a valuable later step, and joint wall moves can outperform separate ones.The one-wall screen can miss improvements that require relaxing multiple walls together; the coupled variant also screens pairs with both walls removed.Source: §3.1 · p. 14

3.2 The algorithm and its guarantees

  • At each iteration, wall relaxation solves software for the current chip, prices screened walls and selected pairs, buys the largest latency drop per added area within budget, measures the design, and reclaims slack resources.If measured and predicted latency drops disagree beyond the noise band, the flow treats this as a cost-model error, recalibrates, and recomputes the incumbent and prices.Source: §3.2 · pp. 14–15
  • With a fixed cost model, accepted positive-price purchases and objective-preserving reclamations yield non-increasing latency across visited chips, but the algorithm has no global optimality guarantee.Its greedy search can omit longer steps, screened-out pairs, higher-order combinations, and alternative purchase paths; recalibration restarts the guarantee under the updated model.Source: §3.2 · p. 15

4 Verification in the Loop

Verification runs inside the optimization loop: templates, solver candidates, and software paired with visited chips are checked before they proceed. Proofs follow refinement one step at a time, but the GB10 programs are checked numerically on tested inputs rather than proved.

4.1 One step, one local proof

  • Five local proofs compose into a proof that the GEMM design computes Y = AB, but correctness composes whereas optimality does not without a dominance argument.Each step relates fine and coarse behavior through initialization, step matching, progress, and completion agreement; progress alone does not ensure waiting requests are served without an arbitration assumption.Source: §4.1 · pp. 16–17

4.2 Prove the template once, check each candidate cheaply

  • 25 ms is the candidate-check cost for the tiling template, after its conditions are proved once for the template family.The proof covers tensor extents and interleavings in a bounded event model with two warps and five reduction phases, but not larger blocks or equivalence of FP32 summation orders.Source: §4.2 · pp. 17–18

4.3 The weakest contract

  • 1.34% latency is the precondition loss from always keeping the trailing barrier on a ragged GEMM; the exact precondition preserves the optimum, while a weaker one admits a race.The exact condition is checked on 24 combinations; the too-weak condition lets the solver select an unsafe design that the verifier rejects.Source: §4.3 · p. 18, Figure 2 · p. 18

4.4 Incremental reuse

  • 2.51× faster checking and 92-to-27 solver queries at depth five for the five-step GEMM chain; edits to an existing program yield 1.25× savings.Reuse saves more overall as refinement depth grows, when new steps build on unchanged ones.Source: §4.4 · p. 19

5 Evaluation

The evaluation uses separate studies to test agent-written templates on a fixed GB10, joint hardware–software design on simulated Ventus, and verification cost and fault detection. Candidates are checked against numerical references before timing, and each study has its own scope and limits.

5.2 Templates Proposed by the agent on GB10

  • 1.075× geometric-mean speedup over SGLang [25, 26] across all eight Qwen3-8B complete-layer scenarios on GB10.The complete Qwen3.5-35B-A3B four-layer group reaches a 1.019× geometric mean over SGLang, but regresses to 0.899× at P128; end-to-end serving gains vary by workload, and MoE decode replacement fails the full-model output and state check.Source: §5.2 · pp. 21–22, Table 7 · p. 22, Table 8 · p. 22

5.3 White Box versus Black Box

  • 5.93–49.76× faster than eager, Formulaic’s selected programs had lower median latency than the direct coding agent at all four histories.The comparison shows attained performance, not total optimization cost; each method ran once, solver selection did not isolate a gain, and the cost model underpredicted 8192 latency by 2.92×.Source: §5.3 · p. 24, Table 9 · p. 24

5.4 Reuse of Templates

  • 1.067–1.319× faster than SGLang, a fixed GateUp family transferred to four new input sizes; a fixed attention family reached 1.9–3.6× over its tiled online-softmax baseline.With prior knowledge, attention construction reached 1.49× FlashInfer and 8.98× eager at length 1025, improved at length 6145, and was nearly tied at 24577, with comparable construction costs.Source: §5.4 · pp. 24–25, Table 10 · p. 25

5.5 Hardware–Software Co-design

  • 812.6 to 264.1 million cycles, versus 539.8 million for software-only, when compiled-kernel changes and queue reallocation jointly optimize Qwen2.5-0.5B at P128.A separate balanced design achieves cycle ratios of 0.342/0.331 for P128/P512 and 0.295/0.272 for D128/D512; joint KV representation and hardware selection reduces storage by 16–17% versus software-only, at latency ratios near 0.18–0.20.Source: §5.5 · pp. 25–26, Table 11 · p. 25
  • 2.77×, 1.60×, and 2.38× performance improvements for prefill, decode, and mixed objectives, respectively, as wall relaxation reached the joint optimum within the finite search domain.Random search with a twelve-chip budget reached the same optimum, so the study demonstrates capacity-driven software reselection, not a search-cost advantage; larger starting chips were already optimal.Source: §5.5 · p. 26, Table 12 · p. 26
  • 16.53% lower energy–delay product and 28.71% lower estimated area than the complete seven-start DoSA run [30], at equal latency.This follows DoSA’s objective on its published weighted BERT GEMM list, not complete Transformer inference, and uses a common Gemmini evaluation policy.Source: §5.5 · pp. 26–27, Table 13 · p. 27

6 Related Work

Formulaic brings formulation-writing agents, mathematical optimization, chip search, simulation, and verification together as a first step toward cross-layer hardware–software design. The paper evaluates these pieces in separate studies.

Optimization-based co-design and design-space exploration

  • Earlier mathematical-program and joint hardware–software searches usually explore a fixed space with a given cost model; Formulaic lets an agent revise the formulation across stack levels.The paper’s Ventus fidelity study motivates testing the cost model itself (Appendix E).Source: §6 · pp. 28–29

Shadow prices and outer search

  • Wall relaxation re-prices integer-program capacity constraints by re-solving, then uses gain-per-cost outer search; unlike DoSA’s continuous relaxation, it evaluates choices on the discrete design domain.Re-solving is practical because the inner solve is small.Source: §6 · p. 29

AI compilers, kernels and serving systems

  • Prism verifies a symbolic tensor-program family before profiling parameter values [8]; Formulaic also proves templates, but searches software and chip together and proves allowed programs for its GEMM chain and tiling template.Existing compiler and kernel systems mostly optimize software for an existing chip, with validation ranging from tests to formal checks.Source: §6 · p. 29

AI for optimization, formulation and design

  • Prior systems already combine agents with evaluators, formal checks, and reusable knowledge [12, 13, 14, 7]; Formulaic investigates explicit formulations and correctness conditions as a shared interface across hardware–software decisions.Examples include OptiMUS’s optimization models, FormuEvo’s formulation evolution, FLARE’s checked reformulation, and Dr. RTL’s checked rewrites.Source: §6 · p. 29

Verification of optimization models, compilers and hardware

  • Existing tools verify optimization models, reformulations, transformations, and hardware [82] [83] [89] [90]; Formulaic asks whether every permitted design is correct within a multilevel optimization loop.The paper demonstrates this for one GEMM chain and one template.Source: §6 · p. 29

Where this paper sits

  • Formulaic combines agent-written cross-layer formulations, bounded solver search, chip search guided by software’s binding limits, simulation, and verification in separate studies.The verification goal is to prove the designs a formulation allows.Source: §6 · pp. 29–30

7 Conclusions

Formulaic divides formulation, optimization, and verification among an agent, solver, and measurement, refining templates from computation graph toward chip. Separate studies report gains in software performance, joint chip-software design, and proof reuse, while leaving an integrated end-to-end loop for future work.

Conclusions

  • Formulaic has an agent write formulations, a solver optimize within them, and verification and measurement check them, with templates refined from computation graph toward chip.Each template defines a family of programs and conditions for correctness; wall relaxation prices hardware limits binding the software and buys worthwhile steps.Source: §7 · p. 30
  • 1.075× faster complete Qwen3-8B layers on NVIDIA GB10 than SGLang; joint design cuts worst-scenario cycles to 0.428 of reference versus 0.934 for software alone; proof checking is 2.51× faster on a five-step chain.On real agent edits, checking is 1.25× faster. The agent-written program family beat a black-box coding agent at every input length in one run each, but the gain came from the family, not solver instance selection; no study runs the whole loop on one design.Source: §7 · p. 30
  • The studies leave limits in finite-domain capacity search, bounded proof coverage, one-run agent comparisons, incomplete chip models, and full-model MoE decode validation.Capacity search found the same optimum as random search only on a finite software and hardware domain; greedy search, single-wall screening, cost-model rankings, and unstated walls constrain it. Proofs cover only the GEMM chain and tiling template on bounded models, with arithmetic symbolic; GB10 programs are numerically checked only on tested inputs. The black-box comparison uses one run per method and host-side diagnostic help. Ventus results lack a power model, cost-model error can shift predicted cycle ratios from near 0.333 to simulated 0.791–0.899, Qwen-selected chips regress on GPT-2 and Pythia, and MoE decode fails a 40-layer output and state check, so serving uses the replacement for prefill only.Source: §7 · p. 30
  • Future work is to run the studies as one loop, expand and evaluate wall relaxation, prove generated GPU programs, adapt cost models and chip models, and grow template reuse across problems.The proposed extensions include throughput-changing resources and GB10 constraints, measuring the gap to joint search and purchase accuracy, adding power and physical design, and making prediction-measurement mismatches inform new walls or cost terms.Source: §7 · p. 30
  • The authors’ repository contains the flow, experiment records, and scripts producing each table and figure, with reported numbers traced to recorded runs.Listed software includes TileLang 0.1.15, SGLang 0.5.9 with FlashInfer, Transformers 4.57.1, HiGHS 1.15.1, Z3 4.16.0.0, and open-source Ventus GPGPU.Source: §7 · pp. 30–31

A The tiling contract: complete checks and ablations

The tiling contract is checked exactly against its stated precondition, while solver choices, contract ablations, and injected faults show how correctness constraints affect optimization. Soundness is argued for the template family, with each selected instance checked separately.

The tiling contract: complete checks and ablations

  • The end-to-end template uses HiGHS for its mixed-integer search, Z3 for correctness proofs, and an independent interpreter to replay counterexamples.Its illustrative chip contract assumes 128 SMs, 1.8 TB/s DRAM bandwidth, 80 TFLOP/s FP32, and a 40-cycle barrier; checks cover tensor extents and modeled schedules.Source: A The tiling contract: complete checks… · p. 36
  • Across all 24 slot-count, prefetch-distance, and barrier combinations, the verifier’s safe set exactly matched P ≤ S−2+β, with no designs wrongly accepted or excluded.Table 16 lists the safe prefetch distances. A third slot permits one more prefetch step or removal of the trailing barrier, but not both.Source: Table 16 · p. 36, A The tiling contract: complete checks… · p. 36
  • 0.03–0.16 s: HiGHS proved each of three GEMM design selections optimal at zero gap, matching brute-force enumeration of 722 feasible designs.Each selected design passed 12 conditions; all used three slots, prefetch distance one, and no trailing barrier, a choice legal under the weakest precondition.Source: Table 17 · p. 36, A The tiling contract: complete checks… · p. 36
  • 1.34% of latency was lost under the stronger contract on the compute-bound ragged shape, while memory-bound shapes lost nothing; the weaker contract selected a raced design.The verifier rejected the weaker-contract design and replayed its race, showing that the solver’s optimum can be wrong when its contract is unsound.Source: Table 18 · p. 37, A The tiling contract: complete checks… · p. 37, Figure 7 · p. 38
  • All six injected faults in the proved 1000×1000×1000 design were rejected by the responsible condition and accompanied by a replayed defect.For overlapping tiles, the coverage proof failed without a semantic witness and remained unresolved; the exact-once condition identified the defect.Source: Table 19 · p. 37, A The tiling contract: complete checks… · p. 37
  • The search constraints and correctness conditions coincide for this template, making its solver optimum correct by construction and eliminating loss to the contract.Soundness is argued for the family; each instance takes at most 0.16 s to solve and 25 ms to check.Source: A The tiling contract: complete checks… · p. 37

B Template reuse and construction details

The section reports template reuse measurements and a knowledge-assisted construction study. Its results compare re-solving or selecting configurations with alternatives, while the construction study specifies how agents build and validate attention kernels.

B Template reuse and construction details

  • Re-solving GateUp improves latency 11% at M128 and 6% at M512, matches at M2048, and is 2.3% slower at M4096; at attention length 6144, the expression-selected split trails the diagnostic split by 4.5–16.0%.Table 20 measures GateUp reuse components; Table 21 covers attention-template reuse on new history lengths.Source: B Template reuse and construction… · p. 38, Table 20 · p. 38, Table 21 · p. 38

B.1 Knowledge-assisted construction

  • The construction study compares common specifications and tools with assistance from an executable family, cost expression, and explanatory optimization knowledge.Each condition has three independent GPT-6 Astra runs at medium reasoning effort; agents can revise programs, decision variables, and expressions using measurement feedback, with final instances selected by expression rather than fastest probe.Source: §B.1 · p. 39
  • Three fresh batch-one, single-query grouped-query attention tasks use KV lengths 1025, 6145, and 24577, with no candidates or feedback carried between tasks.Timing includes attention, split reduction, and input-dependent transformations, but excludes projection, rotary embedding, and KV-cache updates.Source: §B.1 · p. 39
  • Runs are limited to 2400 seconds each for construction and compilation/measurement, plus 24 evaluated source–assignment pairs; final candidates and references pass direct and Graph checks against an independent FP32 reference.The first task allows up to two additional feedback batches; the later tasks receive four from the start. Measurements use warmed CUDA Graph replay on GB10.Source: §B.1 · p. 39
  • Same-batch eager, FlashInfer, and copied-reference latencies are 28.196/4.674/4.048 µs at N=1025, 1143.042/67.586/62.740 µs at N=6145, and 9820.396/439.035/429.582 µs at N=24577.The table defines speedup against the faster FlashInfer mode; costs exclude shared development (1205 s), infrastructure repair, unmeasured historical knowledge, and manual engineering.Source: §B.1 · p. 39, Table 22 · p. 39
  • For the first task, two runs per condition received earlier feedback on a previous host before all runs continued on GB10; final timing uses GB10 only.The cost comparison covers construction of each new family and excludes shared costs.Source: §B.1 · p. 39

C Wall-relaxation protocol

The wall-relaxation protocol searches register capacities by pricing predicted objective reductions per added area and reselecting software as capacities change. Instruction-simulator replay confirmed the selected results and reproduced every predicted gain within the prespecified tolerance.

C Wall-relaxation protocol

  • Capacity changes admit different programs only when every compiled kernel fits eight resident one-warp blocks, while the cost of a fixed program remains unchanged.The hardware domain spans twelve vector/scalar register-capacity combinations under a 1.11 mm2 area ceiling; lower-occupancy mappings are outside the experiment.Source: C Wall-relaxation protocol · pp. 39–40
  • Wall relaxation prices register-capacity increases by predicted objective reduction per added area, then reselects software after each purchase; its coupled extension screens pairs of capacity constraints together.Exact inner problems minimize over a finite program menu.Source: C Wall-relaxation protocol · p. 40
  • The objective is the maximum scenario-specific cycle ratio to the reference program and chip, over two prefill or decode lengths or all four mixed scenarios.The study uses Qwen2.5-0.5B at 128 and 512 tokens, with nine prefill and seven decode programs varying tiling, packing, fusion, and execution order.Source: C Wall-relaxation protocol · pp. 39–40
  • 57 selected results and ten logical purchases across two wall variants and three objectives were confirmed by instruction-simulator evaluation, with every predicted gain reproduced exactly within the 5% tolerance.Validation followed model search, so the experiment did not measure an interleaved online optimization loop.Source: C Wall-relaxation protocol · p. 40

D Verification across program revisions

Formulaic tests whether verification evidence can be reused as optimization changes programs, rebuilding changed obligations and retaining results only under strict matching conditions. Reuse preserves classifications across the evaluated histories, although unsupported spills leave some ELF versions unresolved.

D Verification across program revisions

  • Node reuse retains certificates for unchanged dependency-graph nodes; query reuse also retains prior UNSAT results only when the formula, checker, specification, and solver context match.Changed programs are decoded and obligations rebuilt before reuse, and unresolved results never become proofs.Source: D Verification across program revisions · p. 40
  • Evaluation replays 16 controlled revisions and seven actual agent proposals across a 59-version history, with generation and compilation excluded from timing.The controlled and seven-proposal sequences have three paired replays; the complete history has one, and all strategies start with empty reuse state.Source: D Verification across program revisions · p. 40
  • All strategies preserve classifications on real histories; full and node reuse agree on 192 controlled comparisons, while 45 of 59 real versions are proved and 14 remain unresolved.The unresolved cases involve unsupported spills of thread-private values to memory; a separate 16-revision fault replay preserves expected outcomes.Source: D Verification across program revisions · p. 40
  • Proof reuse remains distinct from floating-point numerical validation, and independent optimization histories remain a further transfer test.The evaluated reuse trajectory also informed development of query reuse.Source: D Verification across program revisions · p. 41

E Cost-model fidelity and chip transfer

The study finds that solver-optimal predictions do not reliably match complete instruction simulation, and Qwen-selected chips transfer poorly to other models.

E Cost-model fidelity and chip transfer

  • Despite zero solver gap and predicted worst-scenario cycle ratios near 0.333, complete instruction simulation yields 0.791–0.899, including a prefill ranking reversal (joint 0.899 versus hardware-only 0.791).In 18 transfer evaluations, Qwen-selected chips take 3.07–5.60× the baseline cycles of GPT-2 small and Pythia-160M.Source: E Cost-model fidelity and chip transfer · p. 41

F Structural and workload checks

The Python/Z3 checker evaluated structural variants and workload schedules, identifying faults and deadlocks while testing accepted schedules against injected fault families.

F Structural and workload checks

  • Across eight structural groups, the Python/Z3 checker evaluated 78 variants, identifying 31 new faults and three deadlocks through counterexample replay.It distinguished inherited faults, failed certificates, and infeasible domains.Source: F Structural and workload checks · p. 41
  • Workload checks accepted 36 causal-attention, 48 prefill-anddecode, and 16 training-transition schedules, replaying counterexamples for all 3/6/7 injected fault families, respectively.Source: F Structural and workload checks · p. 41

Related papers

Loading 2610.39380v1…