Experimental Comparison of Proof Rules for Checking Differential Invariance of Algebraic Sets

We compare all the proof rules experimentally on a heterogeneous collection of 76 invariant varieties of algebraic differential equations.

1. Isolated equilibria as a trivial (for humans not machines) equational invariants
2. Singularities
3. Regular (smooth) varieties, where Lie is both necessary (and sufficient)
4. Functional invariants, where DI= is necessary (and sufficient)

The dimension of the vector field is given under Dim in the tables below. Also shown are the polynomial degree of the invariant candidate d.Inv and the degree of the vector field d.VF defined as the maximum degree of all the polynomials of the vector field. True means that the proof rule was able to prove the invariance of the candidate, otherwise it prints ┴ (except for DRI which prints False as it is necessary and sufficient). The time out is set to 60s per rule per problem. The benchmarks of different classes are available below. Time is given in second.

Figures compare the number of invariant varieties which each rule could prove within 60 seconds. The vertical axis shows cumulative time spent on the problems (log scale).

1. Isolated Equilibria

	Prob.	Dim	d.Inv	d.VF	DI	P-c	SFLie
	1	2	18	17	0.009 True	0.005 True	0.019 ⊥	0.037 True	0.204 True	0.007 True
	2	1	1	1	⊥	True	True	True	True	True
	3	1	2	3	⊥	True	True	True	0.001 True	True
	4	1	2	3	⊥	0.001 ⊥	0.002 True	0.002 True	0.006 True	0.003 True
	5	2	2	2	0.004 ⊥	0.002 True	0.004 ⊥	0.005 True	0.006 True	0.002 True
	6	2	46	4	34.470 ⊥	0.016 ⊥	Timeout	Timeout	Timeout	0.451 True
	7	3	2	243	Timeout	0.057 ⊥	0.023 ⊥	14.260 True	14.180 True	Timeout
	8	2	128	5	0.429 ⊥	0.050 ⊥	0.004 ⊥	0.012 True	0.013 True	Timeout
	9	3	2	2	0.009 ⊥	0.002 ⊥	0.018 ⊥	0.016 True	0.026 True	0.062 True
	10	3	25	2	Timeout	0.007 ⊥	Timeout	Timeout	Timeout	Timeout
	11	3	2	90	Timeout	0.068 ⊥	0.032 ⊥	1.153 True	1.082 True	3.233 True
	12	4	2	4	0.717 ⊥	0.003 ⊥	0.014 ⊥	3.084 True	2.940 True	Timeout
	13	4	2	2	0.030 ⊥	0.005 ⊥	0.020 ⊥	0.019 True	0.035 True	0.021 True
	14	4	2	2	0.002 ⊥	0.002 ⊥	0.019 ⊥	0.023 True	0.027 True	Timeout
	15	5	2	6	0.204 ⊥	0.007 ⊥	0.016 ⊥	8.739 True	8.674 True	Timeout
	16	5	12	3	0.757 ⊥	0.013 ⊥	Timeout	Timeout	Timeout	Timeout
	17	5	2	35	Timeout	1.754 ⊥	0.026 ⊥	Timeout	Timeout	Timeout

2. Singularities

	Prob.	Dim	d.Inv	d.VF	DI	P-c	SFLie
	1	2	6	2	0.013 ⊥	0.005 ⊥	0.023 ⊥	0.029 True	0.438 True	0.054 True
	2	2	4	3	0.006 ⊥	0.004 True	0.009 ⊥	0.014 True	0.022 True	0.003 True
	3	3	6	10	0.016 ⊥	0.006 ⊥	0.081 ⊥	0.081 True	Timeout	Timeout
	4	3	4	3	0.010 ⊥	0.007 ⊥	0.067 ⊥	0.072 ⊥	0.468 ⊥	0.049 True
	5	3	4	3	0.004 ⊥	0.003 ⊥	0.015 ⊥	0.017 ⊥	0.043 ⊥	0.026 True
	6	3	4	1	0.004 ⊥	0.002 ⊥	0.016 ⊥	0.017 ⊥	0.025 ⊥	0.092 True
	7	7	14	1	0.003 ⊥	0.002 True	0.007 ⊥	0.007 ⊥	0.007 True	0.002 True
	8	2	4	2	0.005 ⊥	0.003 True	0.007 ⊥	0.011 True	0.037 True	0.004 True
	9	2	4	2	0.013 ⊥	0.003 True	0.015 ⊥	0.030 ⊥	0.056 True	0.007 True
	10	3	4	3	0.005 ⊥	0.004 ⊥	0.031 ⊥	0.033 ⊥	0.055 ⊥	0.034 True
	11	3	6	2	0.001 ⊥	0.001 ⊥	0.017 ⊥	0.030 ⊥	0.049 ⊥	0.010 True
	12	5	6	2	0.003 ⊥	0.002 ⊥	0.080 ⊥	0.168 ⊥	Timeout	0.058 True
	13	9	18	8	0.013 ⊥	0.023 ⊥	Timeout	Timeout	Timeout	Timeout
	14	5	4	4	0.096 ⊥	0.020 ⊥	0.071 ⊥	0.228 ⊥	Timeout	Timeout
	15	9	10	4	0.009 ⊥	0.010 ⊥	0.708 ⊥	0.511 ⊥	Timeout	0.235 True
	16	3	4	3	0.006 ⊥	0.003 ⊥	0.020 ⊥	0.027 ⊥	0.050 ⊥	0.100 True
	17	6	2	2	0.001 True	True	0.005 ⊥	0.014 True	0.014 True	0.002 True

