solver

Verifiable Environments

This skill helps you answer three questions:

1. Can I build an automated evaluator for this problem?
2. What verification tool should I use?
3. How do I construct the evaluator?

Foundation: the P vs NP asymmetry (Cook, 1971; Karp, 1972). Problems amenable to LLM+verifier loops are those where candidate verification is computationally cheaper than candidate generation. This is the only rigorous foundation — everything else is heuristic.

The Core Requirement

Every working LLM+verifier system converges on one operational requirement: a deterministic function that scores candidates without human judgment.

• FunSearch: evaluate(program) -> score (Romera-Paredes et al., Nature 2024)
• AlphaCode: test cases with expected output (Li et al., Science 2022)
• DeepSeek-R1: rule-based rewards — match answer (math) or pass tests (code) (DeepSeek-AI, Nature 2025, arXiv:2501.12948)

If you can write this function, the problem is amenable. If you can't, it isn't. There is no deeper formalization — this is where the theory ends and domain judgment begins.

Verifiability Assessment

Two questions to answer, in order:

1. Can verification be automated? Can you write code that checks a candidate's correctness without human judgment? If yes, proceed. If no, the problem is not amenable as stated. Consider reformulating to extract a verifiable sub-problem.

2. What verification tool fits? Match your problem to the right tool:

| If your verifier needs to... | Use | Guarantee | |------------------------------|-----|-----------| | Prove properties for ALL inputs | Z3 (SMT solver) or Lean4 (proof assistant) | Sound (within decidable fragment / proof kernel) | | Check pre/postconditions on code | Dafny -> Boogie -> Z3 | Sound for specified contracts | | Run candidates against test cases | Test suite + sandbox | Empirical (bounded by test coverage) | | Aggregate over stochastic runs | Simulation (N>30 runs) | Statistical (confidence intervals) | | Judge quality subjectively | LLM-as-judge | None (non-stationary, noisy) |

Reference: rules/assess-verifiability.md for the full assessment process. Reference: rules/verification-tools.md for tool APIs.

Practitioner Heuristics

Explicitly labeled as heuristics, not formal criteria.

Wei (2025, blog post) identifies 5 properties correlated with LLM+verifier success:

• Objective truth — would two independent evaluators agree?
• Fast verification — does evaluation take <1s per candidate?
• Scalable verification — can you evaluate 1000 candidates in parallel?
• Low noise — does the same candidate get the same score on re-evaluation?
• Continuous reward — do small improvements produce small score changes?

These are useful for quick triage but not formally validated. A problem can satisfy all 5 and still be hard if the evaluator is buggy. A problem can satisfy 3 and work fine if the evaluator is well-designed.

Keles (2025, blog post) observes: "Verifiability is the limit" — LLM capability isn't the bottleneck; the ability to check outputs is. This explains why LLMs succeed at frontend (visual verification) but struggle with backend (test infrastructure required). Directionally correct, not formally defined.

Reference: rules/assess-verifiability.md for how to apply these.

Evaluator Construction

Once you've assessed verifiability and chosen a tool, construct the evaluator:

• Formal verification (Z3/Lean4/Dafny): Encode properties as formulas/types/contracts. Verifier returns sound yes/no + counterexample/error.
• Test-based verification: Write test cases. Use staged evaluation (easy->hard) to fail fast. SDK: BenchmarkEvaluator + CascadeEvaluator.
• Simulation-based: Run N>30 times, aggregate. Separate safety properties (hard constraint, any violation fails) from performance metrics (averaged). SDK: CompositeEvaluator.
• LLM-as-judge: Secondary metric only (weight <= 0.2 in composite). Never primary fitness for evolutionary search.

All evaluators implement: evaluate(program) -> EvaluationResult(score, metrics, feedback, passed)

Reference: rules/design-evaluator.md for construction templates.

Rule Index

| Rule | When to Read | |------|-------------| | rules/assess-verifiability.md | Before starting any solver project — determine if and how the problem is verifiable | | rules/verification-tools.md | When choosing between Z3, Lean4, Dafny, test suites, simulation | | rules/design-evaluator.md | When constructing the evaluator — templates per verification tool | | rules/staged-evaluation.md | When evaluation is expensive (>5s per candidate, 100+ candidates) | | rules/quality-diversity-metrics.md | When using evolutionary search — multi-metric design | | rules/failure-modes.md | Before shipping any evaluator — known failure modes |

SDK Integration

Optional. This skill works without the SDK — patterns are implementable standalone.

If available:

from solver_sdk.core.evaluator import Evaluator, BenchmarkEvaluator, CompositeEvaluator
from solver_sdk.core.types import Program, EvaluationResult, RichEvaluationFeedback
from solver_sdk.verification.cascade import CascadeEvaluator
from solver_sdk.verification.feedback import FeedbackGenerator
from solver_sdk.verification.formal import FormalVerifier  # stubs — requires external toolchains

SDK types are referenced in templates but all patterns are implementable with standard Python.

Epistemic Honesty

• No formal decision procedure exists for "is this problem verifiable?" Domain knowledge is required.
• The verification tool landscape (Z3, Lean4, Dafny) provides sound guarantees within their respective decidable fragments. Outside those fragments, you're in empirical territory (test suites, simulation).
• Practitioner heuristics (Wei, Keles) are directionally useful but not predictive. Don't rely on them for go/no-go decisions.
• When uncertain, build a minimal evaluator prototype and test it on known-good and known-bad candidates before committing to a full system.