Repository navigation
Counterexample Minimisation
Minimisation asks whether a smaller parameter description still preserves a stated failure predicate. It is implemented in aporia-minimize as a library component and is used by the benchmark harness for findings. The shipped aporia run CLI does not invoke it.
The current reducer works on a case consisting of parameter ranges and representative values. It tries to simplify the case in stages:
- ddmin over parameters: remove parameter dimensions and re-check whether the predicate still holds.
- Per-axis interval narrowing: use interval bisection to reduce the range on each retained axis while preserving the predicate.
- Significant-digit reduction: simplify representative values and verify each accepted reduction.
Candidates are accepted only after the selected oracle re-evaluates them. The result records the reduced case and the evaluations spent on verification. The returned case is a verified smaller description under the chosen predicate and budget; it is not a proof of global minimality.
The rule oracle asks whether a declared rule or divergence still fails. It is the direct witness of a model-level contract violation. A second risk oracle was added for findings produced by the campaign's measurement channels even when no declared rule failed.
The risk oracle freezes the report's calibrator, channel correlations, median sensitivity reference, and risk threshold. It uses point-measurable physical, sensitivity, numerical, and differential evidence. It deliberately excludes the behavioral channel: relations such as monotonicity and symmetry are judged across a set of records, and rebuilding such a relation from a single candidate could make a stronger claim than the report itself. The risk oracle is only used after the rule oracle fails and after its score reproduces the finding's representative score.
The two predicates answer different questions. A rule-preserving reduction shows that a declared contract still fails at the reduced case. A risk-preserving reduction shows that the evidence model would still flag the case under frozen campaign references. The harness records which oracle was used.
In the current benchmark measurement, all 341 reported minimisation rows were verified under their recorded oracle. The benchmark notes also state that 100% verified does not mean every row dropped a parameter: 15 of the 54 rows attributed to the risk oracle remove a parameter, while the others reduce span or significant digits. Every attempted change is checked; the initial flagged case is not returned as a successful minimisation.
See Experiments & Results for the source measurement and Archives and Replay for the records that preserve benchmark outputs.