BeTaL-GBI: Admission-Aware Benchmark Tuning and Full-Stack Verification of Geometric Belief Interfaces

Alvin Spivey; Yu Huang

cs.SEAug 21, 2026

BeTaL-GBI: Admission-Aware Benchmark Tuning and Full-Stack Verification of Geometric Belief Interfaces

Authors: Alvin Spivey, Yu Huang

Organizations: Light Imaging Technologies, Inc.

Abstract

A verification substrate is more credible when exposing errors in its own claims, not just model outputs. GBI-DCSE v3 falsified an architectural claim: the reported Fisher value epsilon ~ 0.066 satisfies the kappa^2 <= 10^4 budget only on the slice [epsilon, 3, 4, 5], while the full box [epsilon, 20]^4 requires epsilon ~ 0.326472. This erratum highlights whether an enterprise verification architecture can isolate interface failure, task competence, policy admissibility, and control integrity while keeping claims auditable. BoundaryBench v0.1 established the baseline: Qwen3-4B-Instruct-2507 completed 768 frozen executions, but 0% cleared the contract (369 failed parsing, 399 failed validation), limiting downstream selectivity metrics. This companion study evaluates three successive improvements. First, BeTaL-GBI v0.2 applies Benchmark Tuning with an LLM-in-the-loop over 2,218,750,380 grid points, separating format admission from conditional performance (rho_adm = N_admitted/N; rho_task = N_verified/N_admitted). Following schema repair, a model-free feedback search achieves a 2.87% mean held-out target gap, outperforming non-feedback baselines (13.61%, 11.46%). Second, GBI v2 swaps static keys for a reference-independent witness state W and policy P. Across 512 synthetic tasks, a 16-gate policy detects all 116 injected severe contradictions and accepts all 99 clean records (broad denominator: 4.27%). Hallucinator and evidence-forger surrogates are blocked with zero silent promotions. Third, GBI-DCSE v3 maps 99 claims to machine-readable evidence: 95 of 96 testable claims pass, with 148 standalone checks executed without failure. The harness exercises signed ledgers, PBFT quorums, and enclave forgery across 62 configurations. Under synthetic conditions, GBI-DCSE is a selective, policy-versioned, self-auditing test and routing substrate.

Figures & tables

Synthetic proposal	Authoritative context	Example policy action	What GBI does not decide
Amoxicillin medication request with a record of serious penicillin/beta-lactam hypersensitivity	FHIR AllergyIntolerance is designed to represent patient-specific risk from substance exposure and can inform clinical decision support; current U.S. AMOXIL labeling lists a history of serious hypersensitivity to amoxicillin or other beta-lactams as a contraindication [ 12 , 13 ] .	A version-pinned local policy could refuse autonomous commit and require named clinical review or an authorized override with provenance.	It does not diagnose an allergy, select an alternative antibiotic, or determine patient-specific treatment.
Metformin medication request with required renal-function evidence absent or stale	Current DailyMed labeling directs renal-function assessment before initiation and periodically thereafter, with explicit eGFR-related restrictions [ 14 ] .	If the institution’s declared $P$ requires qualifying renal context, missing evidence can route the proposed write to abstention, quarantine, or expert review until the required evidence is present.	It does not set an individualized dose, diagnose renal impairment, or independently decide whether metformin is clinically appropriate.

Table 1: Two synthetic healthcare boundary cases used to ground the abstract verification objects. Clinical facts cited here motivate the evidence fields; the GBI policy examples remain institution-specific and non-clinical.

