+
+
S1. Introduction (~1.5 pages)
+
+ • Agents hit ~20% on long-horizon tasks — not a capability problem, a decomposition problem
+ • The "review > generation" challenge for mathematical/scientific code
+ • Key insight: reposition humans as creativity source (issues, curation), agents as labor
+ • Three roles: contributors (create issues), maintainer (curate board, write skills), agents (execute)
+ • Contributions: (1) skill-based methodology, (2) verification stack, (3) reduction library artifact
+
+
+
S2. Why Reductions? The Goldilocks Domain (~1 page)
+
+ • Each reduction is self-contained (~50-200 LOC), formally specified, independently verifiable
+ • Round-trip correctness criterion: reduce → solve target → extract back → verify against source
+ • Practical value: QUBO as compilation target for quantum annealers, GNN solvers
+ • Contrast with SWE-Bench: homogeneous tasks enable systematic comparison
+ • Figure 1: The reduction graph (24 problems, 52 edges, variant lattice)
+
+
+
S3. System Architecture (~2 pages)
+
+ • Rust trait hierarchy: Problem → OptimizationProblem / SatisfactionProblem
+ • ReduceTo<T> trait + ReductionResult for type-safe reductions
+ • Compile-time machinery: overhead expressions, variant registration, complexity strings
+ • The design philosophy: make correctness checkable by construction
+ • Figure 2: System architecture diagram (traits, registry, verification layers)
+
+
+
S4. Skill-Based Task Decomposition (~2 pages)
+
+ 4.1 The Three Roles
+ • Contributors: open issues (creative — "is this reduction useful? non-trivial?")
+ • Maintainer: curates project board, writes/evolves skills, moves cards
+ • Agents: pick cards, execute skill pipelines
+
+ 4.2 Skills as Agent Functions
+ • check-issue: validates usefulness, non-triviality, literature correctness
+ • add-model / add-rule: brainstorm → plan → implement → test → review
+ • review-implementation: parallel subagents (structural + quality)
+ • fix-pr: resolve review comments, CI failures, coverage gaps
+
+ 4.3 Card-Based Orchestration
+ • GitHub project board as the coordination mechanism
+ • Manager agent auto-picks a card and drives it through the pipeline
+ • Human moves cards between columns (the creative decision: what to work on next)
+ • Figure 3: Pipeline diagram — issue → check → implement → review → PR → merge
+
+
+
S5. Multi-Layered Verification (~1.5 pages)
+
+ 5.1 The Verification Stack
+ • Layer 1: Rust type system — compile-time enforcement of trait contracts
+ • Layer 2: Unit tests — evaluation, serialization, edge cases
+ • Layer 3: Round-trip (closed-loop) tests — reduce, solve, extract, verify
+ • Layer 4: Overhead validation — symbolic expressions checked against actual sizes
+ • Layer 5: Materialized test data — JSON fixtures locked in version control
+ • Layer 6: Agentic review — parallel subagents with fresh context
+ • Layer 7: Documentation — paper entry forces human-readable proof sketch
+
+ 5.2 Why Layers?
+ • Each layer catches different error classes (table: which errors each layer catches)
+ • Materialized data prevents agents from silently changing tests
+ • The "lazy agent" problem: agents take shortest path to close issues
+ • Figure 4: Verification pyramid with error examples at each layer
+
+
+
S6. Evaluation (~2 pages)
+
+ 6.1 Git History Mining (quantitative)
+ • How many reductions were agent-implemented vs human-implemented
+ • Success rate per skill invocation (first-attempt pass rate)
+ • Review rounds before merge
+ • Error taxonomy: what went wrong and which layer caught it
+ • Coverage metrics across the codebase (>95% target)
+
+ 6.2 Case Studies (qualitative, 2-3 reductions)
+ • Simple: MVC → MIS — complement relationship, near-trivial mapping
+ • Complex: SAT → MIS — clause-variable gadget, quadratic blowup
+ • Multi-hop: Factoring → CircuitSAT → ILP — chain through circuit encoding
+ • For each: show the full pipeline from issue to merged PR with paper entry
+ • Highlight where human judgment was needed vs. where agent executed autonomously
+
+
+
S7. Related Work (~1 page)
+
+ • AI coding agents: SWE-agent, OpenHands, Claude Code, Devin — position vs. our skill approach
+ • AI for reductions: AlphaEvolve gadgets, URSA SAT verification — discovery vs. implementation
+ • Formal verification: VeriCoding, CLEVER — our pragmatic multi-layer alternative
+ • Physics-inspired solvers: QUBO/GNN — our graph as infrastructure for these
+
+
+
S8. Discussion & Conclusion (~1 page)
+
+ • Generalizability: what other domains have the "Goldilocks" property?
+ • Limitations: requires upfront skill engineering, domain expertise doesn't transfer
+ • The human value proposition: creativity, judgment, responsibility — not eliminated, repositioned
+ • Future: connecting to AlphaEvolve-style discovery, formal verification integration
+
+