پژوهش: عامل‌های هوش مصنوعی در صورت‌بندی برهان با ترجیح‌های انسانی تفاوت دارند

پژوهشی پیش‌چاپ در arXiv با بررسی ۹ همکاری بزرگ انسانی در محیط اثبات‌گر Lean، تفاوت‌های عامل‌های هوش مصنوعی و انسان‌ها را هنگام ساخت برهان بررسی کرده است. این مجموعه شامل ۴٫۷ میلیون تعریف در بیش از ۶ هزار commit بود و پژوهشگران برای مطالعهٔ ترجیح‌ها از روشی به نام «همکاری شبیه‌سازی‌شده» استفاده کردند.

یافته‌ها نشان می‌دهد عامل‌های هوش مصنوعی در جریان ساخت برهان، بیش از انسان‌ها به شکاف‌هایی توجه می‌کنند که صریحاً مشخص شده‌اند. آن‌ها همچنین کمتر به مراکز اثباتِ پرتراکم و هدف‌های پیچیده یا غیرمنتظره گرایش دارند؛ در مقابل، برهان‌هایی را که بدنهٔ غیرمنتظره دارند بیشتر می‌پسندند و معمولاً آن‌ها را به سمت الگوهای متعارف‌تر می‌برند. نویسندگان می‌گویند این تفاوت‌ها می‌تواند نقاط کور همکاری انسان و هوش مصنوعی در ریاضیات را آشکار کند و به طراحی مداخله‌های بهتر کمک کند.