Boundary	Evaluated here	Not claimed
Model behavior	Frozen v0.1 Qwen outputs are a historical empirical baseline; v0.2–v3 evaluate benchmark and verification machinery.	General hallucination containment, frontier-model capability, or new LLM performance in v0.2–v3.
Clinical authority	Synthetic witness/policy states route proposed EHR actions and expose the reason for refusal/review.	Diagnosis, treatment recommendation, autonomous prescribing, clinical safety, medical-device validation, or replacement of clinician judgment.
Policy authority	Deterministic execution, version binding, ablations, replay, and reference independence of the declared $P$ .	That an institution’s policy is clinically, legally, or ethically correct; a verifier can faithfully execute a bad policy.
Infrastructure	Software models/proxies exercise signatures, attestation checks, quorum arithmetic, certificates, rollback, receipts, and FHIR-like transaction semantics.	Live TEE attestation, a running BFT cluster, production FHIR integration, hardware-root security, or a zero-knowledge proof system.
Mathematical diagnostics	Finite Boolean, Fisher, mapping-cone, and certificate properties under declared numerical tests.	Clinical truth from geometry; mapping-cone diagnostics have zero scoring weight.
Portability	Code-level reuse is measured in a second synthetic sensitive-infrastructure instantiation.	Readiness for real healthcare, finance, government, or classified infrastructure without domain-specific authority and validation.

Table 2: System boundaries for the companion evaluation.

Parameter	Min	Max	Step/count	Operational interpretation
patient identity normalization	0	1	0.05	identity ambiguity/noise
orphan rate	0	0.5	0.05	orphan/duplicate burden
field anomaly bleed	0	0.5	0.05	structured/free-text contamination
code-system version validation	0	1	0.05	terminology/version difficulty
mapping arity	1	6	6 values	RPMS-to-FHIR mapping branching
temporal ambiguity	0	1	0.05	active/historical ambiguity

Table 4: BeTaL-GBI v0.2 parameter space.

Figure 1: BeTaL-GBI loop supplied with the v0.2 artifact. The important GBI-specific modification is the admission gate before task-level difficulty is interpreted.

Strategy	Mean search gap	Mean held-out gap	Held-out SD across levels
Feedback coordinate	5.23%	2.87%	2.30 pp
Random sampling + PPR	20.90%	13.61%	8.68 pp
Best-of-N	23.72%	11.46%	17.19 pp

Table 5: Mean gap across the four target levels. “Feedback” is the model-free feedback-coordinate implementation; the other two strategies are reimplemented baseline search strategies.

Level	Target $\rho$	Feedback	Random+PPR	Best-of-N
Hard	0.25	0.78%	6.25%	0.39%
Medium	0.50	1.17%	6.64%	0.00%
Easy	0.75	3.91%	17.58%	8.98%
Trivial	0.90	5.63%	23.98%	36.48%

Table 6: Held-out target gaps by difficulty level. Best-of-N wins two individual cells; feedback has the best mean and is substantially better at the high-performance edge.

Figure 2: Held-out gap comparison from the supplied v0.2 artifacts. These are simulator/harness results; no LLM designer or target was executed.

Target tier	Range	0.25	0.50	0.75	0.90
Low (c=0.35)	0.016–0.727	reachable	reachable	floor 2.34%	floor 17.34%
Mid (c=0.55)	0.121–0.898	reachable	reachable	reachable	floor 0.16%
High (c=0.75)	0.238–0.941	reachable	reachable	reachable	reachable

Table 7: Observed task-performance ranges on the declared monotone dial. A positive floor is a property of the reachable space, not necessarily an optimizer failure.

Quantity	Frozen floor	After repair
Admissibility rate	0.0000	0.4648
Coverage	0.0000	0.4473
Selective risk	undefined	1.0 (defined)
Verified completion	0.0000	0.0000

Table 8: Effect of deterministic repair on the frozen v0.1-style format-floor target.

Class	Count	Class	Count
Identity ambiguous	12	Identity unresolvable	12
Provenance absent	11	Required evidence absent	11
Structured field fully contaminated	11	Terminology unpinned	12
Terminology unsigned	12	Terminology unresolvable	11
Validity expired	12	Validity invalid	12
Total			116

Table 9: Injected severe contradiction classes.

Adversary	Attack	Admitted	Silent promotions
Confident hallucinator	Emits format-valid content, confidence 0.97, correct evidence references, and always requests admission. It makes 221 attempted over-admissions.	98	0
Evidence forger	Proposes the witness-consistent action but cites one nonexistent evidence reference and an unwitnessed source record.	0/512	0

Table 10: GBI v2 adversaries. These are deterministic surrogates, not language models.

