From adb5c0f7cc61ba66b2a989623205293268f1715e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 12 Sep 2023 20:09:14 +0000 Subject: [PATCH] Fix some numbers --- .../MaxOfTwoNumbersUndertrainedSimpler/TheoremStatement.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/MaxOfTwoNumbersUndertrainedSimpler/TheoremStatement.v b/theories/MaxOfTwoNumbersUndertrainedSimpler/TheoremStatement.v index 323c264..53b11fb 100644 --- a/theories/MaxOfTwoNumbersUndertrainedSimpler/TheoremStatement.v +++ b/theories/MaxOfTwoNumbersUndertrainedSimpler/TheoremStatement.v @@ -17,11 +17,11 @@ Import Arith.Instances.Truncating. Local Open Scope raw_tensor_scope. Definition total : int := Eval vm_compute in Shape.item (Shape.reshape (shape_of all_tokens)). -Definition expected_correct : int := Eval vm_compute in total - Uint63.of_Z 0 (* (List.length Heuristics.incorrect_results)*). +Definition expected_correct : int := Eval vm_compute in total - Uint63.of_Z 50 (* (List.length Heuristics.incorrect_results)*). Definition totalf : float := Eval vm_compute in PrimFloat.of_uint63 total. Definition expected_correctf : float := Eval vm_compute in PrimFloat.of_uint63 expected_correct. Definition expected_accuracy : float := Eval vm_compute in expected_correctf / totalf. -Definition expected_loss : float := 0x1.7acd560000000p-23. +Definition expected_loss : float := 0x1.02f06a0000000p-3. Module Accuracy. Definition error : float := Eval cbv in (0.5 / totalf)%float. @@ -31,8 +31,8 @@ Module Accuracy. End Accuracy. Module Loss. - Definition error : float := 0x2p-4%float. + Definition error : float := 0x2p-19%float. Local Notation abs := (@abs float float_has_abs) (only parsing). - Notation best := ((abs (true_loss / expected_loss - 3) <=? error)%float = true) + Notation best := ((abs (true_loss / expected_loss - 1) <=? error)%float = true) (only parsing). End Loss.