Skip to content

Repository files navigation

Verified Executable Search (VES)

AI can propose. It cannot grade itself.

VES is a verifier-first runtime for AI-generated executable solutions. LLMs can write candidate programs, search strategies can improve them, but the candidate never gets to decide whether it is correct or good. The host loads its artifact, recomputes the facts, records the evidence, and only then lets a judge or search policy act on it.

中文 README · v0.1.0 · Write your first verifier

VES is aimed at autoresearch, scientific/modeling workflows, optimization, and agentic code search where a generated program must be evaluated against host-owned truth, tests, constraints, or simulators.

Live Demo

🧪 Try the live demo: https://huggingface.co/spaces/235dsds/VES-Core


The problem

A typical agent loop looks like this:

LLM writes code
    ↓
code reports a score
    ↓
agent trusts the score
    ↓
agent improves the code

That is convenient, but the trust boundary is wrong. A candidate can be buggy, miscompute a metric, leak evaluation data, violate constraints, or simply print a great-looking number.

VES changes the loop to:

LLM / generator
      ↓
Candidate program                 untrusted
      ↓
Sandboxed runner
      ↓
Raw artifact                      untrusted
      ↓
──────────── host trust boundary ────────────
      ↓
ArtifactContract + SafeArtifactLoader
      ↓
EvidenceVerifier + VerificationContext
      ↓
Evidence                          verified facts
      ↓
Judge                             preferences / feasibility
      ↓
Search                            acts only on verified evidence

The core rule is simple:

Creation authority and judgment authority are separate.


30-second demo

No LLM is required for the built-in demos.

# Python 3.11+
pip install verified-executable-search

python -m examples.demo_adversarial
python -m examples.demo_search --mock

For development or the real-LLM/Docker adapters, clone the repository and install from source: pip install .[dev,ml,search].

The adversarial demo shows that candidate claims do not become truth:

candidate says: objective = 999999
VES:            self-reported score ignored

malformed / NaN / oversized / symlink artifact
VES:            rejected or blocked

valid artifact
VES:            host recomputes the evidence

The search demo shows the same verification pipeline driving improvement:

draft #1   value=33   feasible=True
draft #2   value=40   feasible=True
improve    value=51   feasible=True

BEST VERIFIED SOLUTION: value=51

The point is not that knapsack is hard. The point is that the search loop can change while the verification boundary stays fixed.


Why VES instead of one more eval.py?

A hand-written evaluator is often enough for one experiment. VES becomes useful when you want the evaluation boundary to be reusable, auditable, and safe to connect to generated code.

Ad-hoc agent loop VES
candidate may report its own metric host recomputes observations
score and feasibility often mixed together Evidence and Judge are separate
hidden truth handling is application-specific host-owned VerificationContext
artifact loading is usually plain file I/O size/path/symlink/UTF-8/JSON checks
comparison logic is embedded in scripts typed gates, objectives and directions
search history is ephemeral candidate lineage + verification records
reruns are informal fingerprinted verification replay

VES does not try to implement a verifier for every domain. It provides a verification runtime; your application supplies the domain truth.

Examples:

  • regression: candidate emits predictions; host recomputes RMSE/MAE
  • constrained optimization: candidate emits a solution; host recomputes the objective and violations
  • mechanism fitting: candidate emits parameters; host checks physical constraints and fit quality
  • code search: candidate emits executable behavior; host runs tests or a benchmark

Core model

VES deliberately separates facts from preferences.

Artifact
   ↓
Verifier
   ↓
Evidence        ← facts
   ↓
Judge
   ↓
Judgment        ← preferences

A verifier can say:

Evidence(
    observations=(
        Observation(name="rmse", value=0.31, provenance="deterministic:host"),
        Observation(name="runtime", value=1.8, provenance="deterministic:host"),
    )
)

The judge separately decides what matters:

JudgeSpec(
    objectives=(
        ObjectiveSpec(observation="rmse", direction=Direction.MINIMIZE),
    ),
)