Group	Measure	Result	Evidence class
Mathematical	Spectral gap $\lambda_{1}-\lambda_{0}\geq 0.15$ on genuine cone Laplacians	1.0000 (within floating point)	MEASURED

Mathematical	Fisher condition number $\leq 10^{4}$ over corrected evidence box	9998.3472	MEASURED

Systems	End-to-end enclave latency $\leq 150$ ms	0.0968 ms CPU-only software path	PARTIAL PROXY

Table 11: GBI v2 scorecard against the architecture manuscript’s proposed Table 3 targets.

Figure 3: Sensitivity/false-conflict frontier from the v2 artifact. The frozen v0.1 point has 100% sensitivity only because every record is refused; its false-conflict rate is therefore 100%.

Quarantine scope	Admissible work surviving	Liveness
Record-scoped refusals only	112/112	1.000
Declared scope incl. mandated shared freezes	84/112	0.750
Naive closure over every shared reference	84/112	0.750
Coarse family-level closure	0/112	0.000

Table 12: Liveness under four quarantine-closure semantics.

Ceiling $A$	Box-wide $\epsilon$	One-dimensional slice value
5	0.093001	0.066022
10	0.161794	0.066022
20	0.326472	0.066022
50	0.918946	0.066022

Table 13: Evidence-box lower bound required for the

\kappa_{2}\leq 10^{4}

budget.

Quantity	Count
Total registered claims	99
Testable claims	96
Testable claims met	95
Testable claims unmet	1 (erratum)
Explicitly out of scope	3
Declared verification checks	148

Table 14: GBI-DCSE v3 claim coverage.

Figure 4: Claim coverage generated from the v3 claim register. The presence of explicit OUT OF SCOPE and ERRATUM classes is part of the evaluation design, not an afterthought.

Resource	Sparse path	Dense path	Declared budget
Floating-point operations	8,440	124,416,000	5,000,000
Heap bytes	13,440	921,600	262,144
Syscalls	2	not the enclave path	64

Table 15: Sparse versus dense verification accounting in the v3 synthetic enclave experiment.

Measure	Result
Severe contradiction sensitivity	265/265 = 1.000
Severe contradictions missed	0
False conflicts over fully clean records	0/175 = 0.000
Receipt chain	valid
Ledger	valid and non-equivocating
Forced-bad-entry atomicity	held

Table 16: Sensitive-infrastructure synthetic triage result.


Stage	Main question	Positive evidence	What it does not establish
v0.1	Will a frozen model output cross a strict contract?	768 executions all fail closed at parse/schema.	Selective utility, task difficulty, policy quality, general model safety.
v0.2	Can benchmark difficulty be tuned without confusing interface failure with task failure?	Degenerate objective detected at zero admission; after repair, feedback search reaches 2.87% mean held-out target gap.	LLM-designer performance, commercial-model difficulty, full-space optimality.
v2	Can the GBI gate selectively admit clean work and refuse declared severe contradictions without answer-key leakage?	116/116 severe injections caught; 0/99 narrow clean false conflicts; zero silent promotions under two synthetic adversaries; policy ablations fail.	Real clinical safety, complete taxonomy, adversarial robustness to arbitrary attacks.
v3	Do the broader testable manuscript claims have executable evidence?	95/96 testable claim criteria met; 148 declared checks; systems modules, receipts, rollback and portability exercised.	Real TEE/BFT/FHIR/ZK deployment, real data, operational accreditation.

Table 17: Evaluation progression and what each stage licenses.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Claim	Why out of scope	What is established instead
C-9.16	No zero-knowledge proof system is present.	Finite certificate predicate, public-input binding, and a blinded binding commitment.

C-B1.7	Retrospective clinical playback requires a preregistered cohort and expert adjudication.	Receipt-driven replay reproduces 14/14 synthetic decisions.

C-B2.4	Attestation bootstrapping target requires real TEE quote generation and an attestation-service handshake.	Software verification path is measured only as a proxy and is not promoted to the hardware target.

Appendix

Table 21

Explore similar work

Apr 2, 2026