3. Regular (Smooth) Varieties

	Prob.	Dim	d.Inv	d.VF	DI	P-c	SFLie
	1	1	5	1	0.001 ⊥	0.001 ⊥	0.002 True	0.002 True	0.004 True	0.005 True
	2	1	21	1	0.002 ⊥	0.003 ⊥	0.001 True	0.001 True	0.003 True	0.035 True
	3	2	6	1	0.003 ⊥	0.002 ⊥	0.004 True	0.005 True	0.008 True	0.023 True
	4	2	22	1	0.006 ⊥	0.006 ⊥	0.004 True	0.005 True	0.007 True	0.419 True
	5	4	14	1	0.093 ⊥	0.074 ⊥	0.062 True	0.128 True	0.169 True	Timeout
	6	4	32	1	0.725 ⊥	0.985 ⊥	0.062 True	0.137 True	0.190 True	Timeout
	7	2	2	1	⊥	True	True	True	True	0.002 True
	8	2	2	1	True	True	0.002 True	0.002 True	0.002 True	True
	9	3	1	1	True	True	True	True	True	True
	10	2	1	5	0.002 ⊥	True	0.002 True	0.002 True	0.002 True	0.001 True
	11	2	2	3	0.002 ⊥	0.002 True	0.004 True	0.006 True	0.008 True	0.002 True
	12	2	6	5	True	True	0.006 True	0.006 True	0.023 True	0.002 True
	13	3	2	4	0.026 ⊥	0.003 True	0.008 True	0.012 True	0.024 True	0.004 True
	14	4	2	4	0.079 ⊥	0.006 True	0.013 True	0.019 True	0.036 True	0.009 True
	15	5	2	4	0.669 ⊥	0.007 True	0.020 True	0.031 True	0.056 True	0.008 True
	16	3	2	3	True	True	True	True	True	0.001 True
	17	3	2	3	0.002 ⊥	True	0.003 True	0.004 True	0.008 True	0.002 True
	18	2	4	2	0.005 ⊥	0.002 True	0.005 True	0.006 True	0.016 True	0.003 True
	19	2	2	2	⊥	True	0.002 True	0.002 True	0.004 True	0.001 True
	20	2	1	3	⊥	True	0.001 True	0.001 True	0.001 True	True
	21	2	1	2	0.002 ⊥	True	0.002 True	0.002 True	0.002 True	0.001 True
	22	2	1	2	0.001 ⊥	True	0.001 True	0.002 True	0.002 True	0.001 True
	23	2	1	2	⊥	True	0.001 True	0.001 True	0.001 True	True
	24	6	2	2	True	True	0.002 True	0.005 True	0.007 True	0.002 True

4. Functional Invariants (First Integrals)

	Prob.	Dim	d.Inv	d.VF	DI	P-c	SFLie
	1	2	3	2	True	True	0.004 ⊥	0.002 True	0.007 True	0.001 True
	2	2	6	5	True	True	0.007 ⊥	0.007 True	2.350 True	0.002 True
	3	2	6	5	0.002 True	0.001 True	0.008 ⊥	0.009 True	0.030 True	0.002 True
	4	2	4	1	True	True	0.014 ⊥	0.014 ⊥	0.026 ⊥	0.003 True
	5	4	3	2	True	True	0.009 ⊥	0.006 True	0.031 True	0.003 True
	6	3	6	10	0.002 True	0.002 True	0.028 ⊥	0.021 True	Timeout	0.005 True
	7	4	2	1	0.001 True	True	0.001 True	0.002 True	0.002 True	0.002 True
	8	4	12	11	True	True	0.010 ⊥	0.006 True	0.025 True	0.003 True
	9	8	12	11	0.005 True	0.003 True	0.007 True	0.011 True	0.011 True	0.007 True
	10	8	9	8	0.003 True	0.003 True	Timeout	0.069 True	Timeout	0.011 True
	11	8	75	74	True	0.192 True	Timeout	Timeout	Timeout	3.498 True
	12	8	31	30	True	0.006 True	12.710 ⊥	Timeout	Timeout	0.091 True
	13	8	29	28	True	0.003 True	7.917 ⊥	8.896 True	Timeout	0.025 True
	14	8	18	17	0.032 True	0.029 True	1.463 ⊥	0.857 True	Timeout	0.045 True
	15	8	5	4	True	True	Timeout	0.029 True	0.362 True	0.003 True
	16	8	16	15	True	0.035 True	20.980 True	27.560 True	Timeout	0.180 True
	17	3	2	1	True	True	0.001 ⊥	0.001 True	0.002 True	True
	18	7	6	1	True	True	0.006 ⊥	0.006 ⊥	0.005 True	0.001 True

