{"id":"W4281873108","doi":"10.1145/3519939.3523726","title":"Recursion synthesis with unrealizability witnesses","year":2022,"lang":"en","type":"article","venue":"","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":18,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Recursion (computer science); Computer science; Counterexample; Set (abstract data type); Program synthesis; Function (biology); Theoretical computer science; Witness; Recursive functions; Algorithm; Programming language; Mathematics; Discrete mathematics","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.002392053,0.0009110186,0.0005952422,0.0008502148,0.0006395921,0.002158775,0.002105602,0.001194312,0.006222233],"category_scores_gemma":[0.01092073,0.0006216769,0.001481743,0.000494341,0.003109387,0.003496485,0.003256385,0.002316556,0.001134251],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001128543,"about_ca_system_score_gemma":0.00194294,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001002046,"about_ca_topic_score_gemma":0.001793633,"domain_scores_codex":[0.9978278,0.0005097788,0.0001366887,0.00044498,0.0008201823,0.0002605685],"domain_scores_gemma":[0.9954554,0.00257776,0.0002303912,0.00114525,0.0004935223,0.00009767451],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0002056452,0.0001286134,0.00137902,0.0004678986,0.00005822004,0.0005253441,0.0007069436,0.07041227,0.0314927,0.7751011,0.002648422,0.1168738],"study_design_scores_gemma":[0.0001077538,0.0001854338,0.0001802392,0.0001507524,0.00009238523,0.0003383404,0.0001978455,0.3913395,0.09266739,0.483147,0.0315349,0.00005836474],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0162274,0.0001061037,0.9741441,0.0002579924,0.00006547007,0.00007844937,0.00008895985,0.002715887,0.006315713],"genre_scores_gemma":[0.3374894,0.0002384437,0.6547068,0.000326861,0.00005094292,0.0002554675,0.0003942915,0.001165796,0.005372043],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006222233,"threshold_uncertainty_score":0.02081537,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0203566923973015,"score_gpt":0.2329297441961982,"score_spread":0.2125730517988967,"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."}}