What Do Claim Verification Datasets Actually Test? A Reasoning Trace Analysis

Despite rapid progress in claim verification, we lack a systematic understanding of what reasoning these benchmarks actually exercise. We generate structured reasoning traces for 24K claim-verification examples across 9 datasets using GPT-4o-mini and find that direct evidence extraction dominates, while multi-sentence synthesis and numerical reasoning are severely under-represented. A dataset-level breakdown reveals stark biases: some datasets almost exclusively test lexical matching, while others require information synthesis in roughly half of cases. Using a compact 1B-parameter reasoning verifier, we further characterize five error types and show that error profiles vary dramatically by domain -- general-domain verification is dominated by lexical overlap bias, scientific verification by overcautiousness, and mathematical verification by arithmetic reasoning failures. Our findings suggest that high benchmark scores primarily reflect retrieval-plus-entailment ability. We outline recommendations for building more challenging evaluation suites that better test the reasoning capabilities verification systems need.

Delip Rao, Chris Callison-Burch

University of Pennsylvania, Philadelphia, PA, USA

Claim Verification LLM Evaluation Scientific Claim Verification

Ask PDF

May 10, 2026

An Executable Benchmarking Suite for Tool-Using Agents

Closed-loop tool-using agents are increasingly evaluated in executable web, code, and micro-task environments, but benchmark reports often conflate workloads, action-generating drivers, and the evidence admitted for systems-facing claims. We present an executable benchmarking suite that makes these objects explicit under a shared evidence-admission contract. The suite connects WebArena Verified, a SWE-Gym slice with SWE-bench-compatible verification, and MiniWoB++ through common workload adapters, task manifests, event schemas, replay/freeze policy, declared drivers, and reporting pipelines. In the canonical release, the gate separates paper-facing evidence from preflight, fixture, smoke, and diagnostic rows while preserving non-admitted artifacts for audit and onboarding. The admitted evidence records latency, invalid-action behavior, patch-generation cost, verifier metadata, replay bindings, and provenance under one auditable contract. The gate is decision-relevant rather than merely clerical: in a separate WebArena Verified controller study, clean-baseline and medium live-stressed evaluation select different fixed controller variants under the same workload and admission contract. The release is scoped as a benchmarking suite and admitted evidence, not a new agent policy, model leaderboard, backend comparison, or autonomous SWE-bench solver.

Zhiqing Zhong, Zhijing Ye, Jiamin Wang +1

Stevens Institute of Technology

Computer-Use Agent Benchmarks Tool-Use Evaluation Benchmark Design Web Agent Benchmarks Software Engineering Benchmarks AI Agent Benchmarks

Ask PDF

Oct 13, 2026

Gaussian Process Bandits for AI System Optimization with Selectively Verified Feedback

Gaussian process bandits exploit similarities among configurations to optimize prompts, retrieval systems, and agent workflows. In these applications, however, inexpensive model-based evaluations can disagree with trusted task outcomes. We study selective verification when an action is chosen before a diagnostic is observed and trusted feedback is informative on an unknown set of diagnostic states. A finite reliability class and a finite RKHS signal dictionary describe these two sources of uncertainty. We construct a fixed audit design that combines reliability coverage with reward separation and establish a finite-time regret bound that accounts for a hard audit budget and the rounds needed to obtain informative observations. A safe adaptive extension mixes this robust design with predictable Chernoff allocations while preserving a uniform identification floor and exact expected acquisition-cost accounting. For signed-coordinate kernels, structured and diffuse reliability classes require different audit scales despite sharing the same reward geometry. Synthetic experiments distinguish these certified designs from an adaptive posterior heuristic and GP controls. Safe adaptive allocation reduces aggregate regret relative to the fixed design under the exact dictionary, but its finite-budget error certificate is numerically loose. Conditional-feedback errors can remove the heuristic's advantage and target perturbations can reverse it. Separate AI-task replays assess feedback correction and fitted-dictionary policies without establishing end-to-end validation of a learned selective-verification method.

Shuang Wu

UCLA

Multi-Armed Bandits Robust Multi-Armed Bandits Algorithmic Auditing

Ask PDF