5. All Examples

	Prob.	Dim	d.Inv	d.VF	DI	P-c	SFLie
	1	2	18	17	0.004 True	0.004 True	0.015 ⊥	0.041 True	0.179 True	0.007 True
	2	1	1	1	⊥	True	True	True	True	True
	3	1	2	3	⊥	True	True	True	True	True
	4	1	2	3	⊥	0.001 ⊥	0.002 True	0.002 True	0.006 True	0.003 True
	5	2	2	2	0.003 ⊥	0.001 True	0.006 ⊥	0.008 True	0.007 True	0.002 True
	6	2	46	4	30.330 ⊥	0.018 ⊥	59.620 ⊥	59.790 True	58.570 True	0.356 True
	7	3	2	243	Timeout	0.060 ⊥	0.025 ⊥	12.430 True	12.270 True	Timeout
	8	2	128	5	0.362 ⊥	0.053 ⊥	0.003 ⊥	0.008 True	0.010 True	Timeout
	9	3	2	2	0.008 ⊥	0.002 ⊥	0.018 ⊥	0.018 True	0.025 True	0.060 True
	10	3	25	2	Timeout	0.007 ⊥	Timeout	Timeout	Timeout	Timeout
	11	3	2	90	Timeout	0.065 ⊥	0.034 ⊥	0.737 True	0.790 True	2.816 True
	12	4	2	4	0.674 ⊥	0.003 ⊥	0.009 ⊥	2.682 True	2.695 True	Timeout
	13	4	2	2	0.027 ⊥	0.003 ⊥	0.023 ⊥	0.018 True	0.025 True	0.026 True
	14	4	2	2	0.001 ⊥	0.002 ⊥	0.020 ⊥	0.024 True	0.024 True	Timeout
	15	5	2	6	0.172 ⊥	0.004 ⊥	0.015 ⊥	8.578 True	8.242 True	Timeout
	16	5	12	3	0.753 ⊥	0.010 ⊥	Timeout	Timeout	Timeout	Timeout
	17	5	2	35	Timeout	1.706 ⊥	0.032 ⊥	Timeout	Timeout	Timeout
	18	1	5	1	0.001 ⊥	0.001 ⊥	0.002 True	0.003 True	0.004 True	0.005 True
	19	1	21	1	0.002 ⊥	0.003 ⊥	0.001 True	0.001 True	0.003 True	0.032 True
	20	2	6	1	0.003 ⊥	0.002 ⊥	0.004 True	0.005 True	0.007 True	0.020 True
	21	2	22	1	0.006 ⊥	0.006 ⊥	0.004 True	0.005 True	0.007 True	0.433 True
	22	4	14	1	0.097 ⊥	0.085 ⊥	0.057 True	0.120 True	0.176 True	Timeout
	23	4	32	1	0.648 ⊥	0.968 ⊥	0.067 True	0.127 True	0.173 True	Timeout
	24	2	2	1	⊥	0.002 True	True	True	True	0.001 True
	25	2	2	1	True	True	0.001 True	0.001 True	0.002 True	True
	26	3	1	1	True	True	True	True	True	True
	27	2	1	5	0.002 ⊥	True	0.001 True	0.001 True	0.002 True	0.001 True
	28	2	2	3	0.004 ⊥	0.001 True	0.003 True	0.005 True	0.007 True	0.004 True
	29	2	6	5	0.002 True	0.001 True	0.008 True	0.007 True	0.029 True	0.002 True
	30	3	2	4	0.028 ⊥	0.004 True	0.011 True	0.017 True	0.017 True	0.004 True
	31	4	2	4	0.078 ⊥	0.005 True	0.012 True	0.020 True	0.030 True	0.005 True
	32	5	2	4	0.655 ⊥	0.007 True	0.021 True	0.041 True	0.057 True	0.007 True
	33	3	2	3	True	True	True	True	True	True
	34	3	2	3	0.002 ⊥	True	0.003 True	0.004 True	0.006 True	0.001 True
	35	2	4	2	0.004 ⊥	0.002 True	0.004 True	0.006 True	0.011 True	0.003 True
	36	2	2	2	⊥	True	0.002 True	0.001 True	0.004 True	0.001 True
	37	2	1	3	⊥	True	0.002 True	0.002 True	0.001 True	True
	38	2	1	2	0.002 ⊥	True	0.002 True	0.002 True	0.002 True	0.001 True
	39	2	1	2	0.001 ⊥	True	0.002 True	0.002 True	0.002 True	0.001 True
	40	2	1	2	⊥	True	0.001 True	0.001 True	0.001 True	0.001 True
	41	6	2	2	True	True	0.002 True	0.004 True	0.010 True	0.002 True
	42	2	3	2	True	True	0.004 ⊥	0.002 True	0.007 True	0.001 True
	43	2	6	5	True	True	0.007 ⊥	0.006 True	2.315 True	0.002 True
	44	2	6	5	True	True	0.007 ⊥	0.012 True	0.032 True	0.002 True
	45	2	4	1	True	True	0.013 ⊥	0.013 ⊥	0.028 ⊥	0.002 True
	46	4	3	2	True	True	0.007 ⊥	0.006 True	0.023 True	0.002 True
	47	3	6	10	0.003 True	0.003 True	0.031 ⊥	0.022 True	Timeout	0.003 True
	48	4	2	1	True	True	0.001 True	0.001 True	0.001 True	0.001 True
	49	4	12	11	True	True	0.010 ⊥	0.006 True	0.025 True	0.002 True
	50	8	12	11	0.004 True	0.003 True	0.006 True	0.006 True	0.007 True	0.006 True
	51	8	9	8	0.003 True	0.003 True	Timeout	0.065 True	Timeout	0.007 True
	52	8	75	74	True	0.166 True	Timeout	Timeout	Timeout	3.862 True
	53	8	31	30	True	0.006 True	13.910 ⊥	Timeout	Timeout	0.094 True
	54	8	29	28	True	0.003 True	8.112 ⊥	8.856 True	Timeout	0.023 True
	55	8	18	17	0.032 True	0.029 True	1.451 ⊥	0.876 True	Timeout	0.055 True
	56	8	5	4	True	0.001 True	Timeout	0.030 True	0.348 True	0.003 True
	57	8	16	15	True	0.035 True	20.280 True	28.550 True	Timeout	0.186 True
	58	3	2	1	True	True	0.001 ⊥	0.001 True	0.002 True	True
	59	7	6	1	True	True	0.009 ⊥	0.006 ⊥	0.007 True	0.001 True
	60	2	6	2	0.007 ⊥	0.003 ⊥	0.024 ⊥	0.031 True	0.452 True	0.051 True
	61	2	4	3	0.003 ⊥	0.002 True	0.009 ⊥	0.014 True	0.027 True	0.003 True
	62	3	6	10	0.014 ⊥	0.006 ⊥	0.083 ⊥	0.082 True	Timeout	Timeout
	63	3	4	3	0.016 ⊥	0.004 ⊥	0.077 ⊥	0.076 ⊥	0.502 ⊥	0.048 True
	64	3	4	3	0.003 ⊥	0.003 ⊥	0.015 ⊥	0.019 ⊥	0.046 ⊥	0.022 True
	65	3	4	1	0.003 ⊥	0.002 ⊥	0.016 ⊥	0.018 ⊥	0.031 ⊥	0.098 True
	66	7	14	1	0.002 ⊥	0.001 True	0.007 ⊥	0.006 ⊥	0.007 True	0.003 True
	67	2	4	2	0.006 ⊥	0.002 True	0.008 ⊥	0.013 True	0.030 True	0.003 True
	68	2	4	2	0.012 ⊥	0.003 True	0.015 ⊥	0.036 ⊥	0.077 True	0.006 True
	69	3	4	3	0.007 ⊥	0.005 ⊥	0.028 ⊥	0.031 ⊥	0.067 ⊥	0.052 True
	70	3	6	2	0.001 ⊥	0.002 ⊥	0.018 ⊥	0.030 ⊥	0.050 ⊥	0.013 True
	71	5	6	2	0.002 ⊥	0.003 ⊥	0.078 ⊥	0.185 ⊥	Timeout	0.037 True
	72	9	18	8	0.010 ⊥	0.018 ⊥	Timeout	Timeout	Timeout	Timeout
	73	5	4	4	0.103 ⊥	0.021 ⊥	0.071 ⊥	0.220 ⊥	Timeout	Timeout
	74	9	10	4	0.007 ⊥	0.009 ⊥	0.721 ⊥	0.478 ⊥	Timeout	0.234 True
	75	3	4	3	0.005 ⊥	0.003 ⊥	0.019 ⊥	0.025 ⊥	0.054 ⊥	0.089 True
	76	6	2	2	0.001 True	True	0.005 ⊥	0.010 True	0.015 True	0.002 True