Research map / Large language models / Agents, code and math

GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching

NeurIPS 2026 · Large language models › Agents, code and math · approach: LLM-guided program synthesis · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces SiMBA, a cache-free GPU bottom-up enumerator that synthesizes mixed-Boolean arithmetic expressions from input-output examples via a bijection between integers and expressions, outperforming VFB and cvc5 on a new 2340-instance benchmark.

Problem

Synthesizing mixed-Boolean arithmetic (MBA) expressions from input-output examples scales poorly on CPUs and on prior GPU synthesizers, whose language-cache deduplication breaks down because quantitative bitvector behaviors are too numerous to cache.

Approach

Replace the language cache with a bijection between integers and RPN MBA expressions of a given size, so each GPU thread decodes its own expression, evaluates it, and discards it; the encoding is locally consistent so threads in a warp share sub-expressions and minimize divergence.

Key results

• Simba solves nearly all instances up to size 11 and is the only tool solving sizes 12-16, while VFB and cvc5 fail beyond size 11.
• Against VFB on 615 commonly solved instances, Simba is faster on 90% with median speedup 1.6x; 634 instances are solved only by Simba.
• VFB cache reaches 2.1 GB at size 10 for k=5 and runs out of GPU memory at size 11, while Simba uses constant memory; Simba is about 4x faster than the random-thread-id variant Simba-RTid.

Surprising findings

• Simba's solving advantage over the random-thread-ID variant is a consistent 4x factor, showing that warp-locality of the encoding matters substantially.

Limitations

• Requires a GPU and gives no benefit on CPU-only hardware.
• Candidate count grows super-exponentially, so practical only up to size around 16.
• Does not handle noisy oracles or synthesize numerical constants.

Experimental setup

Datasets: 2340 randomly generated MBA expressions (new benchmark, sizes 5-30, k=2-10)

Benchmarks: new 2340-instance MBA synthesis benchmark

Metrics: instances solved wall-clock solving time speedup cache size and memory % of formulas cached

Baselines: VFB cvc5 Simba-RTid

Builds on: VFB GPU synthesis bottom-up enumerative synthesis MurmurHash3

Closest papers by meaning

• Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis (AAAI 2025 · similarity 0.85)
• CUDABench: Benchmarking LLMs for Text-to-CUDA Generation (NeurIPS 2026 · similarity 0.84)
• Retrieval-Guided Reinforcement Learning for Boolean Circuit Minimization (ICLR 2024 · similarity 0.83)
• PCBSchemaGen: Reward-Guided LLM Code Synthesis for Printed Circuit Boards (PCB) Schematic Design with Structured Verification (NeurIPS 2026 · similarity 0.83)
• Scalable and Effective Arithmetic Tree Generation for Adder and Multiplier Designs (NeurIPS 2024 · similarity 0.82)
• EasySpec: Layer-Parallel Speculative Decoding for Efficient Multi-GPU Utilization (NeurIPS 2025 · similarity 0.82)