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

What Do Claim Verification Datasets Actually Test? A Reasoning Trace Analysis
Apr 2, 2026Delip Rao, Chris Callison-BurchClaim Verification LLM Evaluation
University of Pennsylvania, Philadelphia, PA, USA
An Executable Benchmarking Suite for Tool-Using Agents
May 10, 2026Zhiqing Zhong, Zhijing Ye, Jiamin Wang +1Computer-Use Agent Benchmarks Tool-Use Evaluation
Stevens Institute of Technology
Gaussian Process Bandits for AI System Optimization with Selectively Verified Feedback
Oct 13, 2026Shuang WuMulti-Armed Bandits Robust Multi-Armed Bandits
UCLA

Apr 2, 2026J/K move · Enter open · S save

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

Delip Rao, Chris Callison-Burch

University of Pennsylvania, Philadelphia, PA, USA

Claim Verification LLM Evaluation Scientific Claim Verification

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

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

An Executable Benchmarking Suite for Tool-Using Agents

Gaussian Process Bandits for AI System Optimization with Selectively Verified Feedback