Abstract
We demonstrate that the StegVerse autonomous mathematical problem-solving framework achieves measurable cost reduction through execution-path optimization. Starting from an unoptimized baseline of $0.061659 per problem, we validate a 50% cost reduction through direct batch execution at $0.0308295 while preserving identical formal-proof output quality.
We document a critical negative result: cache-framing reduced apparent cost to $0.003 but changed the semantic output type, making it an invalid optimization. The recommended production configuration is a tiered Haiku preprocessing plus Sonnet batch proof-generation pipeline, which costs $0.0333 per problem, preserves full proof quality, adds routing intelligence, and achieves a 46% savings versus baseline.
Executive Summary
| Baseline cost | $0.061659 per problem |
| Best validated savings | 50% via direct batch (Sonnet) |
| Recommended production | 46% via tiered routing (Haiku → Sonnet batch) |
| Invalid optimization | 95% apparent savings (rejected — semantic boundary violation) |
| Quality maintained | Yes — the optimized direct-batch run preserved the required formal-proof output type and structural proof components |
| Total validation spend | $0.1095 (4 runs) |
Presentation Claim
StegVerse validated a 50% proof-generation cost reduction using direct batch execution, while preserving the required formal-proof output structure. Its recommended production routing achieves 46% savings by adding Haiku preprocessing before Sonnet batch proof generation. A cheaper cache-framed run was rejected because it changed the task.
Claim Boundary
This paper proves cost reduction for formal proof generation under preserved task identity, output type, quality threshold, and auditability. It does not claim that every optimization path is valid, nor that the full autonomous research pipeline is cheaper than a single proof-only run.
The central result is that the cheapest admissible run is not the cheapest observed run. The valid optimization is the cheapest run that preserves the semantic task boundary.
Quality Equivalence Criteria
Output quality was evaluated by task identity, output type, and required structural components. A valid run had to produce a formal proof for SV-MATH-001, including definitions, theorem structure, proof reasoning, and formal or categorical rewriting content. Runs were rejected if cost reduction was achieved by changing the requested task, omitting the proof, or producing meta-analysis instead of proof content.
Methodology
Validation Run (VAL-001)
Purpose: Prove pipeline works end-to-end. Cost: $0.015. Model: claude-sonnet-4-6. Result: API connectivity confirmed, secret loading verified.
Baseline Run (BL-001)
Unoptimized execution. Model: claude-sonnet-4-6, extended thinking enabled, 4096 max tokens. Cost: $0.061659. Output: Full formal proof with abstract, definitions, theorems, categorical rewriting system. Latency: 52.54s.
Optimized Run v1 — Cache Framing (OP-001)
REJECTED. Batch API + prompt caching enabled. Cost: $0.003 (95% apparent savings). However, output changed to meta-analysis of prompt injection rather than the requested formal proof. The cache-framing language ("cached invariants") triggered the model to analyze prompt structure rather than solve the problem.
Critical lesson: Prompt structure determines output type, not just model capability.
Optimized Run v2 — Direct Batch (OP-002)
VALIDATED. Direct prompt + batch API only. Cost: $0.0308295. Tokens identical to baseline (4,169). Output: Full formal proof preserving the required structural components. Latency: 52.56s. 50% cost reduction with no observed loss under the defined quality-equivalence criteria.
Combined Optimization — Tiered Routing (COMB-001)
RECOMMENDED PRODUCTION. Three-phase pipeline:
- Phase 1 (Haiku): Preprocessing and complexity classification. $0.0025, 529 tokens. Classified problem complexity, estimated token needs.
- Phase 2 (Sonnet batch): Main proof generation. $0.0308, 4,160 tokens. Complete formal theory with definitions and theorems.
- Phase 3 (Escalation check): Sonnet output sufficient; Opus not needed. $0.00.
Total: $0.0333, 4,689 tokens. 46% savings vs baseline with added routing intelligence.
Comparison Table
| Run | Mode | Cost | Savings | Tokens | Quality | Verdict |
|---|---|---|---|---|---|---|
| BL-001 | Unoptimized | $0.0617 | 0% | 4,169 | Full proof | Baseline |
| OP-001 | Cache framing | $0.003 | 95% | 489 | Meta-analysis | REJECTED |
| OP-002 | Direct + batch | $0.0308 | 50% | 4,169 | Full proof | BEST VALIDATED |
| COMB-001 | Tiered models | $0.0333 | 46% | 4,689 | Full proof + classification | RECOMMENDED |
Critical Lessons
- Prompt structure determines output type. Cache framing triggered meta-analysis instead of proof. Use direct prompts for mathematical problems; cache only for invariant libraries.
- Batch API provides reliable 50% discount without quality loss. Enable batch API for all non-urgent production runs.
- Haiku preprocessing is viable for complexity classification. Use Haiku for problem triage before Sonnet main proof.
- Opus escalation not needed for standard StegVerse-native problems. Reserve Opus for novelty spikes > 0.95 only.
Production Recommendations
Default pipeline: Haiku preprocessing → Sonnet batch main proof → Escalation check
Expected cost per problem: $0.0333
Public claim language: Use the 50% direct batch result as the strongest validated savings claim; use the 46% tiered result as the recommended production architecture because it adds classification and routing intelligence.
Invalid claim to avoid: Do not claim 95% deployable savings from OP-001. That run changed the output type and is not a valid optimization.
Governance Interpretation
Cost optimization must itself be admissible. The optimized execution path must preserve task identity, output type, quality threshold, and auditability. Apparent savings are rejected when those conditions fail.
OP-001 is therefore not a failed run in the ordinary sense. It is evidence that optimization must be governed. A cheaper path that changes the task is not a cost reduction; it is a semantic boundary violation.
Extension Path
The next extension is the complete autonomous research pipeline: Haiku complexity mapping, Sonnet extended reasoning, Lean formalization, determinism verification, implication harvesting, and publisher documentation. This extension should be reported separately from the proof-only cost-reduction result because it produces more artifacts and therefore has a different cost basis.
Appendix
- API provider: Anthropic
- Models tested: claude-haiku-4-5, claude-sonnet-4-6, claude-opus-4-6
- GitHub Actions minutes used: ~15 minutes total
- Total API spend validation: $0.1095
- Date range: 2026-05-02
- Repository: GCAT-BCAT-Engine/workflows