Local approximation schemes for shared circuits #
A local approximation scheme supplies an approximate interpretation of every gate and a finite exception set on which that local replacement may be incorrect. Folding the scheme over a straight-line program unions the local exception sets. Consequently each gate is charged once, even when its value fans out to many later gates.
This is deliberately independent of polynomials, probability, and any particular circuit basis. The monotone CLIQUE application uses bounded-width DNF approximators and two different sample families with the same approximate interpretation.
structure
Algebraic.Approximation.Scheme
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
(exactInterpretation : Interpretation σ U)
(approxInterpretation : Interpretation σ A)
(decode : A → Sample → U)
(exactInput : Sample → Fin n → U)
(approxInput : Fin n → A)
[DecidableEq Sample]
:
Type (max (max (max u_1 u_2) u_3) u_4)
A locally sound approximate interpretation on a finite sample space.
- relation : U → U → Prop
One-sided correctness relation from exact to approximate values.
- relation_trans {left middle right : U} : self.relation left middle → self.relation middle right → self.relation left right
Local and inherited correctness compose.
- interpretation_preserves (op : σ.Op) (exactArguments approxArguments : Fin (σ.Arity op) → U) : (∀ (input : Fin (σ.Arity op)), self.relation (exactArguments input) (approxArguments input)) → self.relation (exactInterpretation op exactArguments) (exactInterpretation op approxArguments)
Exact operations preserve the correctness relation pointwise.
- errorCost : OperationCost σ
Maximum number of fresh exceptions charged to an operation.
Fresh exceptions for one concrete approximate gate application.
- input_correct (sample : Sample) (input : Fin n) : self.relation (exactInput sample input) (decode (approxInput input) sample)
Approximate inputs are exact on every sample.
- gate_correct (op : σ.Op) (arguments : Fin (σ.Arity op) → A) (sample : Sample) : sample ∉ self.exceptions op arguments → self.relation (exactInterpretation op fun (input : Fin (σ.Arity op)) => decode (arguments input) sample) (decode (approxInterpretation op arguments) sample)
A local gate is exact away from its fresh exceptions.
- exceptions_card_le (op : σ.Op) (arguments : Fin (σ.Arity op) → A) : (self.exceptions op arguments).card ≤ self.errorCost op
Each fresh exception set respects its advertised operation cost.
Instances For
def
Algebraic.Approximation.Scheme.lineArguments
{σ : Signature}
{A : Type u_2}
{n g : ℕ}
(program : Program σ n g)
(line : Line σ n g)
(approxInterpretation : Interpretation σ A)
(approxInput : Fin n → A)
:
The approximate argument tuple supplied to the next line.
Equations
- Algebraic.Approximation.Scheme.lineArguments program line approxInterpretation approxInput = program.trace approxInterpretation approxInput ∘ line.wires
Instances For
def
Algebraic.Approximation.Scheme.programExceptions
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
{g : ℕ}
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
(program : Program σ n g)
:
Finset Sample
The union of all local exception sets created by a program.
Equations
- One or more equations did not get rendered due to their size.
- scheme.programExceptions Cslib.Circuits.Program.empty = ∅
Instances For
@[simp]
theorem
Algebraic.Approximation.Scheme.programExceptions_empty
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
:
@[simp]
theorem
Algebraic.Approximation.Scheme.programExceptions_gate
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
{g : ℕ}
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
(program : Program σ n g)
(line : Line σ n g)
:
scheme.programExceptions (program.gate line) = scheme.programExceptions program ∪ scheme.exceptions line.op (lineArguments program line approxInterpretation approxInput)
theorem
Algebraic.Approximation.Scheme.programExceptions_card_le_cost
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
{g : ℕ}
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
(program : Program σ n g)
:
The global exception set is bounded by the sum of local gate budgets.
theorem
Algebraic.Approximation.Scheme.program_correct
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
{g : ℕ}
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
(program : Program σ n g)
(sample : Sample)
(fresh : sample ∉ scheme.programExceptions program)
(wire : Wire n g)
:
Every approximate wire agrees with its exact sampled value away from the single global exception set.
theorem
Algebraic.Approximation.Scheme.circuit_correct
{σ : Signature}
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_4}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
{m : ℕ}
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
(circuit : Circuit σ n m)
(output : Fin m)
(sample : Sample)
(fresh : sample ∉ scheme.programExceptions circuit.program)
:
A circuit output is correct on every sample outside the union of its local exceptions.
def
Algebraic.Approximation.Scheme.failures
{U : Type u_1}
{A : Type u_2}
{Sample : Type u_3}
[Fintype Sample]
(relation : U → U → Prop)
[DecidableRel relation]
(decode : A → Sample → U)
(value : A)
(target : Sample → U)
:
Finset Sample
Samples on which one approximate value violates a one-sided correctness relation with a target.
Equations
- Algebraic.Approximation.Scheme.failures relation decode value target = {sample : Sample | ¬relation (target sample) (decode value sample)}
Instances For
@[simp]
theorem
Algebraic.Approximation.Scheme.mem_failures
{U : Type u_2}
{A : Type u_3}
{Sample : Type u_1}
[Fintype Sample]
(relation : U → U → Prop)
[DecidableRel relation]
(decode : A → Sample → U)
(value : A)
(target : Sample → U)
(sample : Sample)
:
theorem
Algebraic.Approximation.Scheme.failures_subset_programExceptions
{σ : Signature}
{U : Type u_3}
{A : Type u_4}
{Sample : Type u_1}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
[Fintype Sample]
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
[DecidableRel scheme.relation]
(circuit : Circuit σ n 1)
(target : Sample → U)
(computes : ∀ (sample : Sample), circuit.eval exactInterpretation (exactInput sample) 0 = target sample)
:
failures scheme.relation decode (circuit.eval approxInterpretation approxInput 0) target ⊆
scheme.programExceptions circuit.program
The failure set of a correctly computed target is contained in the scheme's global exception set.
theorem
Algebraic.Approximation.Scheme.failures_card_le_cost
{σ : Signature}
{U : Type u_3}
{A : Type u_4}
{Sample : Type u_1}
{n : ℕ}
{exactInterpretation : Interpretation σ U}
{approxInterpretation : Interpretation σ A}
{decode : A → Sample → U}
{exactInput : Sample → Fin n → U}
{approxInput : Fin n → A}
[DecidableEq Sample]
[Fintype Sample]
(scheme : Scheme exactInterpretation approxInterpretation decode exactInput approxInput)
[DecidableRel scheme.relation]
(circuit : Circuit σ n 1)
(target : Sample → U)
(computes : ∀ (sample : Sample), circuit.eval exactInterpretation (exactInput sample) 0 = target sample)
:
Total sampled failure is at most the sum of local approximation errors, with sharing charged once.