{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002621118,0.001612367,0.0009128624,0.002759174,0.0008092514,0.003012293,0.003147053,0.001884375,0.01008642],"category_scores_gemma":[0.02253421,0.0009198929,0.002744467,0.00173778,0.001492034,0.004465297,0.002990184,0.002848808,0.005558347],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001956194,"about_ca_system_score_gemma":0.003181631,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004552858,"about_ca_topic_score_gemma":0.01144225,"domain_scores_codex":[0.9970958,0.0009853217,0.0002491103,0.0006983453,0.0007890147,0.0001823396],"domain_scores_gemma":[0.9898427,0.006463756,0.0005112847,0.002072566,0.0009847755,0.0001249281],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"not_applicable","study_design_scores_codex":[0.000649703,0.0003858272,0.005129841,0.003830572,0.000330502,0.0004244649,0.000469115,0.1938725,0.01991807,0.06466071,0.04409508,0.6662337],"study_design_scores_gemma":[0.0001324119,0.0001433998,0.0006879123,0.0003385668,0.0000831213,0.000236395,0.0001405499,0.8437716,0.01626837,0.09736533,0.0407934,0.00003896114],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"other","genre_scores_codex":[0.03082847,0.003351238,0.8919061,0.001611055,0.0003641692,0.000426221,0.00637129,0.05296467,0.01217671],"genre_scores_gemma":[0.1620394,0.001345561,0.8111043,0.0008107411,0.0001157052,0.0005458299,0.01682391,0.003151238,0.004063328],"genre_candidate":"other","genre_consensus":null,"teacher_disagreement_score":0.01008642,"threshold_uncertainty_score":0.03374243,"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."}}