Fix some numbers

JasonGross · Sep 12, 2023 · adb5c0f · adb5c0f
1 parent c1e1622
commit adb5c0f
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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.