{"entities":{"Q7361792":{"pageid":31520915,"ns":120,"title":"Item:Q7361792","lastrevid":105369071,"modified":"2026-10-07T13:37:41Z","type":"item","id":"Q7361792","labels":{"en":{"language":"en","value":"Formalizing Neural Networks"}},"descriptions":{"en":{"language":"en","value":"AFP entry Neural_Networks"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"51afd3133eb1857c71e594341131ae4a04cf2c82","datavalue":{"value":"https://isa-afp.org/entries/Neural_Networks.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361792$A64AE3A8-5E99-4EBA-AAEE-B67094740D92","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"14cb762659b33ccff4ce5d6bbb206b575ef06f04","datavalue":{"value":{"time":"+2025-11-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361792$851EDBB4-F61E-4A0F-91DF-E0756A0AAD76","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c321b6732f723699ff379c28a4499e7172aa303c","datavalue":{"value":"Achim D. Brucker","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361792$A96D81DF-820D-4215-9D78-DA28B891E7CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"9559dbbd5318d85971d88f8cd0c16e3a6afbc1d9","datavalue":{"value":"Amy Stell","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361792$EDD405A7-80B4-4D0F-8A3B-60845AABC426","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"68e8cc9654201b4134f1e0a6a9b5bed5fc369a35","datavalue":{"value":{"text":"Formalizing Neural Networks","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361792$CB3ED4E9-865E-4A37-A86C-D9D429579714","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1bd04a0e1169467a2e9ad96cecd721dd26a8d65e","datavalue":{"value":"Deep learning, i.e., machine learning using neural networks, is used successfully in many application areas. Still, their use in safety-critical or security-critical applications is limited, due to the lack of testing and verification techniques. We address this problem by formalizing an important class of neural networks, feed-forward neural networks, in Isabelle/HOL. We present two different approaches of formalizing feed-forward networks and show their equivalence as well as demonstrate their use in verifying certain safety and correctness properties of various example. Moreover, we do not only provide a formal model that allows to reason over feed-forward neural networks, we also provide a datatype package for Isabelle/HOL that supports importing models from TensorFlow.js.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361792$E42801F1-2A28-4F4E-B614-DCB3D5D8D45B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"94fe41a85a05383935c29ab90c4d3044c329de6e","datavalue":{"value":{"entity-type":"item","numeric-id":4569250,"id":"Q4569250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$C18E0BAB-5851-4AC7-909D-9ED9650C5D2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"793814f2ab7f0f42a058b96b574f2be914fa43ed","datavalue":{"value":{"entity-type":"item","numeric-id":6174545,"id":"Q6174545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$56B69E7B-F0EA-4447-B637-595705DE9D5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09d76610be2db7a475aae1f8e37aec5be549c297","datavalue":{"value":{"entity-type":"item","numeric-id":2151238,"id":"Q2151238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$61E85D46-CE00-4D91-872D-CFF8190C7DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d8a6a7f4a099b96912e5cba667c8ca70d007bb8","datavalue":{"value":{"entity-type":"item","numeric-id":287365,"id":"Q287365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$7F2EF876-3348-4A31-B879-1979B9D2CB3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b36457be3394709f7d33dd1e5729b9a52624062d","datavalue":{"value":{"entity-type":"item","numeric-id":1650418,"id":"Q1650418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$494FB1F8-DEEF-4832-A504-682032A8170E","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$2842F7F2-05CD-40BF-9AAF-9EFC1BF83801","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"b999678a517221bed9bd614caca8006ebca3a529","datavalue":{"value":{"entity-type":"item","numeric-id":7361796,"id":"Q7361796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$EB4DED29-8046-402A-9AD6-FDFC8F28D0BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"f1a2d99bfffe929fae2c95cf31d1b59caff32f7f","datavalue":{"value":{"entity-type":"item","numeric-id":7361791,"id":"Q7361791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$B15ABE22-5E06-4E03-9CE6-7E30AC361CD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"67e8a5ea879a7dc06c8ce830c1b61b9bb35cc48f","datavalue":{"value":{"entity-type":"item","numeric-id":7361432,"id":"Q7361432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$18DEE776-546B-4E8D-9EA0-59AA3ED860F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"64be0447c49928c088aec77cbcc3cee8daad41e8","datavalue":{"value":{"entity-type":"item","numeric-id":7361383,"id":"Q7361383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$7C3A240F-41DA-403F-9F7F-4E6974EFD38A","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ce3280e9ef2fb44c844e03b65b6366a348e2eeb2","datavalue":{"value":{"entity-type":"item","numeric-id":7360783,"id":"Q7360783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$19DABC65-C9B6-40CA-82AB-4EBD5A44FFA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ef7bddd24a035fe32f48fd95ea6033928a9b8e67","datavalue":{"value":{"entity-type":"item","numeric-id":7360788,"id":"Q7360788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$59F07DDB-09BE-4F05-BC89-241D11408C86","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361792$F821CC14-8084-4655-B4D1-4E3682904457","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing Neural Networks","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalizing_Neural_Networks"}}}}}