Google ได้ขยายระบบ Antigravity ที่เป็นระบบหลายตัวแทน โดยใช้ทีมงานที่ขับเคลื่อนด้วย Gemini ในการแก้ปัญหาทางคณิตศาสตร์ที่มีมายาวนาน การตรวจสอบหลักฐานที่ซับซ้อน และการเพิ่มประสิทธิภาพซอฟต์แวร์ บริษัทได้ระบุว่า ระบบ Teamwork ของพวกเขาช่วยให้นักวิจัยสามารถทำให้ผลลัพธ์ทางคณิตศาสตร์ที่สำคัญเป็นทางการ ระบุโครงสร้างโมเลกุล และพัฒนาการดำเนินการซอฟต์แวร์ที่รวดเร็วขึ้น งานนี้รวมความเชี่ยวชาญของมนุษย์เข้ากับความร่วมมือของตัวแทนหลายตัวที่สำรวจวิธีแก้ปัญหา ทดสอบวิธีการ และใช้เครื่องมือคอมพิวเตอร์ในการตรวจสอบผลลัพธ์
หนึ่งในผลลัพธ์ที่น่าทึ่งที่สุดคือการทำให้ Weil Conjecture เป็นทางการ ซึ่งเป็นชุดของผลลัพธ์ทางคณิตศาสตร์ที่สำคัญเกี่ยวกับจำนวนของการแก้สมการพหุนามในฟิลด์ที่จำกัด ระบบ Teamwork-LEAP ของ Google สร้างโค้ด Lean ประมาณ 1.8 ล้านบรรทัดจากการเรียกใช้ตัวแทนย่อย 28,800 ครั้งเพื่อทำให้ผลลัพธ์เหล่านี้เป็นทางการ ซึ่งผลลัพธ์เหล่านี้ถูกพิสูจน์โดยนักคณิตศาสตร์ Pierre Deligne ในปี 1974 Google ยังระบุว่าระบบนี้ได้ทำให้การพิสูจน์ล่าสุดเกี่ยวกับการระเบิดในเวลาจำกัดของสมการ Navier–Stokes สามมิติเป็นทางการ ซึ่งเป็นปัญหาที่เกี่ยวข้องกับหนึ่งในเจ็ดปัญหารางวัล Millennium
คำถามเกี่ยวกับการพัฒนาของการแก้สมการเหล่านี้ที่มีความเรียบง่ายในเวลาจำกัดได้ค้างคาอยู่ประมาณ 90 ปี
ระบบ Antigravity ของ Google ประสบความสำเร็จอย่างมากในด้านคณิตศาสตร์และเคมี
ระบบนี้ยังช่วยให้นักวิจัยสามารถแก้ปัญหา Courtade–Kumar Conjecture ซึ่งเป็นปัญหาทางทฤษฎีข้อมูลที่ถูกเสนอครั้งแรกในปี 2013 นักวิจัยจาก Google และสถาบันการศึกษาได้ใช้กรอบงานนี้ในการพัฒนาหลักฐานที่ครอบคลุม โมเดล Gemini ช่วยในการอนุมานขอบเขตการวิเคราะห์และสร้างใบรับรองที่สามารถตรวจสอบได้โดยคอมพิวเตอร์ นักวิจัยได้ทำให้หลักฐานนี้เป็นทางการใน Lean 4 ซึ่งเป็นภาษาการเขียนโปรแกรมและผู้ช่วยการพิสูจน์ที่ช่วยให้คอมพิวเตอร์สามารถตรวจสอบข้อโต้แย้งทางคณิตศาสตร์ได้ วิธีการของ Google ขึ้นอยู่กับการทำงานร่วมกันของตัวแทนหลายตัว โดยมอบหมายงานที่แตกต่างกันให้กับแต่ละระบบเพื่อตรวจสอบและยืนยันวิธีแก้ปัญหาที่เสนอ โดยมีจุดมุ่งหมายเพื่อลดข้อผิดพลาดที่อาจเกิดขึ้นเมื่อโมเดลเดียวสร้างสายการอนุมานที่ยาว
ตัวแทนเฉพาะทางแต่ละตัวจะได้รับเอกสารและเครื่องมือที่จำเป็นต่อการดำเนินงานของตนเท่านั้น ผู้ตรวจสอบและผู้ตรวจสอบอิสระจะตรวจสอบผลลัพธ์โดยไม่พึ่งพาการอนุมานของตัวแทนต้นฉบับ นอกจากทางคณิตศาสตร์แล้ว Google ยังได้นำวิธีการนี้ไปใช้ในเคมีโมเลกุล ตัวแทนเฉพาะทางจำนวน 30 ตัวทำงานร่วมกับตัวจำลองข้อมูลทางกายภาพในการระบุโครงสร้างโมเลกุลจากข้อมูลการสแกนด้วยคลื่นแม่เหล็กไฟฟ้า (NMR) โดยมีความแม่นยำสูงสุด 95% และความแม่นยำในสามอันดับแรก 100% สำหรับโมเลกุลที่มีความซับซ้อน
กรอบงานนี้ยังประสบความสำเร็จในด้านวิศวกรรมระบบ Google ระบุว่าตัวแทนของพวกเขาได้เขียนโปรแกรมตัวถอดรหัสวิดีโอ libgav1 AV1 ของบริษัทใหม่จาก C++ เป็นโค้ด Rust ประมาณ 170,000 บรรทัด โดยสามารถทำให้การส่งออกมีความสอดคล้องกันอย่างสมบูรณ์ในชุดทดสอบที่กว้างขวาง การเขียนโปรแกรมใหม่ในตอนแรกทำงานได้เร็วประมาณสี่เท่าของการดำเนินการเดิม เมื่อได้รับเครื่องมือวิเคราะห์ประสิทธิภาพและได้รับมอบหมายให้ปรับปรุงประสิทธิภาพ เวอร์ชัน Rust กลายเป็นเร็วขึ้น 20% ถึง 30% เมื่อเปรียบเทียบกับการดำเนินการ C++ เดิมบนโปรเซสเซอร์ x86_64 และ ARM
ในโครงการอีกหนึ่งโครงการ แผนการที่ใช้เวลาสองสัปดาห์ได้ทำการเขียนโปรแกรมโค้ด C++ ที่เหลืออยู่ในไมโครเคอร์เนล Zircon ใหม่เป็นโค้ด Rust ที่ปลอดภัยจากหน่วยความจำประมาณ 800,000 บรรทัด ซึ่งผ่านการทดสอบหน่วยของเคอร์เนลและสามารถเริ่มต้นบนฮาร์ดแวร์ ARM64 ได้
Google ยังรายงานเกี่ยวกับการปรับปรุงโครงสร้างพื้นฐานภายในของตน โดยการทำงานอัตโนมัติในการจัดตารางงานของพวกเขาลดการแย่งชิงภาระงาน TPU บนฮาร์ดแวร์บางประเภทลง 24% ในขณะที่ยังคงรักษาเป้าหมายระดับบริการและอัตราการใช้กลุ่ม บริษัทกำลังนำเสนอ Teamwork และกระบวนการเขียนโค้ดที่พัฒนาขึ้นผ่าน Antigravity โดยเปิดให้มีการสมัครจากนักวิจัยทางวิชาการจำนวน 10,000 คนเพื่อรับสิทธิ์เข้าถึงการใช้งานสูงฟรีเป็นระยะเวลา 6 เดือน บริษัทระบุว่าจะมีการนำเสนอการทำงานเฉพาะทางเพิ่มเติมในอนาคต รวมถึงเครื่องมือในการพิสูจน์ทางการ