Infer a implementation of a blackbox function given table

Stream: Program verification

[Joh-Tob Schäg]

I have a 32bit->32bit function blackbox piece of silicon which computer an approximate inverse square root on single precision floats. What tooling would be suitable for finding a more compact representation of that function using bit level operations?
Would you expect that that tooling to also be able to do the same for black box functions which implement repricals, square roots operating on doubles (64-bit)?
Full enumeration of 64 bit is out of question. But checking out the difference between competing implementations and looking which one is right could be helpful.
(I tried to find literature but my keywords resulted in mostly "can we trust AI?" papers.

[Eric Wieser]

If this is a black box piece of silicon I'm not sure you have any reason to assume that it builds the operation out of components that are IEEE754 operations

[Eric Wieser]

or by bit-level operations are you excluding arithmetic?

[Joh-Tob Schäg]

I have no reason to assume it's made out of purely out of IEE754 compliant components. I said bit level because i assume this circuit has no analog components so what ever it does must operate on bits, it can include arithmetic and the hardware unit that does that opeation has access to an FMA floating point unit.
In particular i am dealing with https://sxauroratsubasa.sakura.ne.jp/documents/guide/pdfs/Aurora_ISA_guide.pdf#%5B%7B%22num%22%3A726%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C155%2C705%2C0%5D which describes the exact behaviour as implementation defined ;-P so that's not helpful.
I just did the math and came to the realisation that 32bits*2^32 fits in RAM and on disk so i could dump the whole thing for 32bits.

[Eric Wieser]

I'm not sure how on-topic this is for this Zulip: certainly to verify a program that uses external hardware you need an accurate model of that hardware. but the process of building that model by reverse-engineering seems like a question for another forum. Perhaps https://reverseengineering.stackexchange.com/?

[Eric Wieser]

Of course another answer would be "use the exhaustive evaluation to find the maximum (relative) error", and then use interval arithmetic for verification purposes; rr slightly more generally, plot the absolute error and find a pair of functions that loosely bound it above and below.

[Joh-Tob Schäg]

My mental was doing program synthesis against a 16GiBs look up table (or a super sparse exabyte sized lookup table). "reverse engineering" seems to be a promising search term. I immeadetly found a paper like https://publications.cispa.saarland/3147/1/ireen_reverse_engineering_of_black_box_functions_via_iterative_neural_program_synthesis.pdf which seems a lot more promising then the papers i found before.

[Joh-Tob Schäg]

Question asked. If there is any input from the program synthesis side i welcome suggestions.

[Eric Wieser]

Have you considered contacting the manufacturer and explaining you would like to know the algorithm for verification purposes? I would assume their IP is primarily in the hardware optimization, not the algorithm itself

[Joh-Tob Schäg]

I have limited social capital with them as i got that component used and don't have a support contract with them. Also it is a neat project that is manageable on my own and i'd like to not go in blindly into that project.