[EM] Exact spatial model probabilities?

[Kristofer Munsterhjelm]

On 26.01.2022 04:23, Forest Simmons wrote:

> The dirac delta is the convolution identity distribution ... convolving
> it with another distribution leaves it unchanged with cliffs and sharp
> corners intact. 
> 
> But if you convolve with a smooth approximation of Dirac,  like a
> gaussian with tiny variance, you get an infinitely differentiable
> approximation of the "horrible" function.

Right. I once wrote a fully differentiable genetic algorithm (I was
intending to use it for hyperparameter tuning). There were two problems.
First, local optima. Second, suppose that you have a plain statement like:

if (x>y) {
	return z;
} else {
	return f(z);
}

When smoothing, this turns into something like

return z * sig(x-y, k) + f(z) * sig(y-x, k)

where sig(x, k) is a sigmoid function that returns 1 if x>>0, 0 if x<<0,
and k is a steepness parameter controlling sig'(x) around 0.

If k is too high, then gradient descent fails because there's no
noticeable slope down to the optimum; it's flat almost everywhere and
then goes to zero exactly at the optimum (vanishing gradient problem).

So we need some smoothness, which means that both branch values come
into play. But this makes the function slow to evaluate as the program
must "go both ways" on every conditional.

> Electrical engineers have a vast library of standard test patterns to
> use as input signals for use in designing and testing circuits.
> 
> We need a similar library of test distributions for use in designing and
> testing election methods.
> 
> Election methods could even be profiled by their responses to these test
> patterns.

This, I do agree with. There have been a lot of voting method proposals
lately, and we need some way to easily determine:

- what is its VSE (under what models)
- what is its voter-strategy susceptibility
- what is its candidate-strategy susceptibility (cloning)
- what criteria does it definitely fail

and it would be nice to also know what criteria it definitely passes,
though that requires formal verification, which is much harder than just
testing a bunch of cases.

(I remember using REDLOG to come up with BTV once, but I don't remember
the details. Perhaps I should look into the current state of the art for
provers, like Z3... so many things to do and so little time in which to
do them!)

-km