This instance will be upgraded to Heptapod 0.31.0 (final) on 2022-05-24 at 14:00 UTC+2 (a few minutes of down time)

Commit 96369422 authored by Alexander Bentkamp's avatar Alexander Bentkamp
Browse files

Add shared weights variant to deep learning thm

--HG--
branch : deep_learning
parent c5bcbcf48fca
......@@ -255,6 +255,16 @@ lemma witness_valid: "valid_net' (witness Y r rs)"
lemma witness'_valid: "valid_net' (witness' Y rs)"
using valid_deep_model' witness'_is_deep_model by auto
lemma shared_weight_net_witness: "shared_weight_net (witness Y r rs)"
proof (induction rs arbitrary:Y r)
case Nil
then show ?case unfolding witness.simps witness'.simps by (simp add: shared_weight_net_Conv shared_weight_net_Input)
next
case (Cons a rs)
then show ?case unfolding witness.simps witness'.simps
by (simp add: shared_weight_net_Conv shared_weight_net_Input shared_weight_net_Pool)
qed
lemma witness_l0': "witness' Y [M] =
(Pool
(Conv (eye_matrix Y M) (Input M))
......@@ -438,6 +448,7 @@ abbreviation "ten2mat == matricize {n. even n}"
abbreviation "mat2ten == dematricize {n. even n}"
locale deep_model_correct_params =
fixes shared_weights::bool
fixes rs::"nat list"
assumes deep:"length rs \<ge> 3"
and no_zeros:"\<And>r. r\<in>set rs \<Longrightarrow> 0 < r"
......@@ -445,7 +456,7 @@ begin
definition "r = min (last rs) (last (butlast rs))"
definition "N_half = 2^(length rs - 3)"
definition "weight_space_dim = count_weights(deep_model_l rs)"
definition "weight_space_dim = count_weights shared_weights (deep_model_l rs)"
end
......@@ -455,7 +466,7 @@ assumes y_valid:"y < rs ! 0"
begin
definition "A ws = tensors_from_net (insert_weights (deep_model_l rs) ws) $ y"
definition "A ws = tensors_from_net (insert_weights shared_weights (deep_model_l rs) ws) $ y"
definition "A' ws = ten2mat (A ws)"
......@@ -498,13 +509,14 @@ shows "dim_row (A' ws) = (last rs) ^ N_half" "dim_col (A' ws) = (last rs) ^ N_ha
definition "Aw = tensors_from_net (witness_l rs) $ y"
definition "Aw' = ten2mat Aw"
definition "witness_weights = (SOME ws. witness_l rs = insert_weights (deep_model_l rs) ws)"
definition "witness_weights = (SOME ws. witness_l rs = insert_weights shared_weights (deep_model_l rs) ws)"
lemma witness_weights:"witness_l rs = insert_weights (deep_model_l rs) witness_weights"
lemma witness_weights:"witness_l rs = insert_weights shared_weights (deep_model_l rs) witness_weights"
proof -
have 0:"\<exists>x. witness_l rs = insert_weights (deep_model_l rs) x"
unfolding weight_space_dim_def using insert_remove_weights witness_is_deep_model by metis
show "witness_l rs = insert_weights (deep_model_l rs) witness_weights"
have 0:"\<exists>x. witness_l rs = insert_weights shared_weights (deep_model_l rs) x"
unfolding weight_space_dim_def using shared_weight_net_witness insert_extract_weights_cong_shared
insert_extract_weights_cong_unshared witness_is_deep_model by (metis (full_types))
show "witness_l rs = insert_weights shared_weights (deep_model_l rs) witness_weights"
unfolding witness_weights_def using someI_ex[OF 0] by blast
qed
......@@ -935,10 +947,10 @@ end
(* Examples to show that the locales can be instantiated: *)
interpretation example : deep_model_correct_params "[10,10,10]"
interpretation example : deep_model_correct_params False "[10,10,10]"
unfolding deep_model_correct_params_def by simp
interpretation example : deep_model_correct_params_y "[10,10,10]" 1
interpretation example : deep_model_correct_params_y False "[10,10,10]" 1
unfolding deep_model_correct_params_y_def deep_model_correct_params_y_axioms_def
deep_model_correct_params_def by simp
......
......@@ -131,7 +131,7 @@ lemma polyfun_evaluate_net_plus_a:
assumes "map dim_vec inputs = input_sizes m"
assumes "valid_net m"
assumes "j < output_size m"
shows "polyfun {..<a + count_weights m} (\<lambda>f. evaluate_net (insert_weights m (\<lambda>i. f (i + a))) inputs $ j)"
shows "polyfun {..<a + count_weights s m} (\<lambda>f. evaluate_net (insert_weights s m (\<lambda>i. f (i + a))) inputs $ j)"
using assms proof (induction m arbitrary:inputs j a)
case (Input)
then show ?case unfolding insert_weights.simps evaluate_net.simps using polyfun_const by metis
......@@ -142,22 +142,22 @@ next
proof (rule polyfun_mult_mat_vec)
{
fix f
have 1:"valid_net' (insert_weights m (\<lambda>i. f (i + x1 * x2)))"
have 1:"valid_net' (insert_weights s m (\<lambda>i. f (i + x1 * x2)))"
using `valid_net (Conv x m)` valid_net.simps by (metis
convnet.distinct(1) convnet.distinct(5) convnet.inject(2) remove_insert_weights)
have 2:"map dim_vec inputs = input_sizes (insert_weights m (\<lambda>i. f (i + x1 * x2)))"
have 2:"map dim_vec inputs = input_sizes (insert_weights s m (\<lambda>i. f (i + x1 * x2)))"
using input_sizes_remove_weights remove_insert_weights
by (simp add: Conv.prems(1))
have "dim_vec (evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2))) inputs) = output_size m"
have "dim_vec (evaluate_net (insert_weights s m (\<lambda>i. f (i + x1 * x2))) inputs) = output_size m"
using output_size_correct[OF 1 2] using remove_insert_weights by auto
then show "evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2))) inputs \<in> carrier_vec (output_size m)"
then show "evaluate_net (insert_weights s m (\<lambda>i. f (i + x1 * x2))) inputs \<in> carrier_vec (output_size m)"
using carrier_vec_def by (metis (full_types) mem_Collect_eq)
}
have "map dim_vec inputs = input_sizes m" by (simp add: Conv.prems(1))
have "valid_net m" using Conv.prems(2) valid_net.cases by fastforce
show "\<And>j. j < output_size m \<Longrightarrow> polyfun {..<a + count_weights (Conv (x1, x2) m)}
(\<lambda>f. evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2 + a))) inputs $ j)"
show "\<And>j. j < output_size m \<Longrightarrow> polyfun {..<a + count_weights s (Conv (x1, x2) m)}
(\<lambda>f. evaluate_net (insert_weights s m (\<lambda>i. f (i + x1 * x2 + a))) inputs $ j)"
unfolding vec_of_list_index count_weights.simps
using Conv(1)[OF `map dim_vec inputs = input_sizes m` `valid_net m`, of _ "x1 * x2 + a"]
unfolding semigroup_add_class.add.assoc ab_semigroup_add_class.add.commute[of "x1 * x2" a]
......@@ -167,78 +167,81 @@ next
show "\<And>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 \<in> carrier_mat x1 (output_size m)" unfolding `output_size m = x2` using dim_extract_matrix
using carrier_matI by (metis (no_types, lifting))
show "\<And>i j. i < x1 \<Longrightarrow> j < output_size m \<Longrightarrow> polyfun {..<a + count_weights (Conv (x1, x2) m)} (\<lambda>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 $$ (i, j))"
unfolding `output_size m = x2` count_weights.simps using polyfun_extract_matrix[of _ x1 _ x2 a "count_weights m"] by blast
show "\<And>i j. i < x1 \<Longrightarrow> j < output_size m \<Longrightarrow> polyfun {..<a + count_weights s (Conv (x1, x2) m)} (\<lambda>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 $$ (i, j))"
unfolding `output_size m = x2` count_weights.simps using polyfun_extract_matrix[of _ x1 _ x2 a "count_weights s m"] by blast
show "j < x1" using Conv.prems(3) \<open>x = (x1, x2)\<close> by auto
qed
next
case (Pool m1 m2 inputs j a)
have A2:"\<And>f. map dim_vec (take (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m1"
have A2:"\<And>f. map dim_vec (take (length (input_sizes (insert_weights s m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m1"
by (metis Pool.prems(1) append_eq_conv_conj input_sizes.simps(3) input_sizes_remove_weights remove_insert_weights take_map)
have B2:"\<And>f. map dim_vec (drop (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m2"
have B2:"\<And>f. map dim_vec (drop (length (input_sizes (insert_weights s m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m2"
using Pool.prems(1) append_eq_conv_conj input_sizes.simps(3) input_sizes_remove_weights remove_insert_weights by (metis drop_map)
have A3:"valid_net m1" and B3:"valid_net m2" using `valid_net (Pool m1 m2)` valid_net.simps by blast+
have "output_size (Pool m1 m2) = output_size m2" unfolding output_size.simps
using `valid_net (Pool m1 m2)` "valid_net.cases" by fastforce
then have A4:"j < output_size m1" and B4:"j < output_size m2" using `j < output_size (Pool m1 m2)` by simp_all
let ?net1 = "\<lambda>f. evaluate_net (insert_weights m1 (\<lambda>i. f (i + a)))
(take (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs)"
let ?net2 = "\<lambda>f. evaluate_net (insert_weights m2 (\<lambda>i. f (i + count_weights m1 + a)))
(drop (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs)"
let ?net1 = "\<lambda>f. evaluate_net (insert_weights s m1 (\<lambda>i. f (i + a)))
(take (length (input_sizes (insert_weights s m1 (\<lambda>i. f (i + a))))) inputs)"
let ?net2 = "\<lambda>f. evaluate_net (insert_weights s m2 (if s then \<lambda>i. f (i + a) else (\<lambda>i. f (i + count_weights s m1 + a))))
(drop (length (input_sizes (insert_weights s m1 (\<lambda>i. f (i + a))))) inputs)"
have length1: "\<And>f. output_size m1 = dim_vec (?net1 f)"
by (metis A2 A3 input_sizes_remove_weights output_size_correct remove_insert_weights)
then have jlength1:"\<And>f. j < dim_vec (?net1 f)" using A4 by metis
have length2: "\<And>f. output_size m2 = dim_vec (?net2 f)"
by (metis B2 B3 input_sizes_remove_weights output_size_correct remove_insert_weights)
then have jlength2:"\<And>f. j < dim_vec (?net2 f)" using B4 by metis
have cong1:"\<And>xf. (\<lambda>f. evaluate_net (insert_weights m1 (\<lambda>i. f (i + a)))
(take (length (input_sizes (insert_weights m1 (\<lambda>i. xf (i + a))))) inputs) $ j)
have cong1:"\<And>xf. (\<lambda>f. evaluate_net (insert_weights s m1 (\<lambda>i. f (i + a)))
(take (length (input_sizes (insert_weights s m1 (\<lambda>i. xf (i + a))))) inputs) $ j)
= (\<lambda>f. ?net1 f $ j)"
using input_sizes_remove_weights remove_insert_weights by auto
have cong2:"\<And>xf. (\<lambda>f. evaluate_net (insert_weights m2 (\<lambda>i. f (i + (a + count_weights m1))))
(drop (length (input_sizes (insert_weights m1 (\<lambda>i. xf (i + a))))) inputs) $ j)
have cong2:"\<And>xf. (\<lambda>f. evaluate_net (insert_weights s m2 (\<lambda>i. f (i + (a + (if s then 0 else count_weights s m1)))))
(drop (length (input_sizes (insert_weights s m1 (\<lambda>i. xf (i + a))))) inputs) $ j)
= (\<lambda>f. ?net2 f $ j)"
unfolding semigroup_add_class.add.assoc[symmetric] ab_semigroup_add_class.add.commute[of a "count_weights m1"]
unfolding semigroup_add_class.add.assoc[symmetric] ab_semigroup_add_class.add.commute[of a "if s then 0 else count_weights s m1"]
using input_sizes_remove_weights remove_insert_weights by auto
show ?case unfolding insert_weights.simps evaluate_net.simps index_component_mult[OF jlength1 jlength2] count_weights.simps
show ?case unfolding insert_weights.simps evaluate_net.simps count_weights.simps
unfolding index_component_mult[OF jlength1 jlength2]
apply (rule polyfun_mult)
using Pool.IH(1)[OF A2 A3 A4, of a, unfolded cong1]
using Pool.IH(2)[OF B2 B3 B4, of "a + count_weights m1", unfolded cong2 semigroup_add_class.add.assoc[of a]]
using polyfun_subset[of "{..<a + count_weights m1}" "{..<a + (count_weights m1 + count_weights m2)}"]
by auto
using Pool.IH(1)[OF A2 A3 A4, of a, unfolded cong1]
apply (simp add:polyfun_subset[of "{..<a + count_weights s m1}" "{..<a + (if s then max (count_weights s m1) (count_weights s m2) else count_weights s m1 + count_weights s m2)}"])
using Pool.IH(2)[OF B2 B3 B4, of "a + (if s then 0 else count_weights s m1)", unfolded cong2 semigroup_add_class.add.assoc[of a]]
by (simp add:polyfun_subset[of "{..<a + ((if s then 0 else count_weights s m1) + count_weights s m2)}" "{..<a + (if s then max (count_weights s m1) (count_weights s m2) else count_weights s m1 + count_weights s m2)}"])
qed
lemma polyfun_evaluate_net:
assumes "map dim_vec inputs = input_sizes m"
assumes "valid_net m"
assumes "j < output_size m"
shows "polyfun {..<count_weights m} (\<lambda>f. evaluate_net (insert_weights m f) inputs $ j)"
shows "polyfun {..<count_weights s m} (\<lambda>f. evaluate_net (insert_weights s m f) inputs $ j)"
using polyfun_evaluate_net_plus_a[where a=0, OF assms] by simp
lemma polyfun_tensors_from_net:
assumes "valid_net m"
assumes "is \<lhd> input_sizes m"
assumes "j < output_size m"
shows "polyfun {..<count_weights m} (\<lambda>f. Tensor.lookup (tensors_from_net (insert_weights m f) $ j) is)"
shows "polyfun {..<count_weights s m} (\<lambda>f. Tensor.lookup (tensors_from_net (insert_weights s m f) $ j) is)"
proof -
have 1:"\<And>f. valid_net' (insert_weights m f)" by (simp add: assms(1) remove_insert_weights)
have input_sizes:"\<And>f. input_sizes (insert_weights m f) = input_sizes m"
have 1:"\<And>f. valid_net' (insert_weights s m f)" by (simp add: assms(1) remove_insert_weights)
have input_sizes:"\<And>f. input_sizes (insert_weights s m f) = input_sizes m"
unfolding input_sizes_remove_weights by (simp add: remove_insert_weights)
have 2:"\<And>f. is \<lhd> input_sizes (insert_weights m f)"
have 2:"\<And>f. is \<lhd> input_sizes (insert_weights s m f)"
unfolding input_sizes using assms(2) by blast
have 3:"\<And>f. j < output_size' (insert_weights m f)"
have 3:"\<And>f. j < output_size' (insert_weights s m f)"
by (simp add: assms(3) remove_insert_weights)
have "\<And>f1 f2. base_input (insert_weights m f1) is = base_input (insert_weights m f2) is"
have "\<And>f1 f2. base_input (insert_weights s m f1) is = base_input (insert_weights s m f2) is"
unfolding base_input_def by (simp add: input_sizes)
then have "\<And>xf. (\<lambda>f. evaluate_net (insert_weights m f) (base_input (insert_weights m xf) is) $ j)
= (\<lambda>f. evaluate_net (insert_weights m f) (base_input (insert_weights m f) is) $ j)"
then have "\<And>xf. (\<lambda>f. evaluate_net (insert_weights s m f) (base_input (insert_weights s m xf) is) $ j)
= (\<lambda>f. evaluate_net (insert_weights s m f) (base_input (insert_weights s m f) is) $ j)"
by metis
then show ?thesis unfolding lookup_tensors_from_net[OF 1 2 3]
using polyfun_evaluate_net[OF base_input_length[OF 2, unfolded input_sizes, symmetric] assms(1) assms(3)]
by fastforce
using polyfun_evaluate_net[OF base_input_length[OF 2, unfolded input_sizes, symmetric] assms(1) assms(3), of s]
(* TODO: Investigate why sledgehammer fails:
using polyfun_evaluate_net[OF base_input_length[OF 2, unfolded input_sizes, symmetric] assms(1) assms(3)] sledgehammer *)
by simp
qed
lemma polyfun_matricize:
......@@ -291,9 +294,9 @@ definition witness_submatrix where
lemma polyfun_tensor_deep_model:
assumes "is \<lhd> input_sizes (deep_model_l rs)"
shows "polyfun {..<weight_space_dim}
(\<lambda>f. Tensor.lookup (tensors_from_net (insert_weights (deep_model_l rs) f) $ y) is)"
(\<lambda>f. Tensor.lookup (tensors_from_net (insert_weights shared_weights (deep_model_l rs) f) $ y) is)"
proof -
have 1:"\<And>f. remove_weights (insert_weights (deep_model_l rs) f) = deep_model_l rs"
have 1:"\<And>f. remove_weights (insert_weights shared_weights (deep_model_l rs) f) = deep_model_l rs"
using remove_insert_weights by metis
then have "y < output_size ( deep_model_l rs)" using valid_deep_model y_valid length_output_deep_model by force
have 0:"{..<weight_space_dim} = set [0..<weight_space_dim]" by auto
......@@ -311,7 +314,7 @@ assumes "j<(last rs) ^ N_half"
shows "polyfun {..<weight_space_dim} (\<lambda>f. A' f $$ (i,j))"
proof -
have 0:"y < output_size ( deep_model_l rs )" using valid_deep_model y_valid length_output_deep_model by force
have 1:"\<And>f. remove_weights (insert_weights (deep_model_l rs) f) = deep_model_l rs"
have 1:"\<And>f. remove_weights (insert_weights shared_weights (deep_model_l rs) f) = deep_model_l rs"
using remove_insert_weights by metis
have 2:"(\<And>f is. is \<lhd> replicate (2 * N_half) (last rs) \<Longrightarrow>
polyfun {..<weight_space_dim} (\<lambda>x. Tensor.lookup (A x) is))"
......@@ -329,7 +332,7 @@ assumes "j < r ^ N_half"
shows "polyfun {..<weight_space_dim} (\<lambda>f. witness_submatrix f $$ (i,j))"
unfolding witness_submatrix_def
proof (rule polyfun_submatrix)
have 1:"\<And>f. remove_weights (insert_weights (deep_model_l rs) f) = deep_model_l rs"
have 1:"\<And>f. remove_weights (insert_weights shared_weights (deep_model_l rs) f) = deep_model_l rs"
using remove_insert_weights by metis
show "\<And>f. A' f \<in> carrier_mat ((last rs) ^ N_half) ((last rs) ^ N_half)"
using "1" dims_A'_pow using weight_space_dim_def by auto
......@@ -347,7 +350,7 @@ lemma polyfun_det_deep_model:
shows "polyfun {..<weight_space_dim} (\<lambda>f. det (witness_submatrix f))"
proof (rule polyfun_det)
fix f
have "remove_weights (insert_weights (deep_model_l rs) f) = deep_model_l rs"
have "remove_weights (insert_weights shared_weights (deep_model_l rs) f) = deep_model_l rs"
using remove_insert_weights by metis
show "witness_submatrix f \<in> carrier_mat (r ^ N_half) (r ^ N_half)"
......
......@@ -28,6 +28,12 @@ lemma extract_matrix_flatten_matrix:
"extract_matrix (flatten_matrix A) (dim_row A) (dim_col A) = A"
unfolding extract_matrix_def flatten_matrix_def by auto
lemma extract_matrix_flatten_matrix_cong:
assumes "\<And>x. x < dim_row A * dim_col A \<Longrightarrow> f x = flatten_matrix A x"
shows "extract_matrix f (dim_row A) (dim_col A) = A"
unfolding extract_matrix_def
by (metis assms extract_matrix_cong extract_matrix_def extract_matrix_flatten_matrix)
lemma flatten_matrix_extract_matrix:
"flatten_matrix (extract_matrix a m n) k = a k" if "k < m * n"
proof -
......
......@@ -45,31 +45,34 @@ qed
lemma if_polynomial_0_evaluate:
assumes "polynomial_f wd \<noteq> 0"
assumes "\<forall>inputs. input_sizes (deep_model_l rs) = map dim_vec inputs \<longrightarrow> evaluate_net (insert_weights (deep_model_l rs) wd) inputs
= evaluate_net (insert_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws) inputs"
assumes "\<forall>inputs. input_sizes (deep_model_l rs) = map dim_vec inputs \<longrightarrow> evaluate_net (insert_weights shared_weights (deep_model_l rs) wd) inputs
= evaluate_net (insert_weights shared_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws) inputs"
shows "Z \<ge> r ^ N_half"
proof -
have valid1:"valid_net' (insert_weights (deep_model_l rs) wd)"
have valid1:"valid_net' (insert_weights shared_weights (deep_model_l rs) wd)"
using remove_insert_weights valid_deep_model by presburger
have valid2:"valid_net' (insert_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws)"
have valid2:"valid_net' (insert_weights shared_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws)"
by (simp add: remove_insert_weights valid_shallow_model)
have input_sizes: "input_sizes (insert_weights (deep_model_l rs) wd)
= input_sizes (insert_weights (shallow_model (rs ! 0) Z (last rs) (2 * N_half - 1)) ws)"
have input_sizes: "input_sizes (insert_weights shared_weights (deep_model_l rs) wd)
= input_sizes (insert_weights shared_weights (shallow_model (rs ! 0) Z (last rs) (2 * N_half - 1)) ws)"
by (metis N_half_def Suc_mult_two_diff_one input_sizes_remove_weights input_sizes_shallow_model local.input_sizes_deep_model power_eq_0_iff remove_insert_weights zero_neq_numeral)
have "tensors_from_net (insert_weights (deep_model_l rs) wd)
= tensors_from_net (insert_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half -1)) ws)"
have 0:"tensors_from_net (insert_weights shared_weights (deep_model_l rs) wd)
= tensors_from_net (insert_weights shared_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half -1)) ws)"
using tensors_from_net_eqI[OF valid1 valid2 input_sizes, unfolded input_sizes_remove_weights remove_insert_weights]
using assms by blast
have "cprank (tensors_from_net (insert_weights shared_weights (deep_model_l rs) wd) $ y) \<le> Z"
unfolding 0 using y_valid cprank_shallow_model by blast
then show ?thesis
using if_polynomial_0_rank assms
by (metis A_def assms(1) cprank_shallow_model less_le_trans not_le remove_insert_weights y_valid)
using A_def assms(1) less_le_trans not_le remove_insert_weights
by fastforce
qed
lemma if_polynomial_0_evaluate_notex:
assumes "polynomial_f wd \<noteq> 0"
shows "\<not>(\<exists>weights_shallow Z. Z < r ^ N_half \<and> (\<forall>inputs. input_sizes (deep_model_l rs) = map dim_vec inputs \<longrightarrow>
evaluate_net (insert_weights (deep_model_l rs) wd) inputs
= evaluate_net (insert_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws) inputs))"
evaluate_net (insert_weights shared_weights (deep_model_l rs) wd) inputs
= evaluate_net (insert_weights shared_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws) inputs))"
using assms if_polynomial_0_evaluate not_le by blast
theorem fundamental_theorem_network_capacity:
......@@ -80,8 +83,8 @@ using AE_I'[OF lebesgue_mpoly_zero_set[OF polynomial_p_not_0 vars_polynomial_p]]
theorem fundamental_theorem_network_capacity_v2:
shows "AE wd in lborel_f weight_space_dim.
\<not>(\<exists>ws Z. Z < r ^ N_half \<and> (\<forall>inputs. input_sizes (deep_model_l rs) = map dim_vec inputs \<longrightarrow>
evaluate_net (insert_weights (deep_model_l rs) wd) inputs
= evaluate_net (insert_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws) inputs))"
evaluate_net (insert_weights shared_weights (deep_model_l rs) wd) inputs
= evaluate_net (insert_weights shared_weights (shallow_model (rs ! 0) Z (last rs) (2*N_half-1)) ws) inputs))"
apply (rule AE_I'[OF lebesgue_mpoly_zero_set[OF polynomial_p_not_0 vars_polynomial_p], unfolded polynomial_pf])
apply (rule subsetI) unfolding mem_Collect_eq
using if_polynomial_0_evaluate_notex by metis
......
......@@ -18,10 +18,13 @@ fun input_sizes :: "'a convnet \<Rightarrow> nat list" where
"input_sizes (Conv A m) = input_sizes m" |
"input_sizes (Pool m1 m2) = input_sizes m1 @ input_sizes m2"
fun count_weights :: "(nat \<times> nat) convnet \<Rightarrow> nat" where
"count_weights (Input M) = 0" |
"count_weights (Conv (r0, r1) m) = r0 * r1 + count_weights m" |
"count_weights (Pool m1 m2) = count_weights m1 + count_weights m2"
fun count_weights :: "bool \<Rightarrow> (nat \<times> nat) convnet \<Rightarrow> nat" where
"count_weights shared (Input M) = 0" |
"count_weights shared (Conv (r0, r1) m) = r0 * r1 + count_weights shared m" |
"count_weights shared (Pool m1 m2) =
(if shared
then max (count_weights shared m1) (count_weights shared m2)
else count_weights shared m1 + count_weights shared m2)"
fun output_size :: "(nat \<times> nat) convnet \<Rightarrow> nat" where
"output_size (Input M) = M" |
......@@ -34,14 +37,14 @@ inductive valid_net :: "(nat\<times>nat) convnet \<Rightarrow> bool" where
"output_size m1 = output_size m2 \<Longrightarrow> valid_net m1 \<Longrightarrow> valid_net m2 \<Longrightarrow> valid_net (Pool m1 m2)"
fun insert_weights :: "(nat \<times> nat) convnet \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> real mat convnet" where
"insert_weights (Input M) w = Input M" |
"insert_weights (Conv (r0,r1) m) w = Conv
fun insert_weights :: "bool \<Rightarrow> (nat \<times> nat) convnet \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> real mat convnet" where
"insert_weights shared (Input M) w = Input M" |
"insert_weights shared (Conv (r0,r1) m) w = Conv
(extract_matrix w r0 r1)
(insert_weights m (\<lambda>i. w (i+r0*r1)))" |
"insert_weights (Pool m1 m2) w = Pool
(insert_weights m1 w)
(insert_weights m2 (\<lambda>i. w (i+(count_weights m1))))"
(insert_weights shared m (\<lambda>i. w (i+r0*r1)))" |
"insert_weights shared (Pool m1 m2) w = Pool
(insert_weights shared m1 w)
(insert_weights shared m2 (if shared then w else (\<lambda>i. w (i+(count_weights shared m1)))))"
fun remove_weights :: "real mat convnet \<Rightarrow> (nat \<times> nat) convnet" where
"remove_weights (Input M) = Input M" |
......@@ -63,25 +66,28 @@ where "mat_tensorlist_mult A Ts ds
= Matrix.vec (dim_row A) (\<lambda>j. tensor_from_lookup ds (\<lambda>is. (A *\<^sub>v (map_vec (\<lambda>T. Tensor.lookup T is) Ts)) $j))"
lemma insert_weights_cong:
assumes "(\<And>i. i<count_weights m \<Longrightarrow> w1 i = w2 i)"
shows "insert_weights m w1 = insert_weights m w2"
assumes "(\<And>i. i<count_weights s m \<Longrightarrow> w1 i = w2 i)"
shows "insert_weights s m w1 = insert_weights s m w2"
using assms proof (induction m arbitrary: w1 w2)
case Input
then show ?case by simp
next
case (Conv r01 m)
then obtain r0 r1 where "r01 = (r0,r1)" by (meson surj_pair)
have 2:"insert_weights m (\<lambda>i. w1 (i + r0 * r1)) = insert_weights m (\<lambda>i. w2 (i + r0 * r1))" using Conv
have 2:"insert_weights s m (\<lambda>i. w1 (i + r0 * r1)) = insert_weights s m (\<lambda>i. w2 (i + r0 * r1))" using Conv
using \<open>r01 = (r0, r1)\<close> add.commute add_less_cancel_right count_weights.simps(2) by fastforce
then show ?case unfolding `r01 = (r0,r1)` insert_weights.simps
by (metis Conv.prems \<open>r01 = (r0, r1)\<close> count_weights.simps(2) extract_matrix_cong trans_less_add1)
next
case (Pool m1 m2)
have 1:"insert_weights m1 w1 = insert_weights m1 w2"
using Pool(1)[of w1 w2] Pool(3)[unfolded count_weights.simps] by simp
have 2:"insert_weights m2 (\<lambda>i. w1 (i + count_weights m1)) = insert_weights m2 (\<lambda>i. w2 (i + count_weights m1))"
using Pool(2)[of "\<lambda>i. w1 (i + count_weights m1)" "\<lambda>i. w2 (i + count_weights m1)"] Pool(3)[unfolded count_weights.simps] by simp
show ?case unfolding insert_weights.simps 1 2 by metis
have 1:"insert_weights s m1 w1 = insert_weights s m1 w2"
using Pool(1)[of w1 w2] Pool(3)[unfolded count_weights.simps]
by (cases s; auto)
have shared:"s=True \<Longrightarrow> insert_weights s m2 w1 = insert_weights s m2 w2"
using Pool(2)[of w1 w2] Pool(3)[unfolded count_weights.simps] by auto
have unshared:"s=False \<Longrightarrow> insert_weights s m2 (\<lambda>i. w1 (i + count_weights s m1)) = insert_weights s m2 (\<lambda>i. w2 (i + count_weights s m1))"
using Pool(2) Pool(3) count_weights.simps by fastforce
show ?case unfolding insert_weights.simps 1 using unshared shared by simp
qed
lemma dims_mat_tensorlist_mult:
......@@ -347,40 +353,85 @@ next
then show ?case using lookup_prod IH base_input_def by auto
qed
lemma insert_remove_weights:
obtains w where "m = insert_weights (remove_weights m) w"
proof (induction m arbitrary:thesis)
case (Input m thesis)
then show ?case by simp
primrec extract_weights::"bool \<Rightarrow> real mat convnet \<Rightarrow> nat \<Rightarrow> real" where
extract_weights_Input: "extract_weights shared (Input M) = (\<lambda>x. 0)"
| extract_weights_Conv: "extract_weights shared (Conv A m) =
(\<lambda>x. if x < dim_row A * dim_col A then flatten_matrix A x
else extract_weights shared m (x - dim_row A * dim_col A))"
| extract_weights_Pool: "extract_weights shared (Pool m1 m2) =
(\<lambda>x. if x < count_weights shared (remove_weights m1)
then extract_weights shared m1 x
else extract_weights shared m2 (x - count_weights shared (remove_weights m1)))"
inductive balanced_net::"(nat \<times> nat) convnet \<Rightarrow> bool" where
balanced_net_Input: "balanced_net (Input M)"
| balanced_net_Conv: "balanced_net m \<Longrightarrow> balanced_net (Conv A m)"
| balanced_net_Pool: "balanced_net m1 \<Longrightarrow> balanced_net m2 \<Longrightarrow>
count_weights True m1 = count_weights True m2 \<Longrightarrow> balanced_net (Pool m1 m2)"
inductive shared_weight_net::"real mat convnet \<Rightarrow> bool" where
shared_weight_net_Input: "shared_weight_net (Input M)"
| shared_weight_net_Conv: "shared_weight_net m \<Longrightarrow> shared_weight_net (Conv A m)"
| shared_weight_net_Pool: "shared_weight_net m1 \<Longrightarrow> shared_weight_net m2 \<Longrightarrow>
count_weights True (remove_weights m1) = count_weights True (remove_weights m2) \<Longrightarrow>
(\<And>x. x < count_weights True (remove_weights m1) \<Longrightarrow> extract_weights True m1 x = extract_weights True m2 x)
\<Longrightarrow> shared_weight_net (Pool m1 m2)"
lemma insert_extract_weights_cong_shared:
assumes "shared_weight_net m"
assumes "\<And>x. x < count_weights True (remove_weights m) \<Longrightarrow> f x = extract_weights True m x"
shows "m = insert_weights True (remove_weights m) f"
using assms proof (induction m arbitrary:f)
case (shared_weight_net_Input M)
then show ?case
by simp
next
case (shared_weight_net_Conv m A)
have "extract_matrix f (dim_row A) (dim_col A) = A"
by (simp add: extract_matrix_cong extract_matrix_flatten_matrix shared_weight_net_Conv.prems)
then show ?case
using shared_weight_net_Conv.IH[of "(\<lambda>i. f (i + dim_row A * dim_col A))"]
using shared_weight_net_Conv.prems by auto
next
case (Conv A m thesis)
then obtain w where "m = insert_weights (remove_weights m) w" by auto
then have 1:"remove_weights (Conv A m) = Conv (dim_row A, dim_col A) (remove_weights m)" by simp
have "Conv A m = insert_weights (remove_weights (Conv A m)) (\<lambda>i. if i<dim_row A *dim_col A then flatten_matrix A i else w (i-dim_row A *dim_col A))"
unfolding 1 insert_weights.simps
using extract_matrix_flatten_matrix[of A] extract_matrix_cong[of "dim_row A" "dim_col A"
"\<lambda>i. if i < dim_row A * dim_col A then flatten_matrix A i else w (i - dim_row A * dim_col A)" "flatten_matrix A"]
using \<open>m = insert_weights (remove_weights m) w\<close> by fastforce
then show ?case using Conv.prems by blast
case (shared_weight_net_Pool m1 m2)
have "m1 = insert_weights True (remove_weights m1) f"
using shared_weight_net_Pool.IH(1) shared_weight_net_Pool.prems by auto
have "m2 = insert_weights True (remove_weights m2) f"
using local.shared_weight_net_Pool(3) shared_weight_net_Pool.IH(2)
shared_weight_net_Pool.hyps(4) shared_weight_net_Pool.prems by fastforce
then show ?case
using \<open>m1 = insert_weights True (remove_weights m1) f\<close> by auto
qed
lemma insert_extract_weights_cong_unshared:
assumes "\<And>x. x < count_weights False (remove_weights m) \<Longrightarrow> f x = extract_weights False m x"
shows "m = insert_weights False (remove_weights m) f"
using assms proof (induction m arbitrary:f)
case (Input M)
then show ?case
by simp
next
case (Conv A m)
then have "extract_matrix f (dim_row A) (dim_col A) = A"
by (metis count_weights.simps(2) extract_matrix_flatten_matrix_cong extract_weights_Conv remove_weights.simps(2) trans_less_add1)
then show ?case
using Conv.IH Conv.prems by auto
next
case (Pool m1 m2)
then obtain w1 w2 where "m1 = insert_weights (remove_weights m1) w1" "m2 = insert_weights (remove_weights m2) w2" by metis
then have "Pool m1 m2 = insert_weights (remove_weights (Pool m1 m2)) (\<lambda>i. if i<count_weights (remove_weights m1) then w1 i else w2 (i - count_weights (remove_weights m1)))"
unfolding remove_weights.simps insert_weights.simps
using insert_weights_cong[of _ "\<lambda>i. if i < count_weights (remove_weights m1) then w1 i else w2 (i - count_weights (remove_weights m1))" w1] by fastforce
then show ?case unfolding Pool using Pool.prems by blast
then show ?case
using Pool.IH(1) Pool.IH(2) Pool.prems by auto
qed
lemma remove_insert_weights:
shows "remove_weights (insert_weights m w) = m"
shows "remove_weights (insert_weights s m w) = m"
proof (induction m arbitrary:w)
case Input
then show ?case by simp
next
case (Conv r12 m)
then obtain r1 r2 where "r12 = (r1, r2)" by fastforce
then have "remove_weights (insert_weights m w) = m" using Conv.IH by blast
then have "remove_weights (insert_weights (Conv (r1,r2) m) w) = Conv (r1,r2) m"
then have "remove_weights (insert_weights s m w) = m" using Conv.IH by blast
then have "remove_weights (insert_weights s (Conv (r1,r2) m) w) = Conv (r1,r2) m"
unfolding insert_weights.simps remove_weights.simps
using extract_matrix_def Conv.IH dim_extract_matrix(1) by (metis dim_col_mat(1) )
then show ?case using \<open>r12 = (r1, r2)\<close> by blast
......@@ -389,6 +440,51 @@ next
then show ?case unfolding insert_weights.simps remove_weights.simps using Pool.IH by blast
qed
lemma extract_insert_weights_shared:
assumes "x<count_weights True m"
and "balanced_net m"
shows "extract_weights True (insert_weights True m w) x = w x"
using assms
proof (induction m arbitrary:w x)
case (Input x)
then show ?case
by simp
next
case (Conv r01 m)
obtain r0 r1 where "r01 = (r0,r1)" by force
then show ?case unfolding \<open>r01 = (r0,r1)\<close> insert_weights.simps extract_weights.simps
apply (cases "x < dim_row (extract_matrix w r0 r1) * dim_col (extract_matrix w r0 r1)")
apply (auto simp add: dim_extract_matrix(1) dim_extract_matrix(2) flatten_matrix_extract_matrix)
using Conv.IH[of _ "\<lambda>i. w (i + r0 * r1)"] Conv.prems(1) Conv.prems(2) \<open>r01 = (r0, r1)\<close> balanced_net.cases by force
next
case (Pool m1 m2)
then show ?case unfolding insert_weights.simps extract_weights.simps remove_insert_weights
apply (cases "x < count_weights True m1")
apply (metis balanced_net.simps convnet.distinct(5) convnet.inject(3) count_weights.simps(1) not_less_zero)
by (metis (no_types, lifting) balanced_net.simps convnet.distinct(5) convnet.inject(3) count_weights.simps(1) count_weights.simps(3) less_max_iff_disj not_less_zero)
qed
lemma shared_weight_net_insert_weights: "balanced_net m \<Longrightarrow> shared_weight_net (insert_weights True m w)"
proof (induction m arbitrary:w)
case (Input x)
then show ?case using insert_weights.simps balanced_net.simps shared_weight_net.simps by metis
next
case (Conv r01 m)
then obtain r0 r1 where "r01 = (r0,r1)" by force
then show ?case unfolding \<open>r01 = (r0,r1)\<close> insert_weights.simps
by (metis Conv.IH Conv.prems balanced_net.simps convnet.distinct(1) convnet.distinct(5) convnet.inject(2) shared_weight_net_Conv)
next
case (Pool m1 m2)
have "balanced_net m1" "balanced_net m2"
using Pool.prems balanced_net.simps by blast+
have "\<And>x. x < count_weights True m1 \<Longrightarrow>
extract_weights True (insert_weights True m1 w) x = extract_weights True (insert_weights True m2 w) x"
using extract_insert_weights_shared
by (metis Pool.prems balanced_net.simps convnet.distinct(3) convnet.distinct(5) convnet.inject(3))
then show ?case unfolding insert_weights.simps using Pool(1)[of w] Pool(2)[of w]
by (metis Pool.prems balanced_net.simps convnet.distinct(3) convnet.distinct(5) convnet.inject(3) remove_insert_weights shared_weight_net_Pool)
qed
lemma finite_valid_index: "finite {is. is \<lhd> ds}"
proof (induction ds)
case Nil
......
......@@ -29,71 +29,90 @@ lemma output_size_shallow_model: "output_size (shallow_model Y Z M N) = Y"
lemma input_sizes_shallow_model: "input_sizes (shallow_model Y Z M N) = replicate (Suc N) M"
apply (induction N) unfolding shallow_model_def input_sizes.simps by simp_all
lemma balanced_net_shallow_model': "balanced_net (shallow_model' Z M N)"
proof(induction N)
case 0
then show ?case
by (metis balanced_net.simps shallow_model'.simps(1))
next
case (Suc N)
have "count_weights True (Conv (Z, M) (Input M)) = count_weights True (shallow_model' Z M N)"
by (induction N; simp)
then show ?case unfolding shallow_model'.simps
by (simp add: Suc.IH balanced_net_Conv balanced_net_Input balanced_net_Pool)
qed
lemma balanced_net_shallow_model: "balanced_net (shallow_model Y Z M N)"
unfolding shallow_model_def
by (simp add: balanced_net_Conv balanced_net_shallow_model')
lemma cprank_max1_shallow_model':
assumes "y < output_size (shallow_model' Z M N)"
shows "cprank_max1 (tensors_from_net (insert_weights (shallow_model' Z M N) w) $ y)"
shows "cprank_max1 (tensors_from_net (insert_weights s (shallow_model' Z M N) w) $ y)"
using assms proof (induction N arbitrary:w)
case 0
then have "input_sizes (insert_weights (shallow_model' Z M 0) w) = [M]"
then have "input_sizes (insert_weights s (shallow_model' Z M 0) w) = [M]"
unfolding shallow_model_def shallow_model'.simps insert_weights.simps
input_sizes.simps by metis
then have "dims (tensors_from_net (insert_weights (shallow_model' Z M 0) w) $ y) = [M]"
then have "dims (tensors_from_net (insert_weights s (shallow_model' Z M 0) w) $ y) = [M]"
using dims_tensors_from_net[OF vec_setI] "0.prems"(1) output_size_correct_tensors
remove_insert_weights valid_shallow_model' by metis
then show ?case
using order1 by (metis One_nat_def eq_imp_le length_Cons list.size(3))
next
case (Suc N)
have y_le_IH:"y < dim_vec (tensors_from_net (insert_weights (shallow_model' Z M N) (\<lambda>i. w (i + (count_weights (shallow_model' Z M 0))))))"
using output_size_correct_tensors[of "insert_weights (shallow_model' Z M N) (\<lambda>i. w (i + (count_weights (shallow_model' Z M 0))))",
have y_le_IH:"y < dim_vec (tensors_from_net (insert_weights s (shallow_model' Z M N) (\<lambda>i. w (i + (count_weights s (shallow_model' Z M 0))))))"
using output_size_correct_tensors[of "insert_weights s (shallow_model' Z M N) (\<lambda>i. w (i + (count_weights s (shallow_model' Z M 0))))",
unfolded remove_insert_weights, OF valid_shallow_model']
using Suc.prems(1) output_size_shallow_model' by auto
have cprank_max1_IH:"cprank_max1 (tensors_from_net (insert_weights (shallow_model' Z M N) (\<lambda>i. w (i + (count_weights (shallow_model' Z M 0))))) $ y)"
have cprank_max1_IH:"cprank_max1 (tensors_from_net (insert_weights s (shallow_model' Z M N) (\<lambda>i. w (i + (count_weights s (shallow_model' Z M 0))))) $ y)"
using Suc.IH Suc.prems(1) output_size_shallow_model' by auto
have y_le_0:"y < dim_vec (tensors_from_net (insert_weights (shallow_model' Z M 0) w))"
have y_le_0:"y < dim_vec (tensors_from_net (insert_weights s (shallow_model' Z M 0) w))"
by (metis assms output_size_correct_tensors output_size_shallow_model' remove_insert_weights valid_shallow_model')
have cprank_max1_0:"cprank_max1 (tensors_from_net (insert_weights (shallow_model' Z M 0) w) $ y)"
have cprank_max1_0:"cprank_max1 (tensors_from_net (insert_weights s (shallow_model' Z M 0) w) $ y)"
proof -
have "input_sizes (insert_weights (shallow_model' Z M 0) w) = [M]"
have "input_sizes (insert_weights s (shallow_model' Z M 0) w) = [M]"
unfolding shallow_model_def shallow_model'.simps insert_weights.simps
input_sizes.simps by metis
then show ?thesis using order1 dims_tensors_from_net[OF vec_setI] One_nat_def eq_imp_le length_Cons list.size(3) y_le_0 by metis
qed
then show ?case unfolding shallow_model'.simps(2) insert_weights.simps tensors_from_net.simps
using cprank_max1_IH cprank_max1_0 cprank_max1_prod index_component_mult y_le_0 y_le_IH by fastforce
using cprank_max1_IH cprank_max1_0 cprank_max1_prod index_component_mult y_le_0 y_le_IH
by (metis Suc.IH output_size_correct_tensors remove_insert_weights valid_shallow_model')
qed