{"id":"0ef31f61-a365-4d3a-b985-4d482206fae8","arxiv_id":"2504.12031","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper defines proof-carrying neuro-symbolic code, a research program for delivering neural-network-containing software with formal safety proofs, and reviews early tools and challenges.","lead":"An invited paper introduces 'proof-carrying neuro-symbolic code', a framework for verifying programs that mix neural networks with traditional code, and argues the approach is meaningful and valuable. It surveys the first tools built in this direction and lists three open challenges.","discovery_kind":"review","skeptic_critique":null,"referee_report":null,"author_rebuttal":null,"desk_editor":null,"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-16T12:39:46.441673+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}