\u4f5c\u8005\uff1aAnjiang Wei, Tianran Sun, Tarun Suresh, Haoze Wu, Ke Wang, Alex <\/p>\n\n\n\n
\u5355\u4f4d\uff1a Stanford University\uff1bShanghai Jiao Tong University\uff1bUniversity of Illinois Urbana-Champaign\uff1bAmherst College\uff1bNanjing UniversityIntelligence \u7b49<\/p>\n\n\n\n
\u6765\u6e90\uff1a ICLR 2026 Workshop VerifAI-2<\/p>\n\n\n\n
\u65f6\u95f4\uff1a2026.04.02<\/p>\n\n\n\n
\u94fe\u63a5\uff1a[<\/a><\/u>Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis<\/a>]<\/a><\/u><\/p>\n\n\n\n \u7a0b\u5e8f\u9a8c\u8bc1\u7684\u76ee\u6807\u662f\u4e3a\u8f6f\u4ef6\u884c\u4e3a\u63d0\u4f9b\u5f62\u5f0f\u5316\u4fdd\u8bc1\uff0c\u5c24\u5176\u9002\u7528\u4e8e\u81ea\u52a8\u9a7e\u9a76\u3001\u822a\u7a7a\u822a\u5929\u3001\u5de5\u4e1a\u63a7\u5236\u3001\u91d1\u878d\u7cfb\u7edf\u7b49\u5b89\u5168\u5173\u952e\u573a\u666f\u3002\u76f8\u6bd4\u666e\u901a\u6d4b\u8bd5\uff0c\u7a0b\u5e8f\u9a8c\u8bc1\u5e0c\u671b\u8bc1\u660e\u7a0b\u5e8f\u5728\u6240\u6709\u53ef\u80fd\u8f93\u5165\u548c\u6267\u884c\u8def\u5f84\u4e0b\u90fd\u6ee1\u8db3\u6307\u5b9a\u6027\u8d28\uff0c\u800c\u4e0d\u662f\u53ea\u5728\u6709\u9650\u6d4b\u8bd5\u6837\u4f8b\u4e0a\u8868\u73b0\u6b63\u786e\u3002<\/p>\n\n\n\n \u4f46\u7a0b\u5e8f\u4e2d\u4e00\u65e6\u51fa\u73b0\u5faa\u73af\u7ed3\u6784\uff0c\u9a8c\u8bc1\u95ee\u9898\u5c31\u4f1a\u663e\u8457\u590d\u6742\u5316\u3002\u5faa\u73af\u53ef\u80fd\u6267\u884c\u4efb\u610f\u6b21\u6570\uff0c\u5e26\u6765\u6f5c\u5728\u65e0\u9650\u72b6\u6001\u7a7a\u95f4\u3002\u4e3a\u4e86\u8bc1\u660e\u5faa\u73af\u7a0b\u5e8f\u7684\u6b63\u786e\u6027\uff0c\u9a8c\u8bc1\u5668\u901a\u5e38\u9700\u8981\u4f9d\u8d56\u5faa\u73af\u4e0d\u53d8\u91cf\u3002<\/p>\n\n\n\n \u6240\u8c13\u5faa\u73af\u4e0d\u53d8\u91cf\uff0c\u662f\u6307\u5728\u5faa\u73af\u5f00\u59cb\u524d\u6210\u7acb\u3001\u6bcf\u6b21\u5faa\u73af\u8fed\u4ee3\u540e\u4ecd\u7136\u6210\u7acb\uff0c\u5e76\u4e14\u5728\u5faa\u73af\u9000\u51fa\u65f6\u80fd\u591f\u63a8\u51fa\u76ee\u6807\u65ad\u8a00\u7684\u903b\u8f91\u6761\u4ef6\u3002\u4f8b\u5982\uff0c\u4e00\u4e2a\u53d8\u91cf\u6bcf\u6b21\u5faa\u73af\u90fd\u52a0 7\uff0c\u5982\u679c\u521d\u503c\u4e3a 10\uff0c\u90a3\u4e48 x % 7 == 3 \u53ef\u80fd\u5c31\u662f\u4e00\u4e2a\u975e\u5e38\u5173\u952e\u7684\u4e0d\u53d8\u91cf\u3002\u5b83\u4e0d\u4ec5\u63cf\u8ff0\u4e86\u5faa\u73af\u8fc7\u7a0b\u4e2d\u53d8\u91cf\u7684\u7ed3\u6784\u6027\u89c4\u5f8b\uff0c\u8fd8\u53ef\u4ee5\u5e2e\u52a9\u9a8c\u8bc1\u5668\u6392\u9664\u67d0\u4e9b\u9519\u8bef\u72b6\u6001\u3002<\/p>\n\n\n\n \u4e0d\u8fc7\uff0c\u751f\u6210\u5faa\u73af\u4e0d\u53d8\u91cf\u5e76\u4e0d\u5bb9\u6613\u3002\u4e00\u4e2a\u4e0d\u53d8\u91cf\u4ec5\u4ec5\u6b63\u786e\u8fd8\u4e0d\u591f\uff0c\u8fd8\u5fc5\u987b\u8db3\u591f\u5f3a\u3002\u4f8b\u5982 x > 0 \u53ef\u80fd\u59cb\u7ec8\u6210\u7acb\uff0c\u4f46\u5b83\u65e0\u6cd5\u5e2e\u52a9\u8bc1\u660e x != 700\uff1b\u800c x % 7 == 3 \u4e0d\u4ec5\u6b63\u786e\uff0c\u8fd8\u80fd\u76f4\u63a5\u6392\u9664 x == 700\uff0c\u56e0\u6b64\u66f4\u6709\u5b9e\u9645\u8bc1\u660e\u4ef7\u503c\u3002<\/p>\n\n\n\n \u672c\u6587\u5173\u6ce8\u7684\u95ee\u9898\u662f\uff1aLLM \u662f\u5426\u80fd\u591f\u901a\u8fc7\u751f\u6210\u6709\u7528\u7684\u5faa\u73af\u4e0d\u53d8\u91cf\u6765\u52a0\u901f\u7a0b\u5e8f\u9a8c\u8bc1\uff1f\u8fdb\u4e00\u6b65\u8bf4\uff0c\u5982\u4f55\u628a LLM \u7684\u4ee3\u7801\u7406\u89e3\u548c\u903b\u8f91\u63a8\u7406\u80fd\u529b\u8f6c\u5316\u4e3a\u53ef\u4fe1\u7684\u7a0b\u5e8f\u9a8c\u8bc1\u80fd\u529b\uff1f<\/p>\n\n\n\n \u8bba\u6587\u56f4\u7ed5 LLM-based invariant synthesis \u5c55\u5f00\uff0c\u63d0\u51fa Quokka \u4f5c\u4e3a\u4e00\u4e2a\u9762\u5411\u8bc4\u4f30\u7684 LLM \u4e0d\u53d8\u91cf\u751f\u6210\u6846\u67b6\u3002\u672c\u6587\u7684\u6838\u5fc3\u8d21\u732e\u4e3b\u8981\u5305\u62ec\u56db\u70b9\uff1a<\/p>\n\n\n\n \u672c\u6587\u4e0e\u4e4b\u524d\u5de5\u4f5c\u7684\u6700\u5927\u4e0d\u540c\u5728\u4e8e\uff0c\u5b83\u76f4\u63a5\u628a LLM \u8f93\u51fa\u4f5c\u4e3a\u5f85\u9a8c\u8bc1\u7684\u8bc1\u660e\u5019\u9009\u3002Quokka \u5e76\u4e0d\u4fe1\u4efb LLM \u7684\u81ea\u7136\u8bed\u8a00\u63a8\u7406\u7ed3\u679c\uff0c\u800c\u662f\u628a LLM \u653e\u5728\u751f\u6210\u5019\u9009\u547d\u9898\u7684\u4f4d\u7f6e\uff0c\u518d\u7531\u5f62\u5f0f\u5316\u9a8c\u8bc1\u5668\u5b8c\u6210\u53ef\u9760\u6027\u5224\u65ad\u3002<\/p>\n\n\n\n \u8fd9\u4e0e\u98df\u54c1\u63a8\u7406\u4efb\u52a1\u975e\u5e38\u76f8\u4f3c\uff1aLLM \u53ef\u4ee5\u63d0\u51fa\u67d0\u7c7b\u914d\u6599\u5360\u6bd4\u5e94\u6ee1\u8db3\u67d0\u4e2a\u7ea6\u675f\u3001\u67d0\u7c7b\u98df\u54c1\u7684\u8425\u517b\u8d21\u732e\u5e94\u7b26\u5408\u67d0\u79cd\u89c4\u5f8b\u7b49\u5019\u9009\u547d\u9898\uff0c\u4f46\u8fd9\u4e9b\u547d\u9898\u4e0d\u80fd\u76f4\u63a5\u5165\u5e93\uff0c\u5fc5\u987b\u7ecf\u8fc7\u7ea6\u675f\u6c42\u89e3\u3001\u8bef\u5dee\u8bc4\u4f30\u548c\u51b2\u7a81\u68c0\u6d4b\u3002<\/p>\n\n\n\n \u672c\u6587\u7684\u6838\u5fc3\u601d\u60f3\u53ef\u4ee5\u6982\u62ec\u4e3a\uff1aLLM \u662f\u5019\u9009\u903b\u8f91\u547d\u9898\u751f\u6210\u5668\uff1b\u9a8c\u8bc1\u5668\u662f\u53ef\u4fe1\u8bc4\u4ef7\u5668\u3002<\/p>\n\n\n\n \u4f20\u7edf LLM-based verifier \u5f80\u5f80\u91c7\u7528\u590d\u6742\u7684\u201c\u751f\u6210\u2014\u8fc7\u6ee4\u2014\u91cd\u7ec4\u2014\u4fee\u590d\u201d\u7b56\u7565\u3002\u6bd4\u5982\u8ba9 LLM \u5148\u751f\u6210\u4e00\u6279\u8c13\u8bcd\uff0c\u518d\u7528\u6a21\u578b\u68c0\u67e5\u5668\u8fc7\u6ee4\u65e0\u6548\u8c13\u8bcd\uff0c\u4e4b\u540e\u901a\u8fc7\u5408\u53d6\u3001\u6790\u53d6\u3001Houdini pruning \u6216\u56de\u6eaf\u7b97\u6cd5\u62fc\u63a5\u51fa\u6700\u7ec8\u4e0d\u53d8\u91cf\u3002\u8fd9\u7c7b\u65b9\u6cd5\u7684\u6f5c\u53f0\u8bcd\u662f\uff1aLLM \u8f93\u51fa\u662f\u4e0d\u53ef\u9760\u7684\uff0c\u9700\u8981\u590d\u6742\u7b97\u6cd5\u4e0d\u65ad\u8865\u6551\u3002<\/p>\n\n\n\n Quokka \u7684\u601d\u8def\u66f4\u76f4\u63a5\uff1a\u5982\u679c LLM \u751f\u6210\u4e86\u4e00\u4e2a\u5019\u9009\u4e0d\u53d8\u91cf\uff0c\u90a3\u4e48\u5c31\u76f4\u63a5\u4ea4\u7ed9\u9a8c\u8bc1\u5668\u5224\u65ad\u5b83\u662f\u5426\u6210\u7acb\u3001\u662f\u5426\u6709\u7528\u3002\u82e5\u5b83\u6b63\u786e\u4e14\u80fd\u5e2e\u52a9\u8bc1\u660e\u76ee\u6807\u65ad\u8a00\uff0c\u5c31\u4fdd\u7559\u5176\u8d21\u732e\uff1b\u82e5\u5b83\u4e0d\u6b63\u786e\u6216\u65e0\u7528\uff0c\u5c31\u4e22\u5f03\u6216\u5224\u4e3a inconclusive\u3002<\/p>\n\n\n\n \u8fd9\u4f53\u73b0\u4e86\u4e00\u4e2a\u5f88\u91cd\u8981\u7684\u7cfb\u7edf\u8bbe\u8ba1\u601d\u60f3\uff1a\u4e0d\u8981\u8ba9 LLM \u76f4\u63a5\u7ed9\u51fa\u6700\u7ec8\u53ef\u4fe1\u7ed3\u8bba\uff0c\u800c\u8981\u8ba9 LLM \u751f\u6210\u5019\u9009\u7ed3\u6784\uff0c\u518d\u7528\u53ef\u9a8c\u8bc1\u673a\u5236\u7b5b\u9009\u3002<\/p>\n\n\n\n \u5728\u7a0b\u5e8f\u9a8c\u8bc1\u4e2d\uff0c\u8fd9\u4e2a\u5019\u9009\u7ed3\u6784\u662f\u4e0d\u53d8\u91cf\uff1b\u5728\u98df\u54c1\u6807\u7b7e\u63a8\u7406\u4e2d\uff0c\u8fd9\u4e2a\u5019\u9009\u7ed3\u6784\u53ef\u4ee5\u662f\u914d\u6599\u6bd4\u4f8b\u7ea6\u675f\u3001\u8425\u517b\u8d21\u732e\u7ea6\u675f\u3001\u7c7b\u522b\u5148\u9a8c\u7ea6\u675f\u3001\u4ef7\u683c\u5408\u7406\u6027\u7ea6\u675f\u6216\u6cd5\u89c4\u5408\u89c4\u7ea6\u675f\u3002<\/p>\n\n\n\n \u56e0\u6b64\uff0cQuokka \u7684\u4ef7\u503c\u4e0d\u53ea\u662f\u7a0b\u5e8f\u9a8c\u8bc1\u672c\u8eab\uff0c\u800c\u662f\u63d0\u4f9b\u4e86\u4e00\u79cd\u201cLLM + \u5f62\u5f0f\u5316\u9a8c\u8bc1\u5668\u201d\u7684\u901a\u7528\u534f\u540c\u8303\u5f0f\u3002<\/p>\n\n\n\n \u8bba\u6587\u9996\u5148\u7528 Hoare Logic \u63cf\u8ff0\u5faa\u73af\u4e0d\u53d8\u91cf\u7684\u4f5c\u7528\u3002<\/p>\n\n\n\n \u5bf9\u4e8e\u4e00\u4e2a\u5faa\u73af\uff1a<\/p>\n\n\n\n while B do S<\/p>\n\n\n\n \u5176\u4e2d P \u662f\u524d\u7f6e\u6761\u4ef6\uff0cQ \u662f\u540e\u7f6e\u6761\u4ef6\uff0cB \u662f\u5faa\u73af\u6761\u4ef6\uff0cS \u662f\u5faa\u73af\u4f53\u3002\u8981\u8bc1\u660e\u7a0b\u5e8f\u4ece P \u51fa\u53d1\u6267\u884c\u5faa\u73af\u540e\u6ee1\u8db3 Q\uff0c\u5c31\u9700\u8981\u627e\u5230\u4e00\u4e2a\u5faa\u73af\u4e0d\u53d8\u91cf I\uff0c\u4f7f\u5176\u6ee1\u8db3\u4e09\u4e2a\u6761\u4ef6\uff1a<\/p>\n\n\n\n \u53ea\u6709\u540c\u65f6\u6ee1\u8db3\u8fd9\u4e09\u4e2a\u6761\u4ef6\uff0cI \u624d\u80fd\u4f5c\u4e3a\u8bc1\u660e\u5faa\u73af\u6b63\u786e\u6027\u7684\u5f52\u7eb3\u5f0f\u903b\u8f91\u6865\u6881\u3002<\/p>\n\n\n\n \u8fd9\u91cc\u9700\u8981\u6ce8\u610f\u7684\u662f\uff1a\u6b63\u786e\u4e0d\u53d8\u91cf\u4e0d\u4e00\u5b9a\u6709\u7528\u3002<\/p>\n\n\n\n \u4f8b\u5982\uff0c\u5bf9\u4e8e\u67d0\u4e2a\u7a0b\u5e8f\u800c\u8a00\uff0cx > 0 \u53ef\u80fd\u786e\u5b9e\u59cb\u7ec8\u6210\u7acb\uff0c\u4f46\u5b83\u53ef\u80fd\u65e0\u6cd5\u5e2e\u52a9\u8bc1\u660e\u6700\u7ec8\u65ad\u8a00\u3002\u800c x % 7 == 3 \u8fd9\u6837\u7684\u4e0d\u53d8\u91cf\u867d\u7136\u66f4\u5177\u4f53\uff0c\u5374\u80fd\u663e\u8457\u7f29\u5c0f\u72b6\u6001\u7a7a\u95f4\uff0c\u76f4\u63a5\u5e2e\u52a9\u9a8c\u8bc1\u5668\u6392\u9664\u9519\u8bef\u72b6\u6001\u3002<\/p>\n\n\n\n \u56e0\u6b64\uff0cQuokka \u7684\u8bc4\u4ef7\u6807\u51c6\u4e0d\u662f\u201cLLM \u662f\u5426\u751f\u6210\u4e86\u6b63\u786e\u4e0d\u53d8\u91cf\u201d\uff0c\u800c\u662f\u8fdb\u4e00\u6b65\u8ffd\u95ee\uff1a<\/p>\n\n\n\n \u8fd9\u4e2a\u4e0d\u53d8\u91cf\u662f\u5426\u5f3a\u5230\u8db3\u4ee5\u52a0\u901f\u76ee\u6807\u6027\u8d28\u7684\u8bc1\u660e\uff1f<\/p>\n\n\n\n Quokka \u7684\u6838\u5fc3\u65b9\u6cd5\u662f\u5bf9\u6bcf\u4e2a\u5019\u9009\u4e0d\u53d8\u91cf\u6267\u884c\u4e24\u4e2a\u9a8c\u8bc1\u5668\u67e5\u8be2\u3002<\/p>\n\n\n\n \u7ed9\u5b9a\uff1a<\/p>\n\n\n\n P\uff1a\u539f\u59cb\u7a0b\u5e8f \u7b2c\u4e00\u4e2a\u67e5\u8be2\u662f\uff1a<\/p>\n\n\n\n da = V(P, \u2205, q)<\/p>\n\n\n\n \u5b83\u7684\u4f5c\u7528\u662f\u9a8c\u8bc1 q \u662f\u5426\u771f\u7684\u662f\u7a0b\u5e8f P \u4e2d\u6210\u7acb\u7684\u4e0d\u53d8\u91cf\u3002\u4e5f\u5c31\u662f\u8bf4\uff0cq \u672c\u8eab\u5fc5\u987b\u5148\u88ab\u8bc1\u660e\u4e3a\u6b63\u786e\u3002<\/p>\n\n\n\n \u7b2c\u4e8c\u4e2a\u67e5\u8be2\u662f\uff1a<\/p>\n\n\n\n db = V(P, {q}, p*)<\/p>\n\n\n\n \u5b83\u7684\u4f5c\u7528\u662f\u5728\u5047\u8bbe q \u6210\u7acb\u7684\u60c5\u51b5\u4e0b\uff0c\u9a8c\u8bc1\u76ee\u6807\u6027\u8d28 p* \u662f\u5426\u53ef\u4ee5\u88ab\u8bc1\u660e\u3002\u4e5f\u5c31\u662f\u8bf4\uff0cq \u4e0d\u4ec5\u8981\u6b63\u786e\uff0c\u8fd8\u8981\u5bf9\u6700\u7ec8\u8bc1\u660e\u6709\u5e2e\u52a9\u3002<\/p>\n\n\n\n \u5982\u679c q \u88ab\u8bc1\u660e\u6210\u7acb\uff0c\u5e76\u4e14\u52a0\u5165 q \u540e\u76ee\u6807\u6027\u8d28\u4e5f\u88ab\u8bc1\u660e\uff0c\u90a3\u4e48 Quokka \u8f93\u51fa T\uff0c\u8868\u793a\u8bc1\u660e\u6210\u529f\u3002 \u8fd9\u4e00\u673a\u5236\u7684\u5173\u952e\u5728\u4e8e\uff1aLLM \u8f93\u51fa\u4e0d\u4f1a\u88ab\u76f4\u63a5\u5f53\u6210\u4e8b\u5b9e\uff0c\u800c\u662f\u88ab\u5f53\u6210\u5f85\u9a8c\u8bc1\u7684\u8bc1\u660e\u5019\u9009\u3002\u7cfb\u7edf\u7684 soundness \u6765\u81ea\u9a8c\u8bc1\u5668\uff0c\u800c\u4e0d\u662f\u6765\u81ea LLM\u3002<\/p>\n\n\n\n \u5728\u771f\u6b63\u8c03\u7528\u9a8c\u8bc1\u5668\u524d\uff0cQuokka \u4f1a\u5148\u505a\u8bed\u6cd5\u5408\u6cd5\u6027\u68c0\u67e5\u3002\u56e0\u4e3a LLM \u53ef\u80fd\u751f\u6210\u975e\u6cd5\u8868\u8fbe\u5f0f\uff0c\u751a\u81f3\u751f\u6210\u4f1a\u6539\u53d8\u7a0b\u5e8f\u72b6\u6001\u7684\u8bed\u53e5\uff0c\u4f8b\u5982 a += 1\u3001x++\u3001\u8d4b\u503c\u8868\u8fbe\u5f0f\u7b49\u3002<\/p>\n\n\n\n Quokka \u53ea\u63a5\u53d7\u4e0d\u4f1a\u6539\u53d8\u7a0b\u5e8f\u72b6\u6001\u7684\u5e03\u5c14\u6761\u4ef6\u4f5c\u4e3a\u5019\u9009\u4e0d\u53d8\u91cf\u3002\u8fd9\u4e00\u6b65\u53ef\u4ee5\u907f\u514d\u628a\u975e\u903b\u8f91\u8c13\u8bcd\u9519\u8bef\u5730\u63d2\u5165\u7a0b\u5e8f\u4e2d\uff0c\u5bfc\u81f4\u9a8c\u8bc1\u7ed3\u679c\u5931\u771f\u3002<\/p>\n\n\n\n \u5728\u5b9e\u73b0\u4e0a\uff0cQuokka \u5bf9\u6bcf\u4e2a\u5019\u9009\u4e0d\u53d8\u91cf\u5e76\u884c\u6267\u884c\u4e24\u4e2a\u9a8c\u8bc1\u5668\u67e5\u8be2\u3002\u8fd9\u6837\u53ef\u4ee5\u964d\u4f4e\u6574\u4f53\u7b49\u5f85\u65f6\u95f4\uff0c\u4e5f\u65b9\u4fbf\u6d4b\u91cf\u52a0\u5165\u5019\u9009\u4e0d\u53d8\u91cf\u540e\u662f\u5426\u771f\u6b63\u5e26\u6765\u52a0\u901f\u3002<\/p>\n\n\n\n \u8fd9\u70b9\u5bf9\u6211\u4eec\u7684\u7814\u7a76\u4e5f\u6709\u542f\u53d1\uff1a\u98df\u54c1\u547d\u9898\u5e93\u4e2d\u7684\u5019\u9009\u547d\u9898\u4e5f\u5e94\u5148\u7ecf\u8fc7\u8bed\u6cd5\u4e0e\u8bed\u4e49\u68c0\u67e5\u3002\u4f8b\u5982\uff1a<\/p>\n\n\n\n \u201c\u767d\u7802\u7cd6\u5360\u6bd4\u5c0f\u4e8e 10%\u201d\u662f\u4e00\u4e2a\u53ef\u9a8c\u8bc1\u547d\u9898\uff1b \u9664\u4e86\u76f4\u63a5\u8bc4\u4f30\u4e0d\u540c LLM \u7684\u4e0d\u53d8\u91cf\u751f\u6210\u80fd\u529b\uff0c\u8bba\u6587\u8fd8\u7814\u7a76\u4e86\u4e24\u79cd\u80fd\u529b\u589e\u5f3a\u7b56\u7565\u3002<\/p>\n\n\n\n \u7b2c\u4e00\u79cd\u662f supervised fine-tuning\u3002\u4f5c\u8005\u4f7f\u7528 GPT-4o \u751f\u6210\u5408\u6210 C \u7a0b\u5e8f\uff0c\u518d\u901a\u8fc7 UAutomizer \u8fc7\u6ee4\u65e0\u6548\u6837\u672c\u5e76\u62bd\u53d6\u771f\u5b9e\u4e0d\u53d8\u91cf\uff0c\u6700\u7ec8\u5f97\u5230 3589 \u4e2a\u8bad\u7ec3\u5b9e\u4f8b\u3002\u968f\u540e\uff0c\u4f5c\u8005\u5bf9 Qwen2.5-7B \u8fdb\u884c LoRA \u5fae\u8c03\u3002<\/p>\n\n\n\n \u5b9e\u9a8c\u7ed3\u679c\u663e\u793a\uff0c\u5fae\u8c03\u5e26\u6765\u4e86\u4e00\u5b9a\u63d0\u5347\uff0c\u4f46\u5e45\u5ea6\u5e76\u4e0d\u5927\u3002\u6b63\u786e\u4e0d\u53d8\u91cf\u6570\u91cf\u4ece 419 \u63d0\u5347\u5230 431\uff0c60s timeout \u4e0b\u989d\u5916\u89e3\u51b3\u5b9e\u4f8b\u4ece 5 \u4e2a\u63d0\u5347\u5230 7 \u4e2a\u3002\u8fd9\u8bf4\u660e\u9886\u57df\u5fae\u8c03\u786e\u5b9e\u6709\u5e2e\u52a9\uff0c\u4f46\u4ec5\u9760\u76d1\u7763\u5fae\u8c03\u8fd8\u4e0d\u8db3\u4ee5\u89e3\u51b3\u6df1\u5c42\u7a0b\u5e8f\u5f52\u7eb3\u63a8\u7406\u95ee\u9898\u3002<\/p>\n\n\n\n \u7b2c\u4e8c\u79cd\u662f Best-of-N Sampling\u3002\u5b83\u7684\u601d\u8def\u662f\u8ba9 LLM \u4e00\u6b21\u751f\u6210\u591a\u4e2a\u5019\u9009\u4e0d\u53d8\u91cf\uff0c\u7136\u540e\u7531\u9a8c\u8bc1\u5668\u9009\u62e9\u5e26\u6765\u6700\u5927\u9a8c\u8bc1\u52a0\u901f\u7684\u5019\u9009\u3002\u5b9e\u9a8c\u663e\u793a\uff0c\u5f53 N \u4ece 1 \u589e\u52a0\u5230 4 \u65f6\uff0c\u6027\u80fd\u660e\u663e\u63d0\u5347\uff1b\u7ee7\u7eed\u589e\u52a0\u5230 N=8 \u65f6\u6548\u679c\u6700\u597d\uff1b\u8d85\u8fc7 N=8 \u540e\uff0c\u7531\u4e8e\u8d44\u6e90\u7ade\u4e89\u548c\u5185\u5b58\u9650\u5236\uff0c\u6536\u76ca\u8d8b\u4e8e\u5e73\u53f0\u3002<\/p>\n\n\n\n \u8fd9\u4e00\u70b9\u975e\u5e38\u9002\u5408\u8fc1\u79fb\u5230\u98df\u54c1\u547d\u9898\u5e93\u573a\u666f\u3002\u6211\u4eec\u4e5f\u53ef\u4ee5\u8ba9 LLM \u4e00\u6b21\u751f\u6210\u591a\u4e2a\u5019\u9009\u98df\u54c1\u63a8\u7406\u547d\u9898\uff0c\u7136\u540e\u901a\u8fc7\u7ea6\u675f\u6c42\u89e3\u5668\u5224\u65ad\u54ea\u6761\u547d\u9898\u6700\u80fd\u964d\u4f4e\u53cd\u6f14\u8bef\u5dee\u3001\u7f29\u5c0f\u89e3\u7a7a\u95f4\u3001\u63d0\u5347\u8bc4\u5206\u7a33\u5b9a\u6027\u3002\u6700\u7ec8\u4e0d\u662f\u8ba9\u6a21\u578b\u81ea\u5df1\u51b3\u5b9a\u54ea\u6761\u89c4\u5219\u597d\uff0c\u800c\u662f\u8ba9\u4efb\u52a1\u53cd\u9988\u51b3\u5b9a\u54ea\u6761\u89c4\u5219\u5165\u5e93\u3002<\/p>\n\n\n\n \u672c\u6587\u7684\u8bc4\u6d4b\u6570\u636e\u6765\u81ea SV-COMP 2025\u3002\u4f5c\u8005\u7b5b\u9009\u51fa\u5305\u542b while \u6216 for \u5faa\u73af\u7684\u7a0b\u5e8f\u9a8c\u8bc1\u4efb\u52a1\uff0c\u6784\u5efa\u4e86 866 \u4e2a\u8bc4\u6d4b\u5b9e\u4f8b\u3002\u76f8\u6bd4\u5df2\u6709 LLM-based verifier \u7684\u6570\u636e\u96c6\uff0cQuokka \u7684 benchmark \u66f4\u590d\u6742\uff1a\u7a0b\u5e8f\u5e73\u5747\u884c\u6570\u66f4\u957f\uff0c\u5e76\u4e14\u5305\u542b\u591a\u5faa\u73af\u3001\u591a\u51fd\u6570\u3001\u6570\u7ec4\u548c\u6307\u9488\u7b49\u7ed3\u6784\u3002\u8fd9\u4e9b\u7279\u5f81\u5728\u771f\u5b9e\u7a0b\u5e8f\u9a8c\u8bc1\u4e2d\u975e\u5e38\u91cd\u8981\uff0c\u4e5f\u66f4\u80fd\u533a\u5206\u4e0d\u540c\u6a21\u578b\u7684\u80fd\u529b\u3002<\/p>\n\n\n\n \u57fa\u7840\u9a8c\u8bc1\u5668\u65b9\u9762\uff0c\u8bba\u6587\u4f7f\u7528 UAutomizer \u4f5c\u4e3a base solver\u3002\u6bd4\u8f83\u4e24\u79cd\u60c5\u51b5\uff1a<\/p>\n\n\n\n \u8bc4\u4ef7\u6307\u6807\u5305\u62ec\uff1a<\/p>\n\n\n\n \u7279\u522b\u6ce8\u610f\u7684\u662f\uff0c\u8bba\u6587\u7edf\u8ba1\u7684\u662f\u7aef\u5230\u7aef\u65f6\u95f4\uff0c\u4e5f\u5c31\u662f\u5305\u542b LLM \u63a8\u7406\u5f00\u9500\u3002\u8fd9\u8ba9\u7ed3\u679c\u66f4\u63a5\u8fd1\u771f\u5b9e\u7cfb\u7edf\u90e8\u7f72\u573a\u666f\uff0c\u800c\u4e0d\u662f\u53ea\u770b\u9a8c\u8bc1\u5668\u5185\u90e8\u65f6\u95f4\u3002<\/p>\n\n\n\n \u8bba\u6587\u8bc4\u4f30\u4e86 9 \u4e2a LLM\uff0c\u7ed3\u679c\u663e\u793a\u6a21\u578b\u4e4b\u95f4\u5dee\u5f02\u975e\u5e38\u660e\u663e\u3002\u6574\u4f53\u8d8b\u52bf\u662f\uff1a\u6a21\u578b\u8d8a\u5f3a\uff0c\u751f\u6210\u6b63\u786e\u4e14\u6709\u7528\u4e0d\u53d8\u91cf\u7684\u80fd\u529b\u8d8a\u5f3a\u3002<\/p>\n\n\n\n \u4ece Llama-3.1-8B \u5230 gpt-5.2\uff0c\u6b63\u786e\u4e0d\u53d8\u91cf\u6570\u91cf\u4ece 342 \u63d0\u5347\u5230 710\uff0c\u5e73\u5747\u6c42\u89e3\u65f6\u95f4\u4e5f\u660e\u663e\u4e0b\u964d\u3002 \u8fd9\u8bf4\u660e Quokka \u662f\u4e00\u4e2a\u80fd\u591f\u533a\u5206\u6a21\u578b\u903b\u8f91\u63a8\u7406\u80fd\u529b\u7684 benchmark\u3002\u5b83\u65e2\u80fd\u5c55\u793a\u5f53\u524d LLM \u7684\u5b9e\u9645\u4ef7\u503c\uff0c\u4e5f\u66b4\u9732\u51fa\u6a21\u578b\u5728\u6df1\u5c42\u7a0b\u5e8f\u5f52\u7eb3\u63a8\u7406\u4e0a\u7684\u80fd\u529b\u4e0a\u9650\u3002<\/p>\n\n\n\n \u8bba\u6587\u8fdb\u4e00\u6b65\u5206\u6790\u4e86\u5931\u8d25\u6848\u4f8b\u3002\u4e00\u4e2a\u91cd\u8981\u53d1\u73b0\u662f\uff1a\u5f88\u591a\u5931\u8d25\u5e76\u4e0d\u662f\u56e0\u4e3a LLM \u751f\u6210\u7684\u4e0d\u53d8\u91cf\u5b8c\u5168\u9519\u8bef\uff0c\u800c\u662f\u56e0\u4e3a\u4e0d\u53d8\u91cf\u592a\u5f31\u6216\u8005\u9a8c\u8bc1\u8fc7\u7a0b\u8d85\u65f6\u3002<\/p>\n\n\n\n \u90e8\u5206 LLM \u751f\u6210\u7684\u4e0d\u53d8\u91cf\u4e0e\u539f\u59cb\u65ad\u8a00\u51e0\u4e4e\u76f8\u540c\uff0c\u7f3a\u4e4f\u5206\u89e3\u4f5c\u7528\u3002\u4e5f\u5c31\u662f\u8bf4\uff0c\u5b83\u6ca1\u6709\u771f\u6b63\u5e2e\u52a9\u9a8c\u8bc1\u5668\u628a\u590d\u6742\u8bc1\u660e\u4efb\u52a1\u62c6\u6210\u66f4\u5bb9\u6613\u5904\u7406\u7684\u5b50\u95ee\u9898\u3002<\/p>\n\n\n\n \u8fd8\u6709\u4e00\u4e9b\u4e0d\u53d8\u91cf\u53ea\u662f\u7b80\u5355\u8fb9\u754c\u6761\u4ef6\uff0c\u867d\u7136\u53ef\u80fd\u6b63\u786e\uff0c\u4f46\u65e0\u6cd5\u6355\u6349\u5faa\u73af\u7684\u6838\u5fc3\u884c\u4e3a\u3002\u4f8b\u5982\uff0c\u53ea\u7ed9\u51fa\u53d8\u91cf\u4e0a\u4e0b\u754c\uff0c\u5374\u6ca1\u6709\u63cf\u8ff0\u53d8\u91cf\u4e4b\u95f4\u7684\u5173\u7cfb\u3001\u6a21\u8fd0\u7b97\u7ed3\u6784\u6216\u5f52\u7eb3\u5f0f\u89c4\u5f8b\u3002<\/p>\n\n\n\n \u8fd9\u5bf9\u6211\u4eec\u7684\u7814\u7a76\u5f88\u6709\u542f\u53d1\uff1a\u98df\u54c1\u63a8\u7406\u4e2d\u7684\u5019\u9009\u547d\u9898\u4e5f\u4e0d\u80fd\u53ea\u8ffd\u6c42\u201c\u770b\u8d77\u6765\u6b63\u786e\u201d\uff0c\u8fd8\u8981\u770b\u5b83\u662f\u5426\u771f\u6b63\u63d0\u4f9b\u63a8\u7406\u589e\u76ca\u3002\u4f8b\u5982\uff1a<\/p>\n\n\n\n \u201c\u914d\u6599\u603b\u548c\u4e3a 100%\u201d\u662f\u6b63\u786e\u7684\uff0c\u4f46\u53ef\u80fd\u8fc7\u4e8e\u57fa\u7840\uff1b \u547d\u9898\u7684\u4ef7\u503c\u4e0d\u53ea\u5728\u4e8e correctness\uff0c\u66f4\u5728\u4e8e utility\u3002<\/p>\n\n\n\n \u76d1\u7763\u5fae\u8c03\u80fd\u5e26\u6765\u6e29\u548c\u63d0\u5347\uff0c\u4f46\u5e76\u6ca1\u6709\u4ea7\u751f\u8d28\u53d8\u3002\u8fd9\u8bf4\u660e LLM \u5bf9\u4e0d\u53d8\u91cf\u751f\u6210\u7684\u56f0\u96be\u4e0d\u53ea\u662f\u683c\u5f0f\u95ee\u9898\uff0c\u4e5f\u6d89\u53ca\u771f\u6b63\u7684\u7a0b\u5e8f\u8bed\u4e49\u7406\u89e3\u548c\u5f52\u7eb3\u63a8\u7406\u3002<\/p>\n\n\n\n \u76f8\u6bd4\u4e4b\u4e0b\uff0cBest-of-N Sampling \u7684\u63d0\u5347\u66f4\u660e\u663e\u3002\u539f\u56e0\u5728\u4e8e\u5b83\u628a\u95ee\u9898\u4ece\u201c\u751f\u6210\u4e00\u4e2a\u7edd\u5bf9\u6b63\u786e\u7684\u7b54\u6848\u201d\u53d8\u6210\u201c\u751f\u6210\u591a\u4e2a\u5019\u9009\uff0c\u518d\u7531\u9a8c\u8bc1\u5668\u9009\u62e9\u6700\u4f18\u5019\u9009\u201d\u3002\u8fd9\u662f\u4e00\u79cd\u975e\u5e38\u9002\u5408 LLM \u7684\u534f\u540c\u65b9\u5f0f\uff1a\u6a21\u578b\u8d1f\u8d23\u6269\u5927\u5019\u9009\u7a7a\u95f4\uff0c\u9a8c\u8bc1\u5668\u8d1f\u8d23\u7b5b\u9009\u3002<\/p>\n\n\n\n \u8fd9\u79cd\u673a\u5236\u5bf9\u81ea\u8fed\u4ee3\u547d\u9898\u5e93\u5c24\u5176\u91cd\u8981\u3002\u56e0\u4e3a\u5728\u98df\u54c1\u6807\u7b7e\u53cd\u6f14\u4efb\u52a1\u4e2d\uff0c\u6211\u4eec\u5f88\u96be\u4e00\u6b21\u751f\u6210\u5b8c\u5168\u6b63\u786e\u4e14\u6700\u6709\u7528\u7684\u89c4\u5219\u3002\u66f4\u5408\u7406\u7684\u65b9\u5f0f\u662f\u751f\u6210\u591a\u4e2a\u5019\u9009\u547d\u9898\uff0c\u518d\u901a\u8fc7\u5b9e\u9645\u53cd\u6f14\u6548\u679c\u6765\u7b5b\u9009\uff1a<\/p>\n\n\n\n \u5019\u9009\u547d\u9898 q1\uff1a\u914d\u6599\u987a\u5e8f\u6ee1\u8db3\u975e\u589e\u7ea6\u675f\uff1b \u6700\u7ec8\u7531\u7ea6\u675f\u6c42\u89e3\u5668\u5224\u65ad\u54ea\u6761\u547d\u9898\u771f\u6b63\u964d\u4f4e\u8425\u517b\u8bef\u5dee\uff0c\u54ea\u6761\u547d\u9898\u4f1a\u9020\u6210\u51b2\u7a81\uff0c\u54ea\u6761\u547d\u9898\u5e94\u8fdb\u5165\u547d\u9898\u5e93\u3002<\/p>\n\n\n\n \u8bba\u6587\u5c06 Quokka \u4e0e LaM4Inv\u3001Clause2Inv\u3001Loopy\u3001LEMUR \u7b49\u65b9\u6cd5\u8fdb\u884c\u6bd4\u8f83\u3002\u4e0d\u540c\u4e8e\u8fd9\u4e9b\u65b9\u6cd5\u4e2d\u7684\u590d\u6742\u8fc7\u6ee4\u3001\u7ec4\u5408\u3001\u4fee\u590d\u548c\u56de\u6eaf\u673a\u5236\uff0cQuokka \u91c7\u7528\u66f4\u76f4\u63a5\u7684\u9a8c\u8bc1\u5668\u8bc4\u4ef7\u63a5\u53e3\u3002\u5b9e\u9a8c\u7ed3\u679c\u663e\u793a\uff0cQuokka-gpt-5.2 best-of-8 \u5728\u591a\u4e2a timeout \u9608\u503c\u4e0b\u53d6\u5f97\u6700\u5f3a\u8868\u73b0\u3002\u5728 LEMUR benchmark \u4e0a\uff0cUAutomizer \u5728\u5341\u5206\u949f\u5185\u65e0\u6cd5\u89e3\u51b3\u4efb\u4f55\u5b9e\u4f8b\uff0c\u800c Quokka \u4ecd\u80fd\u89e3\u51b3\u66f4\u591a\u4efb\u52a1\uff0c\u5e76\u4fdd\u6301\u66f4\u4f4e\u5e73\u5747\u6c42\u89e3\u65f6\u95f4\u3002<\/p>\n\n\n\n \u5f53 LLM \u80fd\u529b\u589e\u5f3a\u65f6\uff0c\u590d\u6742\u540e\u5904\u7406\u672a\u5fc5\u603b\u662f\u5fc5\u8981\u3002\u66f4\u91cd\u8981\u7684\u662f\u5efa\u7acb\u4e00\u4e2a\u5e72\u51c0\u3001\u53ef\u9760\u3001\u53ef\u590d\u6838\u7684\u63a5\u53e3\uff1a\u8ba9 LLM \u7ed9\u51fa\u5019\u9009\u547d\u9898\uff0c\u8ba9\u9a8c\u8bc1\u5668\u5224\u65ad\u5b83\u662f\u5426\u6b63\u786e\u3001\u662f\u5426\u6709\u63a8\u7406\u8d21\u732e\u3002<\/p>\n\n\n\n \u4ece\u5b9e\u9a8c\u7ed3\u679c\u6765\u770b\uff0c\u672c\u6587\u7cfb\u7edf\u8bc1\u660e\u4e86 LLM \u5728\u5faa\u73af\u4e0d\u53d8\u91cf\u751f\u6210\u4e2d\u5177\u6709\u5b9e\u9645\u4ef7\u503c\uff0c\u4f46\u8fd9\u79cd\u4ef7\u503c\u5e76\u4e0d\u662f\u65e0\u9650\u7684\u3002<\/p>\n\n\n\n \u6027\u80fd\u4e0a\uff0cQuokka-gpt-5.2 \u5728\u6b63\u786e\u4e0d\u53d8\u91cf\u6570\u91cf\u3001\u989d\u5916\u89e3\u51b3\u5b9e\u4f8b\u548c\u5e73\u5747\u6c42\u89e3\u65f6\u95f4\u4e0a\u6574\u4f53\u9886\u5148\uff0cBest-of-N \u8fdb\u4e00\u6b65\u63d0\u5347\u8868\u73b0\u3002<\/p>\n\n\n\n \u529f\u80fd\u4e0a\uff0cQuokka \u628a LLM \u5b9a\u4f4d\u4e3a\u5019\u9009\u547d\u9898\u751f\u6210\u5668\uff0c\u628a\u9a8c\u8bc1\u5668\u5b9a\u4f4d\u4e3a\u53ef\u4fe1\u8bc4\u4f30\u5668\uff0c\u5b9e\u73b0\u4e86 LLM \u63a8\u7406\u80fd\u529b\u4e0e\u5f62\u5f0f\u5316\u9a8c\u8bc1\u673a\u5236\u7684\u534f\u540c\u3002<\/p>\n\n\n\n \u4f46\u8bba\u6587\u4e5f\u66b4\u9732\u51fa\u4e00\u4e9b\u5c40\u9650\uff1a<\/p>\n\n\n\n \u914d\u6599\u987a\u5e8f\u7ea6\u675f\uff1a\u6392\u5728\u524d\u9762\u7684\u914d\u6599\u5360\u6bd4\u4e0d\u4f4e\u4e8e\u540e\u9762\u7684\u914d\u6599\uff1b \u4f46\u8fd9\u4e9b\u547d\u9898\u4e0d\u80fd\u76f4\u63a5\u5165\u5e93\uff0c\u800c\u8981\u50cf Quokka \u4e00\u6837\u63a5\u53d7\u9a8c\u8bc1\u3002\u7cfb\u7edf\u53ef\u4ee5\u8bbe\u8ba1\u4e24\u4e2a\u95ee\u9898\uff1a<\/p>\n\n\n\n \u7b2c\u4e00\uff0c\u5019\u9009\u547d\u9898\u662f\u5426\u4e0e\u5df2\u6709\u6807\u7b7e\u6570\u636e\u3001\u8425\u517b\u6570\u636e\u5e93\u548c\u6cd5\u89c4\u77e5\u8bc6\u4e00\u81f4\uff1f \u53ea\u6709\u540c\u65f6\u5177\u5907\u5408\u7406\u6027\u548c\u63a8\u7406\u8d21\u732e\u7684\u547d\u9898\uff0c\u624d\u5e94\u8fdb\u5165\u547d\u9898\u5e93\u3002<\/p>\n\n\n\n \u56e0\u6b64\uff0c\u4efb\u52a1\u672c\u8d28\u4e0a\u662f\u4e00\u4e2a\u5f31\u4fe1\u606f\u6761\u4ef6\u4e0b\u7684\u53cd\u6f14\u95ee\u9898\uff1a<\/p>\n\n\n\n \u5df2\u77e5\u914d\u6599\u987a\u5e8f\u3001\u8425\u517b\u6210\u5206\u8868\u3001\u4ef7\u683c\u548c\u51c0\u542b\u91cf\uff1b \u9996\u5148\uff0c\u7cfb\u7edf\u8bc6\u522b\u98df\u54c1\u54c1\u7c7b\u3002\u4f8b\u5982\u9178\u5976\u3001\u996e\u6599\u3001\u997c\u5e72\u3001\u575a\u679c\u68d2\u3001\u9884\u5236\u83dc\u7b49\u4e0d\u540c\u7c7b\u522b\uff0c\u5e94\u4f7f\u7528\u4e0d\u540c\u7684\u5148\u9a8c\u547d\u9898\u548c\u7ea6\u675f\u6a21\u677f\u3002\u7cfb\u7edf\u6839\u636e\u54c1\u7c7b\u751f\u6210\u5019\u9009\u547d\u9898\u3002\u4f8b\u5982\u4e73\u5236\u54c1\u66f4\u5173\u6ce8\u4e73\u6e90\u86cb\u767d\u8d21\u732e\uff0c\u996e\u6599\u66f4\u5173\u6ce8\u6c34\u5206\u3001\u7cd6\u548c\u751c\u5473\u5242\uff0c\u997c\u5e72\u7cd5\u70b9\u66f4\u5173\u6ce8\u6cb9\u8102\u3001\u7cd6\u548c\u7cbe\u5236\u78b3\u6c34\uff0c\u575a\u679c\u68d2\u66f4\u5173\u6ce8\u575a\u679c\u771f\u5b9e\u542b\u91cf\u548c\u86cb\u767d\u8d28\u5bc6\u5ea6\u3002<\/p>\n\n\n\n \u7136\u540e\uff0c\u7cfb\u7edf\u901a\u8fc7\u7ea6\u675f\u4f18\u5316\u5668\u53cd\u63a8\u914d\u6599\u6bd4\u4f8b\u548c\u8425\u517b\u8d21\u732e\u3002\u4e0d\u662f\u7b80\u5355\u770b\u914d\u6599\u8868\u987a\u5e8f\uff0c\u4e5f\u4e0d\u662f\u76f4\u63a5\u76f8\u4fe1\u6a21\u578b\u4f30\u8ba1\uff0c\u800c\u662f\u5229\u7528\u8425\u517b\u6210\u5206\u8868\u4f5c\u4e3a\u53ef\u68c0\u9a8c\u76ee\u6807\u3002<\/p>\n\n\n\n \u6700\u540e\uff0c\u7cfb\u7edf\u5c06\u53cd\u6f14\u7ed3\u679c\u7528\u4e8e\u8bc4\u5206\u3002\u8bc4\u5206\u4e0d\u53ea\u770b\u6bcf 100g \u7684\u57fa\u7840\u8425\u517b\u6210\u5206\uff0c\u8fd8\u53ef\u4ee5\u7ed3\u5408\u914d\u6599\u8d28\u91cf\u3001\u86cb\u767d\u8d28\u5bc6\u5ea6\u3001\u6dfb\u52a0\u7cd6\u98ce\u9669\u3001\u94a0\u542b\u91cf\u3001\u7406\u8bba\u539f\u6599\u4ef7\u503c\u3001\u5355\u4f4d\u4ef7\u683c\u7b49\u6307\u6807\uff0c\u8f93\u51fa\u98df\u54c1\u6027\u4ef7\u6bd4\u5224\u65ad\u3002<\/p>\n\n\n\n \u5982\u679c\u67d0\u6761\u547d\u9898\u9891\u7e41\u964d\u4f4e\u8bef\u5dee\uff0c\u5c31\u63d0\u9ad8\u5176\u6743\u91cd\uff1b\u5982\u679c\u67d0\u6761\u547d\u9898\u7ecf\u5e38\u5bfc\u81f4\u7ea6\u675f\u4e0d\u53ef\u6ee1\u8db3\u6216\u89e3\u91ca\u51b2\u7a81\uff0c\u5c31\u964d\u4f4e\u6743\u91cd\u6216\u6dd8\u6c70\u3002\u8fd9\u6837\u5c31\u80fd\u5f62\u6210\u4e00\u4e2a\u7c7b\u4f3c Quokka \u7684\u81ea\u8fed\u4ee3\u95ed\u73af\uff1a<\/p>\n\n\n\n \u5019\u9009\u547d\u9898\u751f\u6210 \u2192 \u7ea6\u675f\u9a8c\u8bc1 \u2192 \u6548\u679c\u8bc4\u4f30 \u2192 \u547d\u9898\u5165\u5e93 \u2192 \u6743\u91cd\u66f4\u65b0 \u2192 \u4e0b\u4e00\u8f6e\u63a8\u7406\u3002<\/p>\n","protected":false},"excerpt":{"rendered":" \u4f5c\u8005\uff1aAnjiang Wei, Tianran Sun, Tarun Suresh, Haoze Wu, Ke […]<\/p>\n","protected":false},"author":75,"featured_media":0,"comment_status":"closed","ping_status":"","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-5261","post","type-post","status-publish","format-standard","hentry","category-events"],"_links":{"self":[{"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/posts\/5261","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/users\/75"}],"replies":[{"embeddable":true,"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/comments?post=5261"}],"version-history":[{"count":36,"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/posts\/5261\/revisions"}],"predecessor-version":[{"id":5298,"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/posts\/5261\/revisions\/5298"}],"wp:attachment":[{"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/media?parent=5261"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/categories?post=5261"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.15zhi.net\/blog\/wp-json\/wp\/v2\/tags?post=5261"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\u4e00. \u7814\u7a76\u80cc\u666f<\/h3>\n\n\n\n
\u4e8c. \u8bba\u6587\u6982\u8981<\/h3>\n\n\n\n
\n
\u4e09. \u6838\u5fc3\u601d\u60f3<\/h3>\n\n\n\n
\u56db. \u65b9\u6cd5\u8bbe\u8ba1<\/h3>\n\n\n\n
4.1 \u5faa\u73af\u4e0d\u53d8\u91cf\u7684\u5f62\u5f0f\u5316\u5b9a\u4e49<\/h4>\n\n\n\n
\n
\u5373\u8fdb\u5165\u5faa\u73af\u524d\uff0c\u4e0d\u53d8\u91cf I \u5df2\u7ecf\u6210\u7acb\u3002<\/li>\n\n\n\n
\u5373\u5982\u679c\u5faa\u73af\u5f00\u59cb\u65f6 I \u6210\u7acb\uff0c\u5e76\u4e14\u5faa\u73af\u6761\u4ef6 B \u4e3a\u771f\uff0c\u90a3\u4e48\u6267\u884c\u4e00\u6b21\u5faa\u73af\u4f53 S \u540e\uff0cI \u4ecd\u7136\u6210\u7acb\u3002<\/li>\n\n\n\n
\u5373\u5f53\u5faa\u73af\u7ed3\u675f\u65f6\uff0c\u5982\u679c I \u6210\u7acb\u4e14\u5faa\u73af\u6761\u4ef6\u4e0d\u518d\u6ee1\u8db3\uff0c\u90a3\u4e48\u53ef\u4ee5\u63a8\u51fa\u76ee\u6807\u540e\u7f6e\u6761\u4ef6 Q\u3002<\/li>\n<\/ol>\n\n\n\n
\n\n\n\n4.2 Verifier-Based Approach\uff1a\u4e24\u4e2a\u9a8c\u8bc1\u5668\u67e5\u8be2<\/h4>\n\n\n\n
p*\uff1a\u5f85\u9a8c\u8bc1\u7684\u76ee\u6807\u6027\u8d28
q\uff1aLLM \u751f\u6210\u7684\u5019\u9009\u4e0d\u53d8\u91cf<\/p>\n\n\n\n
\u5982\u679c\u5728 q \u7684\u5047\u8bbe\u4e0b\u4ecd\u7136\u80fd\u53d1\u73b0\u76ee\u6807\u6027\u8d28\u7684\u53cd\u4f8b\uff0c\u90a3\u4e48\u8f93\u51fa F\uff0c\u8868\u793a\u76ee\u6807\u6027\u8d28\u88ab\u53cd\u9a73\u3002
\u5982\u679c\u9a8c\u8bc1\u5668\u65e0\u6cd5\u8bc1\u660e q\uff0c\u6216\u8005\u52a0\u5165 q \u540e\u4ecd\u65e0\u6cd5\u8bc1\u660e\u76ee\u6807\u6027\u8d28\uff0c\u5219\u8f93\u51fa U\uff0c\u8868\u793a\u7ed3\u679c\u4e0d\u786e\u5b9a\u3002<\/p>\n\n\n\n
\n\n\n\n4.3 \u8bed\u6cd5\u68c0\u67e5\u4e0e\u5e76\u884c\u9a8c\u8bc1<\/h4>\n\n\n\n
\u201c\u8fd9\u4e2a\u4ea7\u54c1\u6bd4\u8f83\u5065\u5eb7\u201d\u5219\u4e0d\u662f\u4e00\u4e2a\u76f4\u63a5\u53ef\u6c42\u89e3\u7684\u7ea6\u675f\uff1b
\u201c\u86cb\u767d\u8d28\u4e3b\u8981\u6765\u81ea\u4e73\u6e90\u6210\u5206\u201d\u9700\u8981\u8fdb\u4e00\u6b65\u8f6c\u6210\u8425\u517b\u8d21\u732e\u6bd4\u4f8b\u7ea6\u675f\uff0c\u624d\u80fd\u8fdb\u5165\u6c42\u89e3\u5668\u3002<\/p>\n\n\n\n
\n\n\n\n4.4 SFT \u4e0e Best-of-N Sampling<\/h4>\n\n\n\n
\u4e94. \u5b9e\u9a8c\u8bbe\u8ba1<\/h3>\n\n\n\n
\n
\n
5.1 \u4e0d\u540c LLM \u7684\u8868\u73b0\u5dee\u5f02<\/h4>\n\n\n\n
\u5728 60s timeout \u4e0b\uff0cgpt-5.2 \u989d\u5916\u89e3\u51b3\u4e86 21 \u4e2a UAutomizer baseline \u65e0\u6cd5\u89e3\u51b3\u7684\u5b9e\u4f8b\u3002
\u4f46\u5728 500s timeout \u4e0b\uff0c\u989d\u5916\u6536\u76ca\u663e\u8457\u4e0b\u964d\uff0c\u8bf4\u660e LLM \u5bf9\u4e2d\u7b49\u96be\u5ea6\u4efb\u52a1\u6709\u660e\u663e\u52a0\u901f\u4f5c\u7528\uff0c\u4f46\u9762\u5bf9\u6700\u96be\u9a8c\u8bc1\u4efb\u52a1\u65f6\uff0c\u4ecd\u96be\u4ee5\u751f\u6210\u8db3\u591f\u5f3a\u7684\u4e0d\u53d8\u91cf\u3002<\/p>\n\n\n\n
\n\n\n\n5.2 \u5931\u8d25\u6a21\u5f0f\u5206\u6790<\/h4>\n\n\n\n
\u201c\u9999\u7cbe\u3001\u9632\u8150\u5242\u3001\u8272\u7d20\u603b\u5360\u6bd4\u901a\u5e38\u4f4e\u4e8e 1%\u201d\u66f4\u6709\u52a9\u4e8e\u538b\u7f29\u89e3\u7a7a\u95f4\uff1b
\u201c\u4e73\u5236\u54c1\u4e2d\u86cb\u767d\u8d28\u4e3b\u8981\u6765\u81ea\u4e73\u6e90\u914d\u6599\u201d\u53ef\u80fd\u5bf9\u4e73\u5236\u54c1\u53cd\u6f14\u8d21\u732e\u66f4\u5927\u3002<\/p>\n\n\n\n
\n\n\n\n5.3 SFT \u4e0e Best-of-N \u7684\u6548\u679c<\/h4>\n\n\n\n
\u5019\u9009\u547d\u9898 q2\uff1a\u6dfb\u52a0\u5242\u7c7b\u914d\u6599\u603b\u5360\u6bd4\u5c0f\u4e8e\u9608\u503c\uff1b
\u5019\u9009\u547d\u9898 q3\uff1a\u996e\u6599\u7c7b\u98df\u54c1\u4e2d\u6c34\u5206\u5360\u6bd4\u9ad8\u4e8e\u9608\u503c\uff1b
\u5019\u9009\u547d\u9898 q4\uff1a\u4e73\u6e90\u914d\u6599\u8d21\u732e\u4e3b\u8981\u86cb\u767d\u8d28\u6765\u6e90\uff1b
\u5019\u9009\u547d\u9898 q5\uff1a\u9ad8\u94a0\u98df\u54c1\u4e2d\u76d0\u7c7b\u914d\u6599\u8d21\u732e\u4e3b\u8981\u94a0\u6765\u6e90\u3002<\/p>\n\n\n\n
\n\n\n\n5.4 \u4e0e\u5df2\u6709 LLM-based Verifier \u7684\u6bd4\u8f83<\/h4>\n\n\n\n
\n
\u8fd9\u8bf4\u660e\u751f\u6210\u201c\u6b63\u786e\u4f46\u65e0\u7528\u201d\u7684\u547d\u9898\u4ecd\u7136\u662f LLM \u7684\u5e38\u89c1\u95ee\u9898\u3002<\/li>\n\n\n\n
\u7b80\u5355\u76d1\u7763\u5fae\u8c03\u4e0d\u8db3\u4ee5\u89e3\u51b3\u6df1\u5c42\u5f52\u7eb3\u63a8\u7406\u95ee\u9898\uff0c\u672a\u6765\u53ef\u80fd\u9700\u8981\u66f4\u5f3a\u7684\u641c\u7d22\u3001\u53cd\u9988\u5b66\u4e60\u6216 verifier-in-the-loop \u8bad\u7ec3\u673a\u5236\u3002<\/li>\n\n\n\n
LLM \u672c\u8eab\u5e76\u4e0d\u63d0\u4f9b\u53ef\u9760\u6027\u4fdd\u8bc1\uff0c\u7cfb\u7edf\u6700\u7ec8\u53ef\u4fe1\u6027\u6765\u81ea UAutomizer \u7b49\u5f62\u5f0f\u5316\u9a8c\u8bc1\u5668\u3002<\/li>\n\n\n\n
Quokka \u7684\u65b9\u6cd5\u8bba\u5177\u6709\u8fc1\u79fb\u4ef7\u503c\uff0c\u4f46\u82e5\u8fc1\u79fb\u5230\u98df\u54c1\u3001\u533b\u5b66\u3001\u6cd5\u5f8b\u7b49\u5f31\u5f62\u5f0f\u5316\u9886\u57df\uff0c\u9700\u8981\u91cd\u65b0\u8bbe\u8ba1\u201c\u9a8c\u8bc1\u5668\u201d\u7684\u5b9a\u4e49\u3002<\/li>\n<\/ol>\n\n\n\n\u516d. \u5bf9\u9f50\u601d\u8003<\/h3>\n\n\n\n
\n
\u8425\u517b\u8d21\u732e\u7ea6\u675f\uff1a\u4ea7\u54c1\u8425\u517b\u503c\u7ea6\u7b49\u4e8e\u5404\u914d\u6599\u8425\u517b\u8d21\u732e\u7684\u52a0\u6743\u548c\uff1b
\u7c7b\u522b\u5148\u9a8c\u7ea6\u675f\uff1a\u996e\u6599\u7c7b\u98df\u54c1\u4e2d\u6c34\u5206\u5360\u6bd4\u8f83\u9ad8\uff0c\u9999\u7cbe\u548c\u8272\u7d20\u5360\u6bd4\u8f83\u4f4e\uff1b
\u4ef7\u683c\u5408\u7406\u6027\u7ea6\u675f\uff1a\u7406\u8bba\u539f\u6599\u6210\u672c\u4e0e\u5e02\u573a\u552e\u4ef7\u4e4b\u95f4\u5b58\u5728\u5408\u7406\u533a\u95f4\uff1b
\u6cd5\u89c4\u5408\u89c4\u7ea6\u675f\uff1a\u67d0\u4e9b\u8425\u517b\u58f0\u79f0\u3001\u914d\u6599\u6807\u8bc6\u3001\u6dfb\u52a0\u5242\u4f7f\u7528\u9700\u8981\u6ee1\u8db3\u6807\u51c6\u8981\u6c42\u3002<\/p>\n\n\n\n
\u7b2c\u4e8c\uff0c\u52a0\u5165\u8be5\u547d\u9898\u540e\uff0c\u914d\u6599\u6bd4\u4f8b\u53cd\u6f14\u8bef\u5dee\u662f\u5426\u4e0b\u964d\uff0c\u89e3\u7a7a\u95f4\u662f\u5426\u7f29\u5c0f\uff0c\u8bc4\u5206\u7ed3\u679c\u662f\u5426\u66f4\u7a33\u5b9a\uff1f<\/p>\n\n\n\n
\n\n\n\n\n
\u672a\u77e5\u5404\u914d\u6599\u771f\u5b9e\u5360\u6bd4\u3001\u5404\u8425\u517b\u7d20\u8d21\u732e\u6765\u6e90\u3001\u7406\u8bba\u539f\u6599\u4ef7\u503c\u548c\u7efc\u5408\u6027\u4ef7\u6bd4\u3002<\/p>\n\n\n\n
\n\n\n\n\n