{"id":"W3185895498","doi":"10.1007/978-3-030-81685-8_39","title":"Counterexample-Guided Partial Bounding for Recursive Function Synthesis","year":2021,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Recursion (computer science); Bounding overwatch; Counterexample; Computer science; μ operator; Function (biology); Primitive recursive function; Set (abstract data type); Recursive functions; Context (archaeology); Algorithm; Theoretical computer science; Mathematics; Discrete mathematics; Programming language","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.002231522,0.0005039295,0.0005817511,0.0006315995,0.0004623894,0.0009116868,0.002461348,0.0003972526,0.00003342894],"category_scores_gemma":[0.001094591,0.00050928,0.0002111126,0.000605991,0.0004900546,0.0009646482,0.0007345033,0.0005437701,0.00002299491],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006475075,"about_ca_system_score_gemma":0.0007117408,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001358956,"about_ca_topic_score_gemma":0.00002152028,"domain_scores_codex":[0.9957708,0.00009280854,0.0006901406,0.001801703,0.0009209265,0.0007236237],"domain_scores_gemma":[0.9958285,0.001325623,0.0004927437,0.001589984,0.000609464,0.0001536819],"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.00002402778,0.00002791651,0.00001252448,0.00009933509,0.00002857786,0.00001857973,0.0005319452,0.005730994,0.0006024492,0.3562684,0.00009784583,0.6365574],"study_design_scores_gemma":[0.0003570118,0.0003243274,0.00008586821,0.0009155002,0.00005223097,0.000123212,8.682759e-7,0.6959497,0.02156095,0.2613383,0.01813255,0.001159466],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00004825919,0.0002753367,0.9908153,0.0004168425,0.006263119,0.0006510075,0.00001289135,0.0001684619,0.001348721],"genre_scores_gemma":[0.01099193,0.00003593797,0.9867649,0.0008853482,0.0008970559,0.00009429432,0.0000128227,0.00004397379,0.0002737279],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6902187,"threshold_uncertainty_score":0.9997359,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06086517328587813,"score_gpt":0.3070521637342828,"score_spread":0.2461869904484047,"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."}}