Repository navigation
How APORIA Works
APORIA treats analysis as a budgeted experiment over a model's declared input domain. An execution produces records. Those records support several kinds of evidence, which are calibrated and combined before the Atlas labels regions and the campaign chooses what to evaluate next.
The shipped command reads Aporia DSL source, type-checks its expressions and units, lowers it to A-IR, and verifies that representation before starting the campaign. Invalid source or an invalid A-IR model does not enter the search. See Aporia DSL.
The campaign maps points into declared parameter domains and calls an Executor. The default executor is the scalar interpreter. A run may also buy extra evaluations for perturbations, declared symmetry swaps, lower-precision comparisons, or reference comparisons, subject to configuration and executor capabilities. These extra executions consume the same evaluation budget.
Every execution records outputs and, when produced, traces, flags, and instruction steps. The batch evaluator can produce lane-major records. The analysis associates evidence with observation IDs so the later fusion step can tell when different channels are describing the same executions.
Properties analysis checks require constraints and check relations, detects non-finite outputs, looks for supported patterns in observed outputs, evaluates sensitivity from perturbation probes, and compares numerical paths when available. These signals form the five channels described in Evidence Model.
Raw magnitudes have different units and scales. APORIA fits robust reference scales from the campaign's own measurements, with per-claim scales when enough samples exist. It assigns strengths, estimates channel correlations, and fuses the strongest channel signals with discounts for shared observations and measured correlation. Strengths and fused risks are ranking values, not probabilities.
The Atlas partitions the declared domain into axis-aligned cells. Search-time evidence guides the campaign, and the finished evidence set is applied back to the cells before final labeling. Each cell becomes TRUSTED, SUSPICIOUS, or UNKNOWN under the recorded policy. See Trust Atlas.
The labels are deliberately cautious. A cell with too little sampling remains unknown. Suspicion based on measured channels requires corroboration from multiple channels at an evaluation; an absolute fact such as a violated declared rule or divergence can qualify on its own. Trust means no evidence appeared under the current experiment and policy; it is not a proof of correctness.
Random and stratified campaigns provide baselines. Adaptive campaigns select among coverage, boundary, uncertainty, sensitivity, and contradiction acquisition families using a UCB-style meta-policy with random exploration. The choice is credited with observed information gain per evaluation. See Adaptive Search.
The CLI prints an Atlas summary and up to three findings with the loudest evidence. It does not write an archive or run minimisation. The benchmark harness records its runs, validates the declared benchmark truth before measurement, and replays the largest-budget archived run before reporting. The library contains a separate minimiser and archive tools. See Counterexample Minimisation and Archives and Replay.