[Afp-submit] AFP entry Neural_Networks

[Peter Lammich]

It looks like what has changed is the pretty-printing. I think (just did 
a quick check with Java) as a IEEE-32 value, both numbers are the same 
(the closest IEEE-32 floating point number to this decimal 
representation is the same, namely 3be810c5).

--

   Peter



On 20/11/2025 12:35, Lawrence Paulson wrote:
> I find it surprising that the meaning of a specific bit pattern as a real number according to an established floating-point standard can change from year to year. How do we know it won't change again?
>
> Larry
>
>> On 19 Nov 2025, at 22:37, Achim D. Brucker <adbrucker at 0x5f.org> wrote:
>>
>> Hi,
>> I did a first investigation. Overall, this part of the theory is intended to serve as regression test. Thus, it worked as it should: acting as early warning for subtle changes that otherwise would go undetected, potentially creating "bit rot".
>>
>> The change is actually due to a difference in Poly/ML used in Isabelle 2025 vs the current development version (and, 2025-1, for that matter). Namely:
>>
>> ML\<open>
>>      PackReal32Little.fromBytes (Word8Vector.fromList [0wxC5, 0wx10, 0wxE8, 0wx3B])
>> \<close>
>>
>> returns a different value, namely:
>>
>> * Isabelle 2025:                                  val it = 0.007082077209: PackReal32Little.real
>> * Isabelle development/2025-1:      val it = 0.007082077: PackReal32Little.real
>>
>> As the rule-of-thumb regarding the precision of 32 IEEE-745 floating point numbers is around 7-8 decimal digits, the new behaviour is OK. Hence, the fix to get the AFP entry working again is to update the theories to reflect the new values.
>> We will take care of this tomorrow.
>>
>> Best,
>> Achim (and Amy)
>>
>>
>> On 19/11/2025 16:25, Lawrence Paulson via isabelle-dev wrote:
>>> Neural_Networks is badly broken. I took a look and the failure is in a proof that tests whether a certain generated construction is equal to an explicit construction. They are supposed to be literally identical and are not. I think we should get back to the authors to find out why it failed and how it can be made robust.
>>>
>>> Larry
> _______________________________________________
> Afp-submit mailing list
> Afp-submit at mailman.proof.cit.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/afp-submit