That distinction matters: runtime may be useful evidence without silently becoming an optimization objective.


Public API

The v0.1 facade is intentionally small and split into four layers.

Verification

RawArtifact · ArtifactContract · SafeArtifactLoader · VerificationContext · Observation · Evidence · EvidenceVerifier · VerificationStatus · VerificationResult

Judgment

Gate · ObjectiveSpec · JudgeSpec · Direction · ComparisonRule · ComparisonOutcome · Feasibility · Judge · Verdict · Comparison

Problems and records

VerifiedProblem · VerificationPipeline · Candidate · VerificationRecord · VerifiedCandidate · ComparisonRecord

Search

CandidateGenerator · CodeRunner · RunResult · SearchEngine · SearchResult · AnchorPolicy · GreedyTop1Policy · BranchDiverseTopKPolicy

For new code, prefer the top-level facade:

from ves import (
    ArtifactContract,
    Direction,
    Evidence,
    EvidenceVerifier,
    JudgeSpec,
    ObjectiveSpec,
    Observation,
    VerifiedProblem,
)

See Writing a Verifier for a complete problem from scratch.


CLI: verify and replay

Verify an artifact with a built-in example:

ves verify solution.json --example knapsack --out record.json

Or provide your own VerifiedProblem:

ves verify answer.json --problem my_problem:problem --out record.json

Replay the verification later:

ves replay record.json

Replay v1 checks the problem reference, contract/context/judge fingerprints, verifier version, artifact hash, and newly recomputed evidence before reporting REPRODUCIBLE or MISMATCH.

This is verification replay, not bit-for-bit replay of the original LLM or container execution.


Search

SearchEngine is problem-agnostic. A domain provides only:

VerifiedProblem
CandidateGenerator
CodeRunner
AnchorPolicy

The same engine is tested across unrelated problem types; domain prompts and artifact semantics stay outside the engine.

result = SearchEngine(
    problem=problem,
    generator=generator,
    runner=runner,
    drafts=3,
    improves=5,
).search()

In v0.1, search supports total-order selection. Pareto judging exists, but SearchEngine deliberately fails fast for Pareto search until frontier semantics are defined properly.


Security model

Generated code is untrusted.

  • DockerProcessRunner is the supported execution boundary for untrusted code on Linux Docker.
  • LocalProcessRunner is not a security boundary.
  • SafeArtifactLoader rejects path traversal, symlinks (where O_NOFOLLOW is available), non-regular files, oversized payloads, invalid UTF-8, malformed JSON, and non-finite JSON values.
  • hidden host truth is not mounted into the candidate container; CI includes a real Docker attack test that attempts to read it.

Read SECURITY.md before using VES with hostile or generated code.


Status: v0.1.0

VES v0.1 is an early experimental release.

Stable enough to build on

  • verifier-first artifact → evidence pipeline
  • explicit verification / judgment separation
  • typed objectives and feasibility gates
  • verification records and deterministic replay
  • candidate lineage
  • safe artifact ingestion

Experimental

  • SearchEngine / AnchorPolicy APIs may evolve in v0.2
  • Pareto search is not implemented in v0.1
  • stochastic verifier replay semantics are deferred
  • real LLM + Docker search adapters currently live in source-checkout examples, not in the wheel

VES is intentionally not a multi-agent framework, task decomposer, or full mathematical-modeling system. Those belong above the core runtime.


Where this is going

The next proving ground is VES Modeling: single-file iterative search for well-defined computational modeling problems, where every candidate is graded by independent host verification rather than by the model that generated it.

The goal is not to make VES Core bigger. The goal is to find out whether this trust boundary makes real AI modeling/search workflows more reliable, reproducible, and easier to audit.


Documentation

License and attribution

MIT. VES is derived from and inspired by AIDE / aideml; see NOTICE for attribution.

About

A verifier-first runtime for independently verifying, comparing, and searching AI-generated executable solutions.

Topics

Resources

Security policy

Stars

1 star

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages