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

Yi Ding; Li Shang

cs.AROct 29, 2026

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

Authors: Yi Ding, Li Shang

Organizations: Shenzhen Loop Area Institute (SLAI) · National University of Singapore

Abstract

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.

Figures & tables

Figure 1: The proposed agentic progressive refinement flow. The design moves down seven levels, from the workload specification to the chip microarchitecture, and each level adds detail to both the software and the chip. At each step the agent takes a template from the population or writes a new one. The template’s search constraints

\mathcal{C}

bound the solver’s joint search over software and chip decisions, and its preconditions

\mathrm{Pre}

are what the verifier checks for every candidate. Only candidates that pass reach the evaluator. Counterexamples go back to the agent, which repairs the template, and measured costs go back to the population. In the full flow, the output is one configuration across all levels, with a proof built from the local proof of each step. This paper tests the parts of the loop in separate studies (Section 5 ).

Structure	Example on a GPU	What the search can drop
What to optimize
Bottleneck dominance	In decode at batch one, a projection reads each weight once and does about one operation per byte read, so HBM bandwidth alone sets its time.	a full latency model: rank designs by HBM bytes
Concavity	A larger tile reuses more data until the kernel becomes compute-bound. Past that point it gains nothing and only uses more shared memory.	every tile size except the few near the knee
Monotonicity	Giving each block more shared memory never forces a slower tiling, because every tile that fit before still fits.	regions whose valid lower bounds exceed the incumbent
What is independent
Near-decomposability	The tile staged from HBM into shared memory and the blocking inside the registers interact only through the size of the shared-memory tile.	one three-way search: two smaller ones remain

Table 1: The nine structures, each with an example from a real GPU, grouped by what they do to the search.

Level	Data transactions at this level	Software-stack structure introduced	Chip structure introduced	What must be proved
Workload specification	Required results: what is computed, not how	Required computation, allowed inputs, operator semantics	—	Independent reference contract
0. Computation graph	Tensor values flowing along graph edges	Operators, edges, parameter and state versions	—	Matches the workload specification
1. Operator transformation	Reductions and partial results inside each operator	Fusion, decomposition, reduction partitioning, algorithmic families (e.g. materialized vs. streaming attention)	—	Operator semantics and dependencies preserved
2. Tensor execution mapping	Tile copies between memory levels; values held in storage slots	Tiles, layouts, memory placement, processor mapping	Register and on-chip memory capacity, number of processing units	Coverage, exact-once reductions, address maps, value lifetime
3. Instruction scheduling	Issued and completed transfers; synchronized reads	Instruction selection, transfers, synchronization	Instruction interface, transfer mechanisms, software–hardware boundary	Operand readiness, visibility, progress
4. System architecture	Transfers across units, memory channels and interconnect	Placement of work and data across units	Execution resources, memory hierarchy, interconnect	Resource compatibility, communication contracts

Table 2: Design objects, decisions and what must be proved at each refinement level.

Step	Coarse transaction $\to$ finer transactions	The optimizer gains	The verifier must prove
1. Reduction partition	one sum of $K$ products $\to$ partial sums over groups, then a combine	the assignment $x_{kr}$ of each reduction index $k$ to a group $r$	exact-once: every product contributes exactly once
2. Physical storage	a logical partial result or operand $\to$ an occupancy of a reusable buffer	buffer assignments and the order $z$ of values sharing a buffer	lifetime: a value survives until its last read
3. Asynchronous transfer	an atomic write $\to$ an issue event and a later completion	issue and completion times; the transfer mechanism (software, instruction or controller)	readiness: an operand is read only after its transfer completes
4. Double buffering	one buffer per value $\to$ generations rotating through $S$ slots, loaded $P$ tiles ahead	slots $S$ , prefetch distance $P$ , trailing barrier $\beta$ , and the shared-memory capacity that bounds them	generation correctness: a consumer reads the right generation; lifetime becomes $P\leq S-2+\beta$ (Listing 2.2 )
5. Shared resources	an untimed transfer or access $\to$ requests to banks, ports and bounded queues	bindings of requests to banks and ports; queue depths and port counts on the chip	conflict freedom, no deadlock, and progress under the declared arbitration contract

Table 3: A five-step GEMM refinement and the decisions exposed at each step.

Source	What goes wrong	Repair
Representation	The template cannot express the best design	A new or revised template
Correctness constraints	The preconditions exclude safe designs	A less restrictive condition that is still sound
Optimization	The solver stops short of the model optimum	A better encoding or search
Prediction	The cost model ranks designs wrongly	A better model, fitted to measurements

