Graph
Represent assumptions, evidence, lemmas and conclusions as an explicit dependency graph.
Mathematical assurance for AI systems
The verification layer for AI-generated reasoning.
GERO converts mathematical and technical answers into claim graphs, routes each claim to a bounded checker, attacks fragile steps and returns a decision that never exceeds the evidence behind it.
8verifier modules
4bounded statuses
0verified claims without a certificate
01
ASSUMPTIONDomain is finite
VERIFIED
02
LEMMA∀x ∃y : y = x
VERIFIED
03
CONCLUSIONQuantifiers reversed
CONTRADICTED
REPLAYABLE CERTIFICATE
counterexample: x=1, y=0
sha256: 92b8…e41c
Language models are optimized to produce plausible continuations.
Research systems need reproducible reasons to accept a claim.
GERO separates generation from verification.
The name
GERO means
Graph Evaluation &
Reliability Orchestrator.
A system that organizes independent checks around an AI-generated claim and prevents the final verdict from becoming stronger than its evidence.
Evaluation
Route each necessary claim to a bounded mathematical, executable or expert check.
Reliability
Measure contradictions, missing evidence and residual uncertainty instead of trusting fluency.
Orchestrator
Coordinate models, deterministic tools and human escalation into one replayable decision process.
The assurance pipeline
LLMs generate.
GERO verifies.
Agreement between two models is not independent evidence. GERO moves critical steps into explicit, inspectable checks with named limits.
Compile the claim
Turn prose into assumptions, lemmas, conclusions and declared evidence requirements.
Build the dependency graph
Expose missing premises, circular reasoning and the first step on which a conclusion depends.
Route to real checks
Use exact arithmetic, intervals, units, finite model checks and adapters for symbolic or formal tools.
Return a bounded verdict
Verified, conditional, contradicted or insufficient — with a replayable certificate and explicit scope.
Browser-side deterministic demo
Try to break the reasoning.
Choose a controlled claim, edit its JSON and run the audit. This demo executes a narrow checker in your browser; it does not ask an LLM to judge another LLM.
Only the displayed, restricted JSON contract is evaluated.
GERO AUDIT RESULT
READY
STATUS
AWAITING CLAIM
Run a controlled example to generate a bounded verdict.
CERTIFICATE
{
"scope": "not evaluated",
"replayable": false
}
Boundary: the live demo verifies only its documented finite and arithmetic contracts. It does not certify unrestricted natural-language proofs.
The uncertainty contract
“I don’t know” becomes an engineering result.
The required bounded check completed and produced a certificate.
The claim holds only under assumptions named in the output.
A reproducible mismatch or counterexample was found.
The available checker cannot support the strength of the claim.
Research direction
From a product runtime to a science of reliable reasoning.
AUTODIFF
Same Inputs, Wrong Weights: MLX logcumsumexp Gradients at Large Offsets
Large equal inputs receive gradient [1,1] instead of [0.5,0.5]. Isolated CPU study and research prototype.
Read the case study →AUTODIFF
Missing Curvature: MLX logcumsumexp at a Zero Incoming Gradient
A smooth singleton loses its second derivative. Research C++ prototype: 186 scenarios and 477 checks pass.
Read the case study →AUTODIFF
Zero Mask, Missing Gradient: MLX block_masked_mm
An extra output mask suppresses its own gradient at zero. Local CPU repair: 377 scenarios and 604 checks pass.
Read the case study →AUTODIFF
A Missing Transpose in MLX Quantized Gradients
A missing orientation step miscomputes scale and bias gradients. Local CPU repair: 205 scenarios and 379 checks pass.
Read the case study →AUTODIFF
Sorted Indices, Wrong Gradients: MLX Gather
Sorted gather calls produce incorrect gradients. Bounded FP32 CPU repair: 69 scenarios and 626 checks pass.
Read the case study →AUTODIFF
Orthogonal Is Not Symmetric: MLX Hadamard Gradients
A nonsymmetric transform needs its transpose in backward. Local patch: 64 scenarios and 624 checks pass.
Read the case study →AUTODIFF
A Constant, a Polynomial, a NaN: MLX power Derivatives at Zero
A smooth polynomial receives a NaN gradient. A local C++ patch passes 41 scenarios and 396 checks.
Read the case study →AUTODIFF
An Unused Value Gets a Gradient: MLX Masked Assignment
An unused input gets gradient 20 instead of 0. The local C++ patch passes 19 scenarios and 255 checks.
Read the case study →AUTODIFF
A Missing Gradient in MLX Block Updates
A strict block update loses a winning gradient. Minimal C++ patch passes 26 targeted checks; historical ties treated separately.
Read the case study →LAYERNORM
When Cosine and LayerNorm Break Their Contracts
Two reproduced implementation reports with tested local patches and exact evidence.
Read the technical note →ATTENTION
When Causal Attention Sees the Future
Future values affect earlier outputs. A native reproduction, tested repair and upstream report.
Read the technical note →GRADIENTS
When Dropout Sends Two Gradients to One Input
Correct forward values, wrong gradient destinations. Native reproduction and 19 passing tests after a local patch.
Read the case study →GRADIENTS
Finite Loss, Wrong Gradient: Gaussian NLL in MLX
Finite loss, wrong derivative sign. Native CPU reproduction, regression tests and the limits of a mitigation.
Read the case study →MUON
Same Gradients, Half the Step: MLX Muon and Convolution Shapes
Equivalent weights, different optimizer steps. Native reproduction, a minimal patch and 31 focused checks.
Read the case study →AUTODIFF
A Real Loss, a Reversed Gradient: Complex Autodiff in MLX
A real loss increases after an update. Two derivative mechanisms, a C++ patch and 131 passing local scenarios.
Read the case study →AUTODIFF
A Smooth Polynomial, a NaN Hessian: MLX cumprod at Zero
A smooth polynomial, NaN second derivatives and a division-free prototype. 57 local scenarios pass; performance costs explicit.
Read the case study →Semantic compilation
Did the verifier formalize the claim the model actually made?
Correlated failure
When do generator and critic repeat the same structural mistake?
Risk–coverage calibration
When should an AI system answer, qualify or abstain?
Mechanistic evidence
Can internal model signals predict a fragile reasoning trajectory before release?
Pilot with your own reasoning traces
Five non-confidential paths.
Seven days. One reproducible defect map.
For AI research teams, evaluation engineers and builders of mathematical, scientific or technical agents.
Discuss a seven-day pilotGERO service demonstration
Check the rules behind financial calculations.
A public Fineract example shows how written rules become executable checks, documented mismatches and scoped corrections.