{"id":"W4411552778","doi":"10.1109/icse55347.2025.00002","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","year":2025,"lang":"en","type":"article","venue":"","topic":"Manufacturing Process and Optimization","field":"Engineering","cited_by":4,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"Computer science; Programming language; Proof of concept; Artificial intelligence; Operating system","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0000567867,0.0001055936,0.0001133522,0.00008147014,0.00006349532,0.00005097235,0.00007694506,0.00005520978,0.00003719493],"category_scores_gemma":[0.00006282211,0.00009225329,0.00004747367,0.000160829,0.000008805735,0.00007787607,0.00001543512,0.00004603869,0.00000114241],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003355133,"about_ca_system_score_gemma":0.00001351577,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000009130274,"about_ca_topic_score_gemma":0.0000108487,"domain_scores_codex":[0.999476,0.000004392725,0.000145297,0.0001299939,0.00006030036,0.0001840846],"domain_scores_gemma":[0.9997677,0.00003534107,0.00001352763,0.0001068064,0.00004770885,0.00002898002],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001905659,0.0000332073,0.0001159656,0.0007824059,0.00005930058,6.063714e-7,0.00006293113,0.05583784,0.00009368608,0.001724405,0.0009767207,0.9402938],"study_design_scores_gemma":[0.0003700333,0.00002691852,0.001609618,0.00008726706,0.00006218947,0.000001070556,0.00006160478,0.8082574,0.1260888,0.0001436759,0.06303129,0.0002601776],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01006711,0.0001340556,0.9729759,0.0002954618,0.0004593736,0.0006368512,0.000005082938,0.0009121074,0.01451413],"genre_scores_gemma":[0.9557796,0.0000050819,0.04230668,0.00004253938,0.00003195972,0.0004266064,0.00001338961,0.00002100323,0.001373107],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9457125,"threshold_uncertainty_score":0.376198,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01102941783720241,"score_gpt":0.2347256502724876,"score_spread":0.2236962324352852,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}