Table 4: Four sources of design loss and the repair each calls for.

Figure 2: Weakest precondition as least design loss, for the shared-memory tiling template. The exact precondition equals the safe set and contains the optimum on its boundary. A conservative precondition (always keep the trailing barrier) is sound but excludes that optimum, a precondition loss of

1.34\%

on the

1000^{3}

GEMM. An unsound precondition (

P\leq S-1

) allows an unsafe design that the solver then selects and the verifier catches.

Study	Evidence	Who supplied what	What it does not show
GB10 layers ( 5.2 )	Device latency of complete layers against SGLang; numerical checks on tested inputs	agent wrote program families and cost expressions; production components inherited; solver selects the instance	No formal proof of the GPU program families
White vs. black box ( 5.3 )	One construction run per method from the same eager code under equal caps	agent wrote both programs; host-side help in diagnosis	No demonstrated selection gain over copying; construction-run variability
Template reuse / construction ( 5.4 )	Fixed-family transfer; three construction runs per knowledge condition	Fixed families transferred; agent constructs new families; solver selects instances	Total construction cost including inherited knowledge
Ventus co-design ( 5.5 )	Cycle simulation, calibrated aggregation and extrapolation	Study menus and references set by the authors; solver selects	Cross-study comparisons under a common reference
Wall relaxation ( 5.5 )	Exact inner solves on a 12-chip capacity domain; purchases confirmed by simulation	Author-defined menus; solver-based outer search	A general search-efficiency advantage; random search finds the same optimum
Gemmini ( 5.5 )	Analytical co-design on DoSA’s BERT GEMM list with Timeloop/Accelergy	agent derived costs from the Gemmini source and wrote the enumeration	Automated template construction/reuse loop; complete Transformer inference

Table 5: What each study shows and where it stops.

	Fixed-hardware software	Hardware–software co-design
Platform	NVIDIA GB10; TileLang 0.1.15 [ 22 ]	Ventus, parameterized RISC-V GPU
Workload	Qwen3-8B and Qwen3.5-35B-A3B [ 23 , 24 ] ; BF16, batch one	Qwen2.5-0.5B
Input scenarios	Prefill 128/512/2048/4096; decode history 512/2048/4096/8192	Prefill 128/512; 16 decode steps from history 128/512
Design freedom	Graph structure, kernels, layouts, schedules	Same software freedoms within the study menus, plus chip resources
Primary metric	Complete-scope device latency; service TTFT/TPOT	Worst-scenario normalized cycles at a fixed area budget
Efficiency	Recorded search/build cost and reuse controls	Formulation/search cost and incremental verification cost

Table 6: The two experimental settings. GPU timing, Ventus timing models and checker runs are reported separately.

Figure 3: Complete-scope performance across the eight scenarios of each model. Each point is the SGLang-to-Formulaic latency ratio reported in Tables 7 and 8 ; the dashed line denotes equal performance. P denotes prefill length and D denotes decode history. Both panels use the same scale.

Scenario	Eager	SGLang	Formulaic	Eager	SGLang
				Speedup over
Prefill 128	2211.4	1920.7	1796.3	$1.231\times$	$1.069\times$
Prefill 512	4797.8	2851.8	2659.7	$1.804\times$	$1.072\times$
Prefill 2048	36476.3	11121.9	10087.9	$3.616\times$	$1.103\times$
Prefill 4096	153917.9	22799.9	20969.3	$7.340\times$	$1.087\times$
Decode 512	2255.1	1811.8	1680.3	$1.342\times$	$1.078\times$

Table 7: Qwen3-8B complete-layer latency (

\mu\mathrm{s}

), BF16, batch one. SGLang uses the pinned native-kernel path.

Scenario	SGLang	Formulaic	Speedup
Prefill 128	22411.5	24938.8	$0.899\times$
Prefill 512	31366.2	29034.8	$1.080\times$
Prefill 2048	53139.5	50752.8	$1.047\times$
Prefill 4096	83451.5	79748.2	$1.046\times$
Decode 512	2843.7	2784.0	$1.021\times$
Decode 2048	2873.9	2808.5	$1.023\times$

Table 8: Qwen3.5-35B-A3B complete four-layer group latency (

\mu\mathrm{s}

), BF16, batch one. Each group contains three linear-attention layers and one full-attention layer, all with MoE.

Figure 4: Complete MoE four-layer decode group, measured without CUDA Graph capture. Each row compares all three paths in one timing batch. D2048 uses repaired MMA-based expert projections and newly measured controls; other rows retain their independently measured implementations. The repaired D2048 candidate achieves 5.97

\times

speedup over eager and approximately matches SGLang.

Figure 5: Matched-budget construction across all four histories. Left: speedup over eager on a logarithmic scale. Right: speedup over the faster FlashInfer mode (TC), including the copied development assignment. Values are ratios of the same-row pooled medians in Table 9 . Higher is better in both panels.

History	Eager	Direct	Formulaic	Copied	FI TC	FI SIMT
512	46.14	8.44	7.78	5.67	6.78	12.02
2048	374.22	17.61	11.00	10.16	11.32	15.56
4096	783.15	30.01	15.74	15.74	15.90	20.34
8192	1597.65	141.98	138.16	138.16	137.05	138.41

Table 9: Programs built from eager code and fixed before measurement, across four histories, in

\mu\mathrm{s}

. Each row measures all paths in one process after warming each implementation immediately before its timing block. Formulaic uses the MIP-selected instance; copying the development assignment is reported separately. This compares attained performance, not total optimization cost.

KV length	Task only	+ Executable template
1025	0.835 $\times$	1.488 $\times$
6145	0.942 $\times$	1.158 $\times$
24577	1.038 $\times$	1.031 $\times$

Table 10: Does prior knowledge help the agent construct a faster attention program? Entries are speedups over FlashInfer, using median latency across three independent runs per cell. Values above 1 beat FlashInfer; below 1 are slower. All conditions use the same tools and within-task budgets.

Objective	SW only	HW only	Joint	Speedup over SW
Prefill	0.758	0.440	0.377	2.01 $\times$
Decode	0.934	0.454	0.428	2.18 $\times$
All scenarios	0.934	0.454	0.428	2.18 $\times$

Table 11: Qwen2.5-0.5B co-design on Ventus at a 1.11 mm 2 area ceiling. The first three columns give cycles normalized to the reference software and chip (lower is better). The last column gives joint speedup over software-only optimization (higher is better).

	Prefill		Decode		Mixed
Method	1024/128	2048/256	512/256	2048/256	512/256	2048/256
Fixed hardware	.642 (1)	.231 (1)	.431 (1)	.269 (1)	.642 (1)	.269 (1)
Sequential	.642 (1)	.231 (1)	.431 (1)	.269 (1)	.642 (1)	.269 (1)
Random + exact inner	.231 (12)	.231 (12)	.269 (12)	.269 (12)	.269 (12)	.269 (12)
Wall relaxation	.231 (12)	.231 (3)	.269 (8)	.269 (3)	.269 (11)	.269 (3)
Coupled wall	.231 (16)	.231 (4)	.269 (11)	.269 (4)	.269 (16)	.269 (4)

Table 12: Capacity search across three objectives and two starting chips. Each cell gives the final simulated cycle ratio, followed by the number of distinct inner problems in parentheses; lower is better. Column headers specify vector/scalar register slots per SM.

Figure 6: Quality and search work from the smaller starts. Markers show final selected points checked by instruction simulation. The dashed curve and shaded range show the frozen-model random-search trajectories across five seeds; intermediate random points are not independently replayed. Overlapping markers have the same quality and query count.

Method	Energy ( $\mu$ J)	Latency (cycles)	EDP ( $10^{9}\,\mu$ J cycles)	Area (mm 2 )
Default chip + CoSA	2631.85	2,963,456	7.7994	0.708
DoSA	1983.04	917,508	1.8195	14.088
Formulaic	1655.24	917,508	1.5187	10.043

Table 13: BERT operator-list optimization on Gemmini. Lower energy, latency, energy–delay product (EDP) and area are better. All rows use the same Timeloop/Accelergy evaluation policy.

Added refinement	Full (ms)	Progressive (ms)	Queries, full/ours	Speedup
Reduction partition	25.5	26.3	8/8	0.97 $\times$
Storage	73.8	48.7	23/15	1.51 $\times$
Asynchronous transfer	289.0	200.6	43/20	1.50 $\times$
Double buffering	528.1	218.9	65/22	2.41 $\times$
Shared resources	958.4	380.6	92/27	2.51 $\times$

Table 14: Measured verification cost along the refinement chain. Times are medians of seven paired repetitions; speedups are paired statistics. Progressive is our proof-reuse strategy.

Sequence	Full	Node reuse	Query reuse	Full/Query
7 agent proposals	10.74	10.56	8.56	1.25 $\times$
59-version history	83.04	81.66	72.17	1.15 $\times$

Table 15: Verification replay on an actual optimization history, in seconds. Seven agent proposals have three paired replays; the 59-version history includes 52 host diagnostic executions and has one replay. Speedups use paired ratios.

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Slots $S$	Trailing barrier	Safe prefetch distances $P$
1	yes	0
1	no	none
2	yes	0, 1
2	no	0
3	yes	0, 1, 2
3	no	0, 1

Appendix

Table 16: Safe schedules of the shared-memory tiling template. The verifier’s accepted set equals the template’s precondition

P\leq S-2+\beta

on all 24 combinations.

GEMM	$(T_{m},T_{n},T_{k},S,P,\beta)$	Shared memory	Modeled time
$4096^{3}$	$(128,256,16,3,1,0)$	72 KiB	1826.9 $\mu$ s, memory-bound
$64\times 4096\times 4096$	$(64,64,16,3,1,0)$	24 KiB	75.1 $\mu$ s, memory-bound
$1000\times 1000\times 1000$ , ragged tails	$(128,128,32,3,1,0)$	96 KiB, at capacity	53.1 $\mu$ s, compute-bound

Appendix

Table 17: Designs selected by the template MILP. Every row passes all 12 conditions; times are modeled.

Precondition given to the solver	$4096^{3}$	$64\times 4096^{2}$	$1000\times 1000\times 1000$
Exact, $P\leq S-2+\beta$	optimal, passes	optimal, passes	optimal, passes
Too strong: always keep the trailing barrier	+0.0%, passes	+0.0%, passes	+1.34% , passes
Too weak: $P\leq S-1$ , barrier ignored	rejected by verifier	rejected by verifier	rejected by verifier

Appendix

Table 18: Contract ablation. Percentages are precondition loss in modeled latency relative to the exact contract.

Variant	Failing condition	Replayed defect
Floor-divided grid (tail uncovered)	coverage	missing reduction terms
Unguarded tail	no phantom	write outside $C$ ; padding term added
Overlapping tiles (stride $T-1$ )	exact-once	$C[127,0]$ receives $A[127,0]\,B[0,0]$ twice
Single buffer with prefetch one	lifetime	missing term
Double buffer, $P=1$ , no trailing barrier	lifetime	the race of Figure 7
Missing leading barrier	readiness, lifetime	reads of uninitialized slot elements

Appendix

Table 19: Faults injected into the proved

1000\times 1000\times 1000

design, all rejected with a replayed defect.

Figure 7: The counterexample the verifier replays for the unsound precondition, with

S=2

slots and prefetch distance

P=1

. (a) Without a trailing barrier (

\beta=0

), warp 1 finishes reading slot 0, crosses no barrier, and prefetches k-tile 4 into slot 0 while warp 0 is still waiting to read k-tile 2 from it. Output

C[0,1]

then accumulates

A[0,2]\,B[4,1]

instead of

A[0,2]\,B[2,1]

: one term is lost and a foreign one is added. (b) With the trailing barrier (

\beta=1

), which the exact precondition

P\leq S-2+\beta

requires for this design, the load waits until every warp has finished reading the slot.

M	Solver total	Build/pack	SGLang	Reused selection	Speedup
128	19.060	2.878	1349.65	1264.97	1.067 $\times$
512	19.162	2.851	1984.91	1505.20	1.319 $\times$
2048	16.782	2.575	6980.16	5973.93	1.168 $\times$
4096	17.081	2.499	13736.33	12096.62	1.136 $\times$

Appendix

Table 20: Measured reuse components for unchanged GateUp source and expression on Qwen2.5-7B layer-0 weights, input dimension

K=3584

and intermediate dimension

I=18944

. Each row uses a separate paired comparison with production; activations are synthetic. Solver and build/packing columns are seconds, kernel columns microseconds. Construction of the original family is excluded.

History KV	Split	Online ( $\mu\mathrm{s}$ )	Formulaic ( $\mu\mathrm{s}$ )	Paired speedup
3072	4	66.464	20.043	3.296–3.383 $\times$
6144	4	131.915	67.573	1.942–2.200 $\times$
1536	4	34.882	11.442	3.047–3.052 $\times$
5120	16	108.400	29.826	3.637–3.644 $\times$

Appendix

Table 21: An attention template reused on new history lengths. Each row has its own timing batch; the 1536 and 5120 rows check all six configurations. All implementations pass complete-output checks on the tested inputs.

Task	Condition	Latency ( $\mu\mathrm{s}$ )	vs. FlashInfer	Active cost (s)
$N=1025$	Task only	5.598 [5.326, 6.400]	0.835 $\times$	2225
	Executable template	3.142 [3.137, 3.443]	1.488 $\times$	2069
$N=6145$	Task only	71.725 [58.424, 72.786]	0.942 $\times$	2089
	Executable template	58.362 [56.626, 61.149]	1.158 $\times$	2083
$N=24577$	Task only	422.976 [419.722, 423.445]	1.038 $\times$	1826
	Executable template	425.649 [424.966, 468.482]	1.031 $\times$	2075

Appendix

Table 22: Knowledge-assisted construction on three attention tasks. Latency is the median [minimum, maximum] across three independent agent runs. Speedup compares that median with the faster FlashInfer mode in the common batch. Recorded active cost is the median sum of agent construction, solving and worker execution time per run.

Sequence	Versions	Full (s)	Node (s)	Query (s)	Full/Node	Full/Query
Controlled, 1 shape	16	4.06	2.34	–	1.72 $\times$	–
Controlled, 2 shapes	16	6.48	3.94	–	1.66 $\times$	–
Controlled, 4 shapes	16	11.74	7.24	–	1.62 $\times$	–
Controlled, 8 shapes	16	25.19	15.87	–	1.59 $\times$	–
agent proposals	7	10.74	10.56	8.56	1.02 $\times$	1.25 $\times$
Complete execution history	59	83.04	81.66	72.17	1.02 $\times$	1.15 $\times$

Appendix

Table 23: Verification cost across program revisions. Times are sequence totals in seconds (medians for three replays); speedups are medians of paired full/reuse ratios, so they need not equal ratios of displayed medians. Query reuse includes node reuse. A dash denotes an unmeasured strategy. The final row is one replay; all other rows have three.

Hardware-Software Co-Design

Hardware-software co-design jointly shapes algorithms, software, and computing hardware to meet performance, energy, cost, and deployment constraints.

See all 70 papers

Can Agents Design Better Chips with a Higher Level Abstraction?
Sep 17, 2026Zijian Ding, Yang Zou, Yizhou Sun +1Electronic Design Automation LLM Agent Workflow Optimization
UCLA Los Angeles, CA, USA
Agent Factories for High Level Synthesis: How Far Can General-Purpose Coding Agents Go in Hardware Optimization?
Mar 26, 2026Abhishek Bhandwaldar, Mihir Choudhury, Ruchir Puri +1Electronic Design Automation Multi-Agent Coding
IBM Corporation
Agent-Orchestration in Autonomous Chip Design
Aug 14, 2026Linyang LiLLM Agent Orchestration Electronic Design Automation
Nova Silicon

Sep 17, 2026J/K move · Enter open · S save

Can Agents Design Better Chips with a Higher Level Abstraction?

Zijian Ding, Yang Zou, Yizhou Sun, Jason Cong

UCLA Los Angeles, CA, USA

Electronic Design Automation LLM Agent Workflow Optimization

Open paper AskPDF arXiv

Large Language Model (LLM) agents are increasingly being explored for chip design, but most existing approaches operate directly at RTL. We ask whether agents can design better chips by leveraging higher-level abstractions. We compare Direct RTL Design, Agent-based HLS Design, Post-Compiler HLS Refinement, and Post-HLS RTL Refinement, and combine Agent-based HLS Design with Post-HLS RTL Refinement as Agent-based HLS with RTL Refinement (AHRR). We use FPGAs as a practical, easy-to-deploy platform for end-to-end evaluation, but note that the design-flow tradeoffs we study are largely independent of the target technology. Across a diverse 11-tasks benchmark suite, AHRR achieves a 2.6

\times

geometric-mean speedup over Direct RTL Design across our benchmark suite. Case studies show that HLS distills design knowledge into abstractions that agents can leverage, while RTL refinement recovers lower-level optimization opportunities. Together, these results make AHRR a promising workflow for agentic chip design. The code and evaluation artifacts are available at https://github.com/ZijD/AHRR.

Abstract

Hardware-Software Co-Design

Explore similar work

Can Agents Design Better Chips with a Higher Level Abstraction?

Agent Factories for High Level Synthesis: How Far Can General-Purpose Coding Agents Go in Hardware Optimization?

Agent-Orchestration in Autonomous